From 1b95e78dbb71f76c475bab62b648e6af9f043a79 Mon Sep 17 00:00:00 2001
From: Rahul Chhabra <rahul29112002@gmail.com>
Date: Sat, 17 Aug 2024 00:01:17 +0530
Subject: [PATCH] Isomorphism of PERs and Modest Sets

---
 .../#SubQuotientCanonicalPERToOriginal.agda#  |  53 +++++++
 .../.#SubQuotientCanonicalPERToOriginal.agda  |   1 +
 src/Realizability/Modest/CanonicalPER.agda    |  22 +--
 .../Modest/GenericUniformFamily.agda          |  17 +-
 .../Modest/SubQuotientCanonicalPERIso.agda    | 147 ++++++++++++++++++
 .../SubQuotientCanonicalPERToOriginal.agda    |  49 +++---
 .../Modest/UnresizedGeneric.agda              |  10 +-
 7 files changed, 261 insertions(+), 38 deletions(-)
 create mode 100644 src/Realizability/Modest/#SubQuotientCanonicalPERToOriginal.agda#
 create mode 120000 src/Realizability/Modest/.#SubQuotientCanonicalPERToOriginal.agda
 create mode 100644 src/Realizability/Modest/SubQuotientCanonicalPERIso.agda

diff --git a/src/Realizability/Modest/#SubQuotientCanonicalPERToOriginal.agda# b/src/Realizability/Modest/#SubQuotientCanonicalPERToOriginal.agda#
new file mode 100644
index 0000000..c6ceb57
--- /dev/null
+++ b/src/Realizability/Modest/#SubQuotientCanonicalPERToOriginal.agda#
@@ -0,0 +1,53 @@
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Powerset
+open import Cubical.Foundations.Path
+open import Cubical.Foundations.Structure using (⟨_⟩; str)
+open import Cubical.Data.Sigma
+open import Cubical.Data.FinData
+open import Cubical.Data.Unit
+open import Cubical.HITs.PropositionalTruncation as PT hiding (map)
+open import Cubical.HITs.PropositionalTruncation.Monad
+open import Cubical.HITs.SetQuotients as SQ
+open import Cubical.Reflection.RecordEquiv
+open import Cubical.Categories.Category
+open import Cubical.Categories.Displayed.Base
+open import Cubical.Categories.Displayed.Reasoning
+open import Cubical.Categories.Limits.Pullback
+open import Cubical.Categories.Functor hiding (Id)
+open import Cubical.Categories.Constructions.Slice
+open import Categories.CartesianMorphism
+open import Categories.GenericObject
+open import Realizability.CombinatoryAlgebra
+open import Realizability.ApplicativeStructure
+open import Realizability.PropResizing
+
+module Realizability.Modest.SubQuotientCanonicalPERToOriginal {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) where
+
+open import Realizability.Assembly.Base ca
+open import Realizability.Assembly.Morphism ca
+open import Realizability.Assembly.Terminal ca
+open import Realizability.Assembly.SetsReflectiveSubcategory ca
+open import Realizability.Modest.Base ca
+open import Realizability.Modest.UniformFamily ca
+open import Realizability.Modest.CanonicalPER ca
+open import Realizability.PERs.PER ca
+open import Realizability.PERs.SubQuotient ca
+
+open Assembly
+open CombinatoryAlgebra ca
+open Realizability.CombinatoryAlgebra.Combinators ca renaming (i to Id; ia≡a to Ida≡a)
+open Contravariant UNIMOD
+open UniformFamily
+open DisplayedUFamMap
+
+module
+  _ {X : Type ℓ}
+  (asmX : Assembly X)
+  (isModestAsmX : isModest asmX) where
+
+  
+
diff --git a/src/Realizability/Modest/.#SubQuotientCanonicalPERToOriginal.agda b/src/Realizability/Modest/.#SubQuotientCanonicalPERToOriginal.agda
new file mode 120000
index 0000000..4751d10
--- /dev/null
+++ b/src/Realizability/Modest/.#SubQuotientCanonicalPERToOriginal.agda
@@ -0,0 +1 @@
+rahul@Rahuls-MacBook-Air.local.13251:1720167879
\ No newline at end of file
diff --git a/src/Realizability/Modest/CanonicalPER.agda b/src/Realizability/Modest/CanonicalPER.agda
index 30ade69..f0d0682 100644
--- a/src/Realizability/Modest/CanonicalPER.agda
+++ b/src/Realizability/Modest/CanonicalPER.agda
@@ -48,19 +48,13 @@ module _
   (isModestAsmX : isModest asmX) where
 
   canonicalPER : PER
-  PER.relation canonicalPER a b = ∃[ x ∈ X ] a ⊩[ asmX ] x × b ⊩[ asmX ] x
-  PER.isPropValued canonicalPER a b = isPropPropTrunc
-  fst (PER.isPER canonicalPER) a b ∃x = PT.map (λ { (x , a⊩x , b⊩x) → x , b⊩x , a⊩x }) ∃x
-  snd (PER.isPER canonicalPER) a b c ∃x ∃x' =
-    do
-      (x , a⊩x , b⊩x) ← ∃x
-      (x' , b⊩x' , c⊩x') ← ∃x'
-      let
-        x≡x' : x ≡ x'
-        x≡x' = isModestAsmX x x' b b⊩x b⊩x'
-
-        c⊩x : c ⊩[ asmX ] x
-        c⊩x = subst (c ⊩[ asmX ]_) (sym x≡x') c⊩x'
-      return (x , a⊩x , c⊩x)
+  PER.relation canonicalPER a b = Σ[ x ∈ X ] a ⊩[ asmX ] x × b ⊩[ asmX ] x
+  PER.isPropValued canonicalPER a b (x , a⊩x , b⊩x) (x' , a⊩x' , b⊩x') =
+    Σ≡Prop
+      (λ x → isProp× (asmX .⊩isPropValued a x) (asmX .⊩isPropValued b x))
+      (isModestAsmX x x' a a⊩x a⊩x')
+  fst (PER.isPER canonicalPER) a b (x , a⊩x , b⊩x) = x , b⊩x , a⊩x
+  snd (PER.isPER canonicalPER) a b c (x , a⊩x , b⊩x) (x' , b⊩x' , c⊩x') =
+    x' , subst (a ⊩[ asmX ]_) (isModestAsmX x x' b b⊩x b⊩x') a⊩x , c⊩x'
     
   
diff --git a/src/Realizability/Modest/GenericUniformFamily.agda b/src/Realizability/Modest/GenericUniformFamily.agda
index 2a37bef..0a0f881 100644
--- a/src/Realizability/Modest/GenericUniformFamily.agda
+++ b/src/Realizability/Modest/GenericUniformFamily.agda
@@ -70,7 +70,22 @@ GenericObject.isGeneric genericUniformFamily {X , asmX} M =
       cart' : isCartesian' f fᴰ
       cart' {Y , asmY} {N} g hᴰ =
         (! , {!!}) , {!!} where
+        
           ! : DisplayedUFamMap asmY asmX g N M
-          DisplayedUFamMap.fibrewiseMap ! y Ny = {!hᴰ .fibrewiseMap y Ny!}
+          DisplayedUFamMap.fibrewiseMap ! y Ny = lhsIsoRhs .fst .map {!hᴰ .fibrewiseMap y Ny!} module !Definition where
+            gy : X
+            gy = g .map y
+
+            canonicalPERMgy : PER
+            canonicalPERMgy = canonicalPER (M .assemblies gy) (M .isModestFamily gy)
+
+            lhsModestSet : MOD .Category.ob
+            lhsModestSet = subQuotient canonicalPERMgy , subQuotientAssembly canonicalPERMgy , isModestSubQuotientAssembly canonicalPERMgy
+
+            rhsModestSet : MOD .Category.ob
+            rhsModestSet = M .carriers gy , M .assemblies gy , M .isModestFamily gy
+
+            lhsIsoRhs : CatIso MOD lhsModestSet rhsModestSet
+            lhsIsoRhs = {!!}
           DisplayedUFamMap.isTracked ! = {!!}
     
diff --git a/src/Realizability/Modest/SubQuotientCanonicalPERIso.agda b/src/Realizability/Modest/SubQuotientCanonicalPERIso.agda
new file mode 100644
index 0000000..82cb630
--- /dev/null
+++ b/src/Realizability/Modest/SubQuotientCanonicalPERIso.agda
@@ -0,0 +1,147 @@
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Powerset
+open import Cubical.Foundations.Path
+open import Cubical.Foundations.Structure using (⟨_⟩; str)
+open import Cubical.Data.Sigma
+open import Cubical.Data.FinData
+open import Cubical.Data.Unit
+open import Cubical.HITs.PropositionalTruncation as PT hiding (map)
+open import Cubical.HITs.PropositionalTruncation.Monad
+open import Cubical.HITs.SetQuotients as SQ
+open import Cubical.Reflection.RecordEquiv
+open import Cubical.Categories.Category
+open import Cubical.Categories.Displayed.Base
+open import Cubical.Categories.Displayed.Reasoning
+open import Cubical.Categories.Limits.Pullback
+open import Cubical.Categories.Functor hiding (Id)
+open import Cubical.Categories.Constructions.Slice
+open import Categories.CartesianMorphism
+open import Categories.GenericObject
+open import Realizability.CombinatoryAlgebra
+open import Realizability.ApplicativeStructure
+open import Realizability.PropResizing
+
+module Realizability.Modest.SubQuotientCanonicalPERIso {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) where
+
+open import Realizability.Assembly.Base ca
+open import Realizability.Assembly.Morphism ca
+open import Realizability.Assembly.Terminal ca
+open import Realizability.Assembly.SetsReflectiveSubcategory ca
+open import Realizability.Modest.Base ca
+open import Realizability.Modest.UniformFamily ca
+open import Realizability.Modest.CanonicalPER ca
+open import Realizability.PERs.PER ca
+open import Realizability.PERs.SubQuotient ca
+
+open Assembly
+open CombinatoryAlgebra ca
+open Realizability.CombinatoryAlgebra.Combinators ca renaming (i to Id; ia≡a to Ida≡a)
+open Contravariant UNIMOD
+open UniformFamily
+open DisplayedUFamMap
+
+module
+  _ {X : Type ℓ}
+  (asmX : Assembly X)
+  (isModestAsmX : isModest asmX) where
+
+  theCanonicalPER : PER
+  theCanonicalPER = canonicalPER asmX isModestAsmX
+
+  theSubQuotient : Assembly (subQuotient theCanonicalPER)
+  theSubQuotient = subQuotientAssembly theCanonicalPER
+
+  invert : AssemblyMorphism theSubQuotient asmX
+  AssemblyMorphism.map invert sq = SQ.rec (asmX .isSetX) reprAction reprActionCoh sq module Invert where
+
+    reprAction : Σ[ a ∈ A ] (a ~[ theCanonicalPER ] a) → X
+    reprAction (a , x , a⊩x , _) = x
+
+    reprActionCoh : ∀ a b a~b → reprAction a ≡ reprAction b
+    reprActionCoh (a , x , a⊩x , _) (b , x' , b⊩x' , _) (x'' , a⊩x'' , b⊩x'') =
+      x
+        ≡⟨ isModestAsmX x x'' a a⊩x a⊩x'' ⟩
+      x''
+        ≡⟨ isModestAsmX x'' x' b b⊩x'' b⊩x' ⟩
+      x'
+        ∎
+  AssemblyMorphism.tracker invert = return (Id , (λ sq a a⊩sq → goal sq a a⊩sq)) where
+    realizability : (sq : subQuotient theCanonicalPER) → (a : A) → a ⊩[ theSubQuotient ] sq → a ⊩[ asmX ] (invert .map sq)
+    realizability sq a a⊩sq =
+      SQ.elimProp
+        {P = motive}
+        isPropMotive
+        elemMotive
+        sq a a⊩sq where
+
+      motive : (sq : subQuotient theCanonicalPER) → Type _
+      motive sq = ∀ (a : A) → a ⊩[ theSubQuotient ] sq → a ⊩[ asmX ] (invert .map sq)
+
+      isPropMotive : ∀ sq → isProp (motive sq)
+      isPropMotive sq = isPropΠ2 λ a a⊩sq → asmX .⊩isPropValued _ _
+
+      elemMotive : (x : domain theCanonicalPER) → motive [ x ]
+      elemMotive (r , x , r⊩x , _) a (x' , a⊩x' , r⊩x') = subst (a ⊩[ asmX ]_) (isModestAsmX x' x r r⊩x' r⊩x) a⊩x'
+
+    goal : (sq : subQuotient theCanonicalPER) → (a : A) → a ⊩[ theSubQuotient ] sq → (Id ⨾ a) ⊩[ asmX ] (invert .map sq)
+    goal sq a a⊩sq = subst (_⊩[ asmX ] _) (sym (Ida≡a a)) (realizability sq a a⊩sq)
+
+  forward : AssemblyMorphism asmX theSubQuotient
+  AssemblyMorphism.map forward x = subquot module Forward where
+    mainMap : Σ[ a ∈ A ] (a ⊩[ asmX ] x) → subQuotient theCanonicalPER
+    mainMap (a , a⊩x) = [ a , x , a⊩x , a⊩x ]
+ 
+    mainMap2Constant : 2-Constant mainMap
+    mainMap2Constant (a , a⊩x) (b , b⊩x) = eq/ _ _ (x , a⊩x , b⊩x)
+
+    subquot : subQuotient theCanonicalPER
+    subquot = PT.rec→Set squash/ mainMap mainMap2Constant (asmX .⊩surjective x)
+  AssemblyMorphism.tracker forward =
+    return
+      (Id ,
+      (λ x a a⊩x →
+        PT.elim
+          {P = λ surj → (Id ⨾ a) ⊩[ theSubQuotient ] (PT.rec→Set squash/ (Forward.mainMap x) (Forward.mainMap2Constant x) surj)}
+          (λ surj → theSubQuotient .⊩isPropValued (Id ⨾ a) (PT.rec→Set squash/ (Forward.mainMap x) (Forward.mainMap2Constant x) surj))
+          (λ { (b , b⊩x) → x , subst (_⊩[ asmX ] x) (sym (Ida≡a a)) a⊩x , b⊩x })
+          (asmX .⊩surjective x)))
+
+  subQuotientCanonicalIso : CatIso MOD (X , asmX , isModestAsmX) (subQuotient theCanonicalPER , theSubQuotient , isModestSubQuotientAssembly theCanonicalPER)
+  fst subQuotientCanonicalIso = forward
+  isIso.inv (snd subQuotientCanonicalIso) = invert
+  isIso.sec (snd subQuotientCanonicalIso) = goal where
+    opaque
+      pointwise : ∀ sq → (invert ⊚ forward) .map sq ≡ sq
+      pointwise sq =
+        SQ.elimProp
+          (λ sq → squash/ (forward .map (invert .map sq)) sq)
+          (λ { d@(a , x , a⊩x , a⊩'x) →
+            PT.elim
+              {P = λ surj → PT.rec→Set squash/ (Forward.mainMap (Invert.reprAction [ d ] d)) (Forward.mainMap2Constant (Invert.reprAction [ d ] d)) surj ≡ [ d ]}
+              (λ surj → squash/ _ _)
+              (λ { (b , b⊩x) → eq/ _ _ (x , b⊩x , a⊩x) })
+              (asmX .⊩surjective x) })
+          sq
+
+    goal : invert ⊚ forward ≡ identityMorphism theSubQuotient
+    goal = AssemblyMorphism≡ _ _ (funExt pointwise)
+  isIso.ret (snd subQuotientCanonicalIso) = goal where
+    opaque
+      pointwise : ∀ x → (forward ⊚ invert) .map x ≡ x
+      pointwise x =
+        PT.elim
+          {P =
+            λ surj →
+              invert .map
+                (PT.rec→Set squash/ (Forward.mainMap x) (Forward.mainMap2Constant x) surj)
+              ≡ x}
+          (λ surj → asmX .isSetX _ _)
+          (λ { (a , a⊩x) → refl })
+          (asmX .⊩surjective x)
+
+    goal : forward ⊚ invert ≡ identityMorphism asmX
+    goal = AssemblyMorphism≡ _ _ (funExt pointwise)
diff --git a/src/Realizability/Modest/SubQuotientCanonicalPERToOriginal.agda b/src/Realizability/Modest/SubQuotientCanonicalPERToOriginal.agda
index 319a0ad..e492d8c 100644
--- a/src/Realizability/Modest/SubQuotientCanonicalPERToOriginal.agda
+++ b/src/Realizability/Modest/SubQuotientCanonicalPERToOriginal.agda
@@ -56,24 +56,37 @@ module
   theSubQuotient = subQuotientAssembly theCanonicalPER
 
   invert : AssemblyMorphism theSubQuotient asmX
-  AssemblyMorphism.map invert sq = SQ.rec (asmX .isSetX) mainMap mainMapCoh sq where
+  AssemblyMorphism.map invert sq = SQ.rec (asmX .isSetX) reprAction reprActionCoh sq module Invert where
 
-    mainMap : Σ[ a ∈ A ] (theCanonicalPER .PER.relation a a) → X
-    mainMap (a , a~a) = PT.rec→Set (asmX .isSetX) action 2ConstantAction a~a where
-      action : Σ[ x ∈ X ] ((a ⊩[ asmX ] x) × (a ⊩[ asmX ] x)) → X
-      action (x , _ , _) = x
+    reprAction : Σ[ a ∈ A ] (a ~[ theCanonicalPER ] a) → X
+    reprAction (a , x , a⊩x , _) = x
 
-      2ConstantAction : 2-Constant action
-      2ConstantAction (x , a⊩x , _) (x' , a⊩x' , _) = isModestAsmX x x' a a⊩x a⊩x'
+    reprActionCoh : ∀ a b a~b → reprAction a ≡ reprAction b
+    reprActionCoh (a , x , a⊩x , _) (b , x' , b⊩x' , _) (x'' , a⊩x'' , b⊩x'') =
+      x
+        ≡⟨ isModestAsmX x x'' a a⊩x a⊩x'' ⟩
+      x''
+        ≡⟨ isModestAsmX x'' x' b b⊩x'' b⊩x' ⟩
+      x'
+        ∎
+  AssemblyMorphism.tracker invert = return (Id , (λ sq a a⊩sq → goal sq a a⊩sq)) where
+    realizability : (sq : subQuotient theCanonicalPER) → (a : A) → a ⊩[ theSubQuotient ] sq → a ⊩[ asmX ] (invert .map sq)
+    realizability sq a a⊩sq =
+      SQ.elimProp
+        {P = motive}
+        isPropMotive
+        elemMotive
+        sq a a⊩sq where
+
+      motive : (sq : subQuotient theCanonicalPER) → Type _
+      motive sq = ∀ (a : A) → a ⊩[ theSubQuotient ] sq → a ⊩[ asmX ] (invert .map sq)
+
+      isPropMotive : ∀ sq → isProp (motive sq)
+      isPropMotive sq = isPropΠ2 λ a a⊩sq → asmX .⊩isPropValued _ _
+
+      elemMotive : (x : domain theCanonicalPER) → motive [ x ]
+      elemMotive (r , x , r⊩x , _) a (x' , a⊩x' , r⊩x') = subst (a ⊩[ asmX ]_) (isModestAsmX x' x r r⊩x' r⊩x) a⊩x'
+
+    goal : (sq : subQuotient theCanonicalPER) → (a : A) → a ⊩[ theSubQuotient ] sq → (Id ⨾ a) ⊩[ asmX ] (invert .map sq)
+    goal sq a a⊩sq = subst (_⊩[ asmX ] _) (sym (Ida≡a a)) (realizability sq a a⊩sq)
 
-    mainMapCoh : ∀ a b a~b → mainMap a ≡ mainMap b
-    mainMapCoh (a , a~a) (b , b~b) a~b =
-      PT.elim3
-        {P = λ a~a b~b a~b → mainMap (a , a~a) ≡ mainMap (b , b~b)}
-        (λ _ _ _ → asmX .isSetX _ _)
-        (λ { (x , a⊩x , _) (x' , b⊩x' , _) (x'' , a⊩x'' , b⊩x'') →
-          {!isModestAsmX x x' !} })
-        a~a
-        b~b
-        a~b
-  AssemblyMorphism.tracker invert = {!!}
diff --git a/src/Realizability/Modest/UnresizedGeneric.agda b/src/Realizability/Modest/UnresizedGeneric.agda
index 4c97614..4330640 100644
--- a/src/Realizability/Modest/UnresizedGeneric.agda
+++ b/src/Realizability/Modest/UnresizedGeneric.agda
@@ -54,15 +54,15 @@ module Unresized
   theCanonicalPER x = canonicalPER (M . assemblies x) (M .isModestFamily x)
 
   elimRealizerForMx : ∀ (x : X) (Mx : M .carriers x) → Σ[ a ∈ A ] (a ⊩[ M .assemblies x ] Mx) → subQuotient (canonicalPER (M .assemblies x) (M .isModestFamily x))
-  elimRealizerForMx x Mx (a , a⊩Mx) = [ a , (return (Mx , a⊩Mx , a⊩Mx)) ]
+  elimRealizerForMx x Mx (a , a⊩Mx) = [ a , Mx , a⊩Mx , a⊩Mx ]
 
   opaque
     elimRealizerForMx2Constant : ∀ x Mx → 2-Constant (elimRealizerForMx x Mx)
     elimRealizerForMx2Constant x Mx (a , a⊩Mx) (b , b⊩Mx) =
       eq/
-        (a , (return (Mx , a⊩Mx , a⊩Mx)))
-        (b , return (Mx , b⊩Mx , b⊩Mx))
-        (return (Mx , a⊩Mx , b⊩Mx))
+        (a , Mx , a⊩Mx , a⊩Mx)
+        (b , Mx , b⊩Mx , b⊩Mx)
+        (Mx , a⊩Mx , b⊩Mx)
 
   mainMapType : Type _
   mainMapType =
@@ -86,7 +86,7 @@ module Unresized
         ((λ { (c , c⊩Mx) →
           (elimRealizerForMx x Mx (c , c⊩Mx)) ,
           (λ a a⊩x b b⊩Mx →
-            subst (_⊩[ subQuotientAssembly (theCanonicalPER x) ] (elimRealizerForMx x Mx (c , c⊩Mx))) (sym (λ*2ComputationRule (# zero) a b)) (return (Mx , b⊩Mx , c⊩Mx))) }))
+            subst (_⊩[ subQuotientAssembly (theCanonicalPER x) ] (elimRealizerForMx x Mx (c , c⊩Mx))) (sym (λ*2ComputationRule (# zero) a b)) (Mx , b⊩Mx , c⊩Mx)) }))
         (λ { (a , a⊩Mx) (b , b⊩Mx) →
           Σ≡Prop (λ out → isPropΠ4 λ a a⊩x b b⊩Mx → str (subQuotientRealizability (theCanonicalPER x) (λ*2 (# zero) ⨾ a ⨾ b) out)) (elimRealizerForMx2Constant x Mx (a , a⊩Mx) (b , b⊩Mx)) })
         (M .assemblies x .⊩surjective Mx)