Partial Surjections stuff

rahulc29 · May 20, 2024 · a5d8149 · a5d8149
1 parent 56dbf84
commit a5d8149
Show file tree

Hide file tree

Showing 3 changed files with 124 additions and 22 deletions.
diff --git a/src/Realizability/Assembly/SIP.agda b/src/Realizability/Assembly/SIP.agda
@@ -1,10 +1,9 @@
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Structure
-open import Cubical.Foundations.SIP
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Univalence
-open import Cubical.Foundations.CartesianKanOps
+open import Cubical.Foundations.Isomorphism
 open import Cubical.Functions.FunExtEquiv
 open import Cubical.Data.Sigma
 open import Cubical.HITs.PropositionalTruncation
@@ -16,10 +15,19 @@ open Realizability.CombinatoryAlgebra.Combinators ca renaming (i to Id; ia≡a t
 open import Realizability.Assembly.Base ca
 open import Realizability.Assembly.Morphism ca
 
-Assembly≡ : ∀ {X Y : Type ℓ}
-          → (asmX : Assembly X)
-          → (asmY : Assembly Y)
-          → (P : X ≡ Y)
-          → (⊩overP : PathP (λ i → ∀ (a : A) (p : P i) → Type ℓ) (asmX ._⊩_) (asmY ._⊩_))
-          → PathP (λ i → Assembly (P i)) asmX asmY
-Assembly≡ {X} {Y} asmX asmY P ⊩overP = {!AssemblyIsoΣ!}
+module _ {X : Type ℓ} where
+
+  Assembly≡Iso : ∀ (asmA asmB : Assembly X) → Iso (asmA ≡ asmB) (∀ r x → r ⊩[ asmA ] x ≡ r ⊩[ asmB ] x)
+  Iso.fun (Assembly≡Iso asmA asmB) path r x i = r ⊩[ path i ] x
+  Assembly._⊩_ (Iso.inv (Assembly≡Iso asmA asmB) pointwisePath i) r x = pointwisePath r x i
+  Assembly.isSetX (Iso.inv (Assembly≡Iso asmA asmB) pointwisePath i) = isPropIsSet {A = X} (asmA .isSetX) (asmB .isSetX) i
+  Assembly.⊩isPropValued (Iso.inv (Assembly≡Iso asmA asmB) pointwisePath i) r x = isProp→PathP {B = λ j → isProp (pointwisePath r x j)} (λ j → isPropIsProp) (asmA .⊩isPropValued r x) (asmB .⊩isPropValued r x) i
+  Assembly.⊩surjective (Iso.inv (Assembly≡Iso asmA asmB) pointwisePath i) x = isProp→PathP {B = λ j → ∃[ a ∈ A ] (pointwisePath a x j)} (λ j → isPropPropTrunc) (asmA .⊩surjective x) (asmB .⊩surjective x) i
+  Iso.rightInv (Assembly≡Iso asmA asmB) pointwise = funExt₂ λ r x → refl
+  Iso.leftInv (Assembly≡Iso asmA asmB) path = isSetAssembly X asmA asmB _ _
+
+  Assembly≡Equiv : ∀ (asmA asmB : Assembly X) → (asmA ≡ asmB) ≃ (∀ r x → r ⊩[ asmA ] x ≡ r ⊩[ asmB ] x)
+  Assembly≡Equiv asmA asmB = isoToEquiv (Assembly≡Iso asmA asmB)
+
+  Assembly≡ : ∀ (asmA asmB : Assembly X) → (∀ r x → r ⊩[ asmA ] x ≡ r ⊩[ asmB ] x) → (asmA ≡ asmB)
+  Assembly≡ asmA asmB pointwise = Iso.inv (Assembly≡Iso asmA asmB) pointwise
diff --git a/src/Realizability/Modest/Base.agda b/src/Realizability/Modest/Base.agda
@@ -32,8 +32,8 @@ module _ {X : Type ℓ} (asmX : Assembly X) where
   isPropIsModest : isProp isModest
   isPropIsModest = isPropΠ3 λ x y a → isProp→ (isProp→ (asmX .isSetX x y))
 
-  isUniqueRealised : isModest → ∀ (a : A) → isProp (Σ[ x ∈ X ] (a ⊩[ asmX ] x))
-  isUniqueRealised isMod a (x , a⊩x) (y , a⊩y) = Σ≡Prop (λ x' → asmX .⊩isPropValued a x') (isMod x y a a⊩x a⊩y)
+  isUniqueRealized : isModest → ∀ (a : A) → isProp (Σ[ x ∈ X ] (a ⊩[ asmX ] x))
+  isUniqueRealized isMod a (x , a⊩x) (y , a⊩y) = Σ≡Prop (λ x' → asmX .⊩isPropValued a x') (isMod x y a a⊩x a⊩y)
 
 ModestSet : Type ℓ → Type (ℓ-suc ℓ)
 ModestSet X = Σ[ xs ∈ Assembly X ] isModest xs

diff --git a/src/Realizability/Modest/PartialSurjection.agda b/src/Realizability/Modest/PartialSurjection.agda
@@ -22,7 +22,8 @@ module Realizability.Modest.PartialSurjection {ℓ} {A : Type ℓ} (ca : Combina
 
 open import Realizability.Assembly.Base ca
 open import Realizability.Assembly.Morphism ca
-open import Realizability.Modest.Base ca resizing
+open import Realizability.Assembly.SIP ca
+open import Realizability.Modest.Base ca
 
 open Assembly
 open CombinatoryAlgebra ca
@@ -40,8 +41,36 @@ record PartialSurjection (X : Type ℓ) : Type (ℓ-suc ℓ) where
     isSetX : isSet X -- potentially redundant?
 open PartialSurjection
 
+module _ (X : Type ℓ) (isCorrectHLevel : isSet X) where
+  -- first we need a Σ type equivalent to partial surjections
+  -- we could use RecordEquiv but this does not give hProps and hSets and
+  -- that causes problems when trying to compute the hlevel
+
+  PartialSurjectionΣ : Type (ℓ-suc ℓ)
+  PartialSurjectionΣ = Σ[ support ∈ (A → hProp ℓ) ] Σ[ enumeration ∈ ((Σ[ a ∈ A ] ⟨ support a ⟩) → X) ] isSurjection enumeration × isSet X
+
+  isSetPartialSurjectionΣ : isSet PartialSurjectionΣ
+  isSetPartialSurjectionΣ = isSetΣ (isSet→ isSetHProp) (λ support → isSetΣ (isSet→ isCorrectHLevel) (λ enum → isSet× (isProp→isSet isPropIsSurjection) (isProp→isSet isPropIsSet)))
+
+  PartialSurjectionIsoΣ : Iso (PartialSurjection X) PartialSurjectionΣ
+  Iso.fun PartialSurjectionIsoΣ surj =
+    (λ a → (surj .support a) , (surj .isPropSupport a)) , (λ { (a , suppA) → surj .enumeration (a , suppA) }) , surj .isSurjectionEnumeration , PartialSurjection.isSetX surj
+  Iso.inv PartialSurjectionIsoΣ (support , enumeration , isSurjectionEnumeration , isSetX) = makePartialSurjection (λ a → ⟨ support a ⟩) enumeration (λ a → str (support a)) isSurjectionEnumeration isSetX
+  Iso.rightInv PartialSurjectionIsoΣ (support , enumeration , isSurjectionEnumeration , isSetX) = refl
+  support (Iso.leftInv PartialSurjectionIsoΣ surj i) a = surj .support a
+  enumeration (Iso.leftInv PartialSurjectionIsoΣ surj i) (a , suppA) = surj .enumeration (a , suppA)
+  isPropSupport (Iso.leftInv PartialSurjectionIsoΣ surj i) a = surj .isPropSupport a
+  isSurjectionEnumeration (Iso.leftInv PartialSurjectionIsoΣ surj i) = surj .isSurjectionEnumeration
+  isSetX (Iso.leftInv PartialSurjectionIsoΣ surj i) = surj .isSetX
+
+  PartialSurjection≡Σ : PartialSurjection X ≡ PartialSurjectionΣ
+  PartialSurjection≡Σ = isoToPath PartialSurjectionIsoΣ
+
+  isSetPartialSurjection : isSet (PartialSurjection X)
+  isSetPartialSurjection = subst isSet (sym PartialSurjection≡Σ) isSetPartialSurjectionΣ
+
 -- let us derive a structure of identity principle for partial surjections
-module _ (X : Type ℓ) where
+module SIP (X : Type ℓ) (isCorrectHLevel : isSet X) where
 
   PartialSurjection≡Iso :
     ∀ (p q : PartialSurjection X)
@@ -60,22 +89,24 @@ module _ (X : Type ℓ) where
       (p .isSurjectionEnumeration b) (q .isSurjectionEnumeration b) i
   isSetX (Iso.fun (PartialSurjection≡Iso p q) (suppPath , enumPath) i) = isPropIsSet (p .isSetX) (q .isSetX) i
   Iso.inv (PartialSurjection≡Iso p q) p≡q = (λ i → p≡q i .support) , (λ i → p≡q i .enumeration)
-  Iso.rightInv (PartialSurjection≡Iso p q) p≡q = {!!}
+  Iso.rightInv (PartialSurjection≡Iso p q) p≡q = isSetPartialSurjection X isCorrectHLevel _ _ _ _ 
   Iso.leftInv (PartialSurjection≡Iso p q) (suppPath , enumPath) = ΣPathP (refl , refl)
 
   PartialSurjection≡ : ∀ (p q : PartialSurjection X) → Σ[ suppPath ∈ p .support ≡ q .support ] PathP (λ i → Σ[ a ∈ A ] (suppPath i a) → X) (p .enumeration) (q .enumeration) → p ≡ q
   PartialSurjection≡ p q (suppPath , enumPath) = Iso.fun (PartialSurjection≡Iso p q) (suppPath , enumPath)
 
 -- the type of partial surjections is equivalent to the type of modest assemblies on X
-module _ (X : Type ℓ) where
+module ModestSetIso (X : Type ℓ) (isCorrectHLevel : isSet X) where
+
+  open SIP X isCorrectHLevel
 
   {-# TERMINATING #-}
   ModestSet→PartialSurjection : ModestSet X → PartialSurjection X
   support (ModestSet→PartialSurjection (xs , isModestXs)) r = ∃[ x ∈ X ] (r ⊩[ xs ] x)
   enumeration (ModestSet→PartialSurjection (xs , isModestXs)) (r , ∃x) =
     let
       answer : Σ[ x ∈ X ] (r ⊩[ xs ] x)
-      answer = PT.rec (isUniqueRealised xs isModestXs r) (λ t → t) ∃x
+      answer = PT.rec (isUniqueRealized xs isModestXs r) (λ t → t) ∃x
     in fst answer
   isPropSupport (ModestSet→PartialSurjection (xs , isModestXs)) r = isPropPropTrunc
   isSurjectionEnumeration (ModestSet→PartialSurjection (xs , isModestXs)) x =
@@ -108,7 +139,7 @@ module _ (X : Type ℓ) where
     rightInv : ∀ surj → ModestSet→PartialSurjection (PartialSurjection→ModestSet surj) ≡ surj
     rightInv surj =
       PartialSurjection≡
-        X (ModestSet→PartialSurjection (PartialSurjection→ModestSet surj)) surj
+        (ModestSet→PartialSurjection (PartialSurjection→ModestSet surj)) surj
         (funExt supportEq ,
         funExtDep
           {A = λ i → Σ-syntax A (funExt supportEq i)}
@@ -119,20 +150,28 @@ module _ (X : Type ℓ) where
             PT.elim
               {P = λ ∃x → fst
                              (PT.rec
-                              (isUniqueRealised (fst (PartialSurjection→ModestSet surj))
+                              (isUniqueRealized (fst (PartialSurjection→ModestSet surj))
                                (snd (PartialSurjection→ModestSet surj)) r)
                               (λ t → t) ∃x)
                           ≡ surj .enumeration (s , supp)}
              (λ ∃x → surj .isSetX _ _)
-             (λ { (x , r⊩x) →
+             (λ { (x , suppR , ≡x) →
                let
                  ∃x' = transport (sym (supportEq s)) supp
+                 r≡s : r ≡ s
+                 r≡s = PathPΣ p .fst
                in
                equivFun
-                 (propTruncIdempotent≃ {!!})
+                 (propTruncIdempotent≃ (surj .isSetX x (surj .enumeration (s , supp))))
                  (do
                    (x' , suppS , ≡x') ← ∃x'
-                   return {!!}) })
+                   return
+                     (x
+                       ≡⟨ sym ≡x ⟩
+                     surj .enumeration (r , suppR)
+                       ≡⟨ cong (surj .enumeration) (ΣPathP (r≡s , (isProp→PathP (λ i → surj .isPropSupport (PathPΣ p .fst i)) suppR supp))) ⟩
+                     surj .enumeration (s , supp)
+                       ∎)) })
              ∃x }) where
           supportEq : ∀ r → (∃[ x ∈ X ] (Σ[ supp ∈ surj .support r ] (surj .enumeration (r , supp) ≡ x))) ≡ support surj r
           supportEq =
@@ -143,8 +182,63 @@ module _ (X : Type ℓ) where
                 (λ ∃x → PT.rec (surj .isPropSupport r) (λ { (x , supp , ≡x) → supp }) ∃x)
                 (λ supp → return (surj .enumeration (r , supp) , supp , refl)))
 
+  leftInv : ∀ mod → PartialSurjection→ModestSet (ModestSet→PartialSurjection mod) ≡ mod
+  leftInv (asmX , isModestAsmX) =
+    Σ≡Prop
+      isPropIsModest
+      (Assembly≡ _ _
+        λ r x →
+          hPropExt
+            (isPropΣ isPropPropTrunc (λ ∃x → asmX .isSetX _ _))
+            (asmX .⊩isPropValued r x)
+            (λ { (∃x , ≡x) →
+              let
+                (x' , r⊩x') = PT.rec (isUniqueRealized asmX isModestAsmX r) (λ t → t) ∃x
+              in subst (λ x' → r ⊩[ asmX ] x') ≡x r⊩x'})
+            λ r⊩x → ∣ x , r⊩x ∣₁ , refl)
+
   IsoModestSetPartialSurjection : Iso (ModestSet X) (PartialSurjection X)
   Iso.fun IsoModestSetPartialSurjection = ModestSet→PartialSurjection
   Iso.inv IsoModestSetPartialSurjection = PartialSurjection→ModestSet
   Iso.rightInv IsoModestSetPartialSurjection = rightInv 
-  Iso.leftInv IsoModestSetPartialSurjection mod = {!!}
+  Iso.leftInv IsoModestSetPartialSurjection = leftInv
+
+record PartialSurjectionMorphism {X Y : Type ℓ} (psX : PartialSurjection X) (psY : PartialSurjection Y) : Type ℓ where
+  no-eta-equality
+  constructor makePartialSurjectionMorphism
+  field
+    map : X → Y
+    {-
+      The following "diagram" commutes
+                              
+      Xˢ -----------> X
+      |              |
+      |              |
+      |              |
+      |              |
+      |              |
+      ↓              ↓
+      Yˢ -----------> Y
+    -}
+    isTracked : ∃[ t ∈ A ] (∀ (a : A) (sᵃ : psX .support a) → Σ[ sᵇ ∈ (psY .support (t ⨾ a)) ] map (psX .enumeration (a , sᵃ)) ≡ psY .enumeration ((t ⨾ a) , sᵇ))
+
+-- SIP
+module MorphismSIP {X Y : Type ℓ} (psX : PartialSurjection X) (psY : PartialSurjection Y) where
+  open PartialSurjectionMorphism
+  PartialSurjectionMorphism≡Iso : ∀ (f g : PartialSurjectionMorphism psX psY) → Iso (f ≡ g) (f .map ≡ g .map)
+  Iso.fun (PartialSurjectionMorphism≡Iso f g) f≡g i = f≡g i .map
+  map (Iso.inv (PartialSurjectionMorphism≡Iso f g) fMap≡gMap i) = fMap≡gMap i
+  isTracked (Iso.inv (PartialSurjectionMorphism≡Iso f g) fMap≡gMap i) =
+    isProp→PathP
+      -- Agda can't infer the type B
+      {B = λ j → ∃-syntax A
+      (λ t →
+         (a : A) (sᵃ : psX .support a) →
+         Σ-syntax (psY .support (t ⨾ a))
+         (λ sᵇ →
+            fMap≡gMap j (psX .enumeration (a , sᵃ)) ≡
+            psY .enumeration (t ⨾ a , sᵇ)))}
+      (λ j → isPropPropTrunc)
+      (f .isTracked) (g .isTracked) i
+  Iso.rightInv (PartialSurjectionMorphism≡Iso f g) fMap≡gMap = refl
+  Iso.leftInv (PartialSurjectionMorphism≡Iso f g) f≡g = {!!}