From a84a79ba81af3a524d645cffd4511ba8af20038e Mon Sep 17 00:00:00 2001
From: Rahul Chhabra <rahul29112002@gmail.com>
Date: Sun, 25 Aug 2024 19:31:51 +0530
Subject: [PATCH] Subquotient functor

---
 src/Realizability/PERs/SubQuotient.agda | 97 ++++++++++++++++++++++++-
 1 file changed, 95 insertions(+), 2 deletions(-)

diff --git a/src/Realizability/PERs/SubQuotient.agda b/src/Realizability/PERs/SubQuotient.agda
index 0c12f24..ae9720f 100644
--- a/src/Realizability/PERs/SubQuotient.agda
+++ b/src/Realizability/PERs/SubQuotient.agda
@@ -67,8 +67,7 @@ module _
       (λ [a] → isPropPropTrunc)
       (λ { (a , a~a) → return (a , a~a) })
       [a]
-
-  
+      
   isModestSubQuotientAssembly : isModest subQuotientAssembly
   isModestSubQuotientAssembly x y a a⊩x a⊩y =
     SQ.elimProp2
@@ -83,3 +82,97 @@ module _
 
         isPropMotive : ∀ x y → isProp (motive x y)
         isPropMotive x y = isPropΠ3 λ _ _ _ → squash/ x y
+
+module _ (R S : PER) (f : perMorphism R S) where
+
+  subQuotientAssemblyMorphism : AssemblyMorphism (subQuotientAssembly R) (subQuotientAssembly S)
+  subQuotientAssemblyMorphism =
+    SQ.rec
+      (isSetAssemblyMorphism (subQuotientAssembly R) (subQuotientAssembly S))
+      mainMap
+      mainMapCoherence
+      f where
+
+      mainMap : perTracker R S → AssemblyMorphism (subQuotientAssembly R) (subQuotientAssembly S)
+      AssemblyMorphism.map (mainMap (f , fIsTracker)) sqR =
+        SQ.rec
+          squash/
+          mainMapRepr
+          mainMapReprCoherence
+          sqR module MainMapDefn where
+            mainMapRepr : domain R → subQuotient S
+            mainMapRepr (r , r~r) = [ f ⨾ r , fIsTracker r r r~r ]
+
+            mainMapReprCoherence : (a b : domain R) → R .PER.relation (a .fst) (b .fst) → mainMapRepr a ≡ mainMapRepr b
+            mainMapReprCoherence (a , a~a) (b , b~b) a~b = eq/ _ _ (fIsTracker a b a~b)
+ 
+      AssemblyMorphism.tracker (mainMap (f , fIsTracker)) =
+        do
+          return
+            (f ,
+            (λ sqR s s⊩sqR →
+              SQ.elimProp
+                {P =
+                  λ sqR
+                  → ∀ (s : A)
+                  → s ⊩[ subQuotientAssembly R ] sqR
+                  → ⟨ subQuotientRealizability S (f ⨾ s) (SQ.rec squash/ (MainMapDefn.mainMapRepr f fIsTracker sqR) (MainMapDefn.mainMapReprCoherence f fIsTracker sqR) sqR) ⟩}
+                (λ sqR → isPropΠ2 λ s s⊩sqR → str (subQuotientRealizability S (f ⨾ s) (SQ.rec squash/ (MainMapDefn.mainMapRepr f fIsTracker sqR) (MainMapDefn.mainMapReprCoherence f fIsTracker sqR) sqR)))
+                (λ { (a , a~a) s s~a → fIsTracker s a s~a })
+                sqR s s⊩sqR))
+
+      mainMapCoherence : (a b : perTracker R S) → isEquivTracker R S a b → mainMap a ≡ mainMap b
+      mainMapCoherence (a , a~a) (b , b~b) a~b =
+        AssemblyMorphism≡ _ _
+          (funExt
+            λ sq →
+              SQ.elimProp
+                {P =
+                  λ sq →
+                    SQ.rec
+                      squash/
+                      (MainMapDefn.mainMapRepr a a~a sq)
+                      (MainMapDefn.mainMapReprCoherence a a~a sq) sq
+                    ≡
+                    SQ.rec
+                      squash/
+                      (MainMapDefn.mainMapRepr b b~b sq)
+                      (MainMapDefn.mainMapReprCoherence b b~b sq) sq}
+                (λ sq → squash/ _ _)
+                (λ { (r , r~r) → eq/ _ _ (a~b r r~r) })
+                sq)
+    
+
+subQuotientModestSet : PER → MOD .Category.ob
+subQuotientModestSet R = subQuotient R , subQuotientAssembly R , isModestSubQuotientAssembly R
+
+subQuotientFunctor : Functor PERCat MOD
+Functor.F-ob subQuotientFunctor R = subQuotientModestSet R
+Functor.F-hom subQuotientFunctor {R} {S} f = subQuotientAssemblyMorphism R S f
+Functor.F-id subQuotientFunctor {R} =
+  AssemblyMorphism≡ _ _
+    (funExt
+      λ sqR →
+        SQ.elimProp
+          {P = λ sqR → subQuotientAssemblyMorphism R R (PERCat .Category.id {R}) .AssemblyMorphism.map sqR ≡ identityMorphism (subQuotientAssembly R) .AssemblyMorphism.map sqR}
+          (λ sqR → squash/ _ _)
+          (λ { (a , a~a) →
+            eq/ _ _
+              (subst (_~[ R ] a) (sym (Ida≡a a)) a~a) })
+          sqR)
+Functor.F-seq subQuotientFunctor {R} {S} {T} f g =
+  AssemblyMorphism≡ _ _
+    (funExt
+      λ sq →
+        SQ.elimProp3
+          {P = λ sqR f g →
+            subQuotientAssemblyMorphism R T (seq' PERCat {R} {S} {T} f g) .AssemblyMorphism.map sqR ≡
+            seq' MOD
+              {x = subQuotientModestSet R}
+              {y = subQuotientModestSet S}
+              {z = subQuotientModestSet T}
+              (subQuotientAssemblyMorphism R S f) (subQuotientAssemblyMorphism S T g) .AssemblyMorphism.map sqR}
+          (λ sq f g → squash/ _ _)
+          (λ { (a , a~a) (b , bIsTracker) (c , cIsTracker) →
+            eq/ _ _ (subst (_~[ T ] (c ⨾ (b ⨾ a))) (sym (λ*ComputationRule (` c ̇ (` b ̇ # zero)) a)) (cIsTracker (b ⨾ a) (b ⨾ a) (bIsTracker a a a~a))) })
+          sq f g)