From a5d81497ee84ce309e36b8f0f394f8d7e20f87cc Mon Sep 17 00:00:00 2001 From: Rahul Chhabra Date: Mon, 20 May 2024 19:01:32 +0530 Subject: [PATCH] Partial Surjections stuff --- src/Realizability/Assembly/SIP.agda | 26 ++-- src/Realizability/Modest/Base.agda | 4 +- .../Modest/PartialSurjection.agda | 116 ++++++++++++++++-- 3 files changed, 124 insertions(+), 22 deletions(-) diff --git a/src/Realizability/Assembly/SIP.agda b/src/Realizability/Assembly/SIP.agda index c9782fa..72f37b6 100644 --- 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 index e2e9b1c..8295067 100644 --- 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 index 7fb7aac..8ca4c13 100644 --- 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,14 +89,16 @@ 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 @@ -75,7 +106,7 @@ module _ (X : Type ℓ) where 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 = {!!}