From bd065f5ed75999b3b072dc3d73ee2b019ae25abf Mon Sep 17 00:00:00 2001 From: Rahul Chhabra Date: Wed, 15 May 2024 17:14:39 +0530 Subject: [PATCH] Start working towards LCCC on Mod --- src/Realizability/Assembly/Base.agda | 1 + src/Realizability/Assembly/Pullbacks.agda | 159 ++++++++++++++++++ .../Assembly/SetsReflectiveSubcategory.agda | 62 +++++++ src/Realizability/Assembly/Terminal.agda | 49 ++++++ src/Realizability/Modest/Base.agda | 78 +++++++++ src/Realizability/Modest/FamilyOverAsm.agda | 63 +++++++ .../Modest/PartialSurjection.agda | 150 +++++++++++++++++ src/Realizability/PERs/#TerminalObject.agda# | 43 +++++ src/Realizability/PERs/.#TerminalObject.agda | 1 + src/Realizability/PERs/PER.agda | 17 ++ src/Realizability/PERs/TerminalObject.agda | 43 +++++ src/Realizability/PropResizing.agda | 54 ++++++ 12 files changed, 720 insertions(+) create mode 100644 src/Realizability/Assembly/Pullbacks.agda create mode 100644 src/Realizability/Assembly/SetsReflectiveSubcategory.agda create mode 100644 src/Realizability/Assembly/Terminal.agda create mode 100644 src/Realizability/Modest/Base.agda create mode 100644 src/Realizability/Modest/FamilyOverAsm.agda create mode 100644 src/Realizability/Modest/PartialSurjection.agda create mode 100644 src/Realizability/PERs/#TerminalObject.agda# create mode 120000 src/Realizability/PERs/.#TerminalObject.agda create mode 100644 src/Realizability/PERs/TerminalObject.agda diff --git a/src/Realizability/Assembly/Base.agda b/src/Realizability/Assembly/Base.agda index 8ddc335..ae68e6c 100644 --- a/src/Realizability/Assembly/Base.agda +++ b/src/Realizability/Assembly/Base.agda @@ -13,6 +13,7 @@ open import Realizability.CombinatoryAlgebra module Realizability.Assembly.Base {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) where record Assembly (X : Type ℓ) : Type (ℓ-suc ℓ) where + constructor makeAssembly infix 25 _⊩_ field _⊩_ : A → X → Type ℓ diff --git a/src/Realizability/Assembly/Pullbacks.agda b/src/Realizability/Assembly/Pullbacks.agda new file mode 100644 index 0000000..d2bb815 --- /dev/null +++ b/src/Realizability/Assembly/Pullbacks.agda @@ -0,0 +1,159 @@ +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.HLevels +open import Cubical.Data.Sigma +open import Cubical.Data.FinData +open import Cubical.HITs.PropositionalTruncation hiding (map) +open import Cubical.HITs.PropositionalTruncation.Monad +open import Cubical.Categories.Limits.Pullback +open import Cubical.Categories.Category.Base +open import Cubical.Categories.Functor +open import Cubical.Categories.Constructions.Slice +open import Realizability.CombinatoryAlgebra +open import Realizability.ApplicativeStructure + +module Realizability.Assembly.Pullbacks {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) where + +open CombinatoryAlgebra ca +open Realizability.CombinatoryAlgebra.Combinators ca renaming (i to Id; ia≡a to Ida≡a) hiding (Z) +open import Realizability.Assembly.Base ca +open import Realizability.Assembly.Morphism ca + +module _ (cspn : Cospan ASM) where + open Cospan cspn + + X = l .fst + xs = l .snd + + Y = m .fst + ys = m .snd + + Z = r .fst + zs = r .snd + + f = s₁ + g = s₂ + + opaque + pullbackType : Type ℓ + pullbackType = (Σ[ x ∈ X ] Σ[ z ∈ Z ] (f .map x ≡ g .map z)) + + opaque + unfolding pullbackType + pullbackAsm : Assembly pullbackType + Assembly._⊩_ pullbackAsm = λ { r (x , z , fx≡gz) → (pr₁ ⨾ r) ⊩[ xs ] x × ((pr₂ ⨾ r) ⊩[ zs ] z) } + Assembly.isSetX pullbackAsm = isSetΣ (xs .isSetX) (λ _ → isSetΣ (zs .isSetX) (λ _ → isProp→isSet (ys .isSetX _ _))) + Assembly.⊩isPropValued pullbackAsm = λ { r (x , z , fx≡gz) → isProp× (xs .⊩isPropValued _ _) (zs .⊩isPropValued _ _) } + Assembly.⊩surjective pullbackAsm = + (λ { (x , z , fx≡gz) → + do + (a , a⊩x) ← xs .⊩surjective x + (b , b⊩z) ← zs .⊩surjective z + return + (pair ⨾ a ⨾ b , + subst (λ r' → r' ⊩[ xs ] x) (sym (pr₁pxy≡x _ _)) a⊩x , + subst (λ r' → r' ⊩[ zs ] z) (sym (pr₂pxy≡y _ _)) b⊩z) }) + + opaque + unfolding pullbackType + unfolding pullbackAsm + pullbackPr₁ : AssemblyMorphism pullbackAsm xs + AssemblyMorphism.map pullbackPr₁ (x , z , fx≡gz) = x + AssemblyMorphism.tracker pullbackPr₁ = + return (pr₁ , (λ { (x , z , fx≡gz) r (pr₁r⊩x , pr₂r⊩z) → pr₁r⊩x })) + + opaque + unfolding pullbackType + unfolding pullbackAsm + pullbackPr₂ : AssemblyMorphism pullbackAsm zs + AssemblyMorphism.map pullbackPr₂ (x , z , fx≡gz) = z + AssemblyMorphism.tracker pullbackPr₂ = + return (pr₂ , (λ { (x , z , fx≡gz) r (pr₁r⊩x , pr₂r⊩z) → pr₂r⊩z })) + + opaque + unfolding pullbackAsm + unfolding pullbackPr₁ + unfolding pullbackPr₂ + pullback : Pullback ASM cspn + Pullback.pbOb pullback = pullbackType , pullbackAsm + Pullback.pbPr₁ pullback = pullbackPr₁ + Pullback.pbPr₂ pullback = pullbackPr₂ + Pullback.pbCommutes pullback = AssemblyMorphism≡ _ _ (funExt λ { (x , z , fx≡gz) → fx≡gz }) + Pullback.univProp pullback {D , ds} p q pf≡qg = + uniqueExists + uniqueMorphism + ((AssemblyMorphism≡ _ _ (funExt (λ d → refl))) , (AssemblyMorphism≡ _ _ (funExt (λ d → refl)))) + (λ !' → isProp× (isSetAssemblyMorphism _ _ p (!' ⊚ pullbackPr₁)) (isSetAssemblyMorphism _ _ q (!' ⊚ pullbackPr₂))) + λ { !' (p≡!'*pr₁ , q≡!'*pr₂) → + AssemblyMorphism≡ + _ _ + (funExt + λ d → + ΣPathP + ((λ i → p≡!'*pr₁ i .map d) , + ΣPathPProp + {u = q .map d , λ i → pf≡qg i .map d} + {v = !' .map d .snd} + (λ z → ys .isSetX _ _) + λ i → q≡!'*pr₂ i .map d)) } + where + uniqueMap : D → pullbackType + uniqueMap d = p .map d , q .map d , λ i → pf≡qg i .map d + + uniqueMorphism : AssemblyMorphism ds pullbackAsm + uniqueMorphism = + (makeAssemblyMorphism + uniqueMap + (do + (p~ , isTrackedP) ← p .tracker + (q~ , isTrackedQ) ← q .tracker + let + realizer : Term as 1 + realizer = ` pair ̇ (` p~ ̇ # zero) ̇ (` q~ ̇ # zero) + return + (λ* realizer , + λ d r r⊩d → + subst (λ r' → r' ⊩[ xs ] (p .map d)) (sym (cong (λ x → pr₁ ⨾ x) (λ*ComputationRule realizer r) ∙ pr₁pxy≡x _ _)) (isTrackedP d r r⊩d) , + subst (λ r' → r' ⊩[ zs ] (q .map d)) (sym (cong (λ x → pr₂ ⨾ x) (λ*ComputationRule realizer r) ∙ pr₂pxy≡y _ _)) (isTrackedQ d r r⊩d)))) + +PullbacksASM : Pullbacks ASM +PullbacksASM cspn = pullback cspn + +-- Using pullbacks we get a functor that sends any f : X → Y to f* : Asm / Y → Asm / X +module _ {X Y : Type ℓ} (asmX : Assembly X) (asmY : Assembly Y) (f : AssemblyMorphism asmX asmY) where + open Pullback + opaque + unfolding pullbackAsm + unfolding pullbackPr₁ + unfolding pullback + pullbackFunctor : Functor (SliceCat ASM (Y , asmY)) (SliceCat ASM (X , asmX)) + Functor.F-ob pullbackFunctor sliceY = sliceob (pullback (cospan (X , asmX) (Y , asmY) (sliceY .S-ob) f (sliceY .S-arr)) .pbPr₁) + Functor.F-hom pullbackFunctor {ySliceA} {ySliceB} sliceHomAB = + let + sliceACospan : Cospan ASM + sliceACospan = cospan (X , asmX) (Y , asmY) (ySliceA .S-ob) f (ySliceA .S-arr) + p = pullbackPr₂ sliceACospan + m = ySliceA .S-arr + n = ySliceB .S-arr + f*m = pullbackPr₁ sliceACospan + h = sliceHomAB .S-hom + m≡h⊚n = sliceHomAB .S-comm + f*m⊚f≡p⊚m = pbCommutes (pullback sliceACospan) + arrow = + pullbackArrow + ASM + (pullback (cospan (X , asmX) (Y , asmY) (ySliceB .S-ob) f (ySliceB .S-arr))) (pullbackPr₁ sliceACospan) (p ⊚ h) + (AssemblyMorphism≡ _ _ + (funExt + λ { (x , a , fx≡ma) → + f .map x + ≡⟨ fx≡ma ⟩ + m .map a + ≡[ i ]⟨ m≡h⊚n (~ i) .map a ⟩ + n .map (h .map a) + ∎ })) + in + slicehom + arrow + {!!} + Functor.F-id pullbackFunctor = {!!} + Functor.F-seq pullbackFunctor = {!!} diff --git a/src/Realizability/Assembly/SetsReflectiveSubcategory.agda b/src/Realizability/Assembly/SetsReflectiveSubcategory.agda new file mode 100644 index 0000000..8a2f295 --- /dev/null +++ b/src/Realizability/Assembly/SetsReflectiveSubcategory.agda @@ -0,0 +1,62 @@ +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.Data.Sigma +open import Cubical.Data.FinData +open import Cubical.Data.Unit +open import Cubical.HITs.PropositionalTruncation hiding (map) +open import Cubical.HITs.PropositionalTruncation.Monad +open import Cubical.Reflection.RecordEquiv +open import Cubical.Categories.Category +open import Cubical.Categories.Functor +open import Cubical.Categories.Instances.Sets +open import Cubical.Categories.Adjoint +open import Cubical.Categories.NaturalTransformation +open import Realizability.CombinatoryAlgebra +open import Realizability.ApplicativeStructure + +module Realizability.Assembly.SetsReflectiveSubcategory {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) where + +open import Realizability.Assembly.Base ca +open import Realizability.Assembly.Morphism ca + +open Assembly +open CombinatoryAlgebra ca +open Realizability.CombinatoryAlgebra.Combinators ca renaming (i to Id; ia≡a to Ida≡a) + +forgetfulFunctor : Functor ASM (SET ℓ) +Functor.F-ob forgetfulFunctor (X , asmX) = X , asmX .isSetX +Functor.F-hom forgetfulFunctor {X , asmX} {Y , asmY} f = f .map +Functor.F-id forgetfulFunctor = refl +Functor.F-seq forgetfulFunctor {X , asmX} {Y , asmY} {Z , asmZ} f g = refl + +∇ : Functor (SET ℓ) ASM +Functor.F-ob ∇ (X , isSetX) = X , makeAssembly (λ a x → Unit*) isSetX (λ _ _ → isPropUnit*) λ x → ∣ k , tt* ∣₁ +Functor.F-hom ∇ {X , isSetX} {Y , isSetY} f = makeAssemblyMorphism f (return (k , (λ _ _ _ → tt*))) +Functor.F-id ∇ {X , isSetX} = AssemblyMorphism≡ _ _ refl +Functor.F-seq ∇ {X , isSetX} {Y , isSetY} {Z , isSetZ} f g = AssemblyMorphism≡ _ _ refl + +module _ where + open UnitCounit + + adjointUnitCounit : forgetfulFunctor ⊣ ∇ + NatTrans.N-ob (_⊣_.η adjointUnitCounit) (X , asmX) = makeAssemblyMorphism (λ x → x) (return (k , (λ _ _ _ → tt*))) + NatTrans.N-hom (_⊣_.η adjointUnitCounit) {X , asmX} {Y , asmY} f = AssemblyMorphism≡ _ _ refl + NatTrans.N-ob (_⊣_.ε adjointUnitCounit) (X , isSetX) x = x + NatTrans.N-hom (_⊣_.ε adjointUnitCounit) {X , isSetX} {Y , isSetY} f = refl + TriangleIdentities.Δ₁ (_⊣_.triangleIdentities adjointUnitCounit) (X , asmX) = refl + TriangleIdentities.Δ₂ (_⊣_.triangleIdentities adjointUnitCounit) (X , isSetX) = AssemblyMorphism≡ _ _ refl + +module _ where + open NaturalBijection + + adjointNaturalBijection : forgetfulFunctor ⊣ ∇ + Iso.fun (_⊣_.adjIso adjointNaturalBijection) f = makeAssemblyMorphism f (return (k , (λ x r r⊩x → tt*))) + Iso.inv (_⊣_.adjIso adjointNaturalBijection) f = f .map + Iso.rightInv (_⊣_.adjIso adjointNaturalBijection) b = AssemblyMorphism≡ _ _ refl + Iso.leftInv (_⊣_.adjIso adjointNaturalBijection) a = refl + _⊣_.adjNatInD adjointNaturalBijection {X , isSetX} {Y , isSetY} f g = AssemblyMorphism≡ _ _ refl + _⊣_.adjNatInC adjointNaturalBijection {X , asmX} {Y , asmY} f g = refl + diff --git a/src/Realizability/Assembly/Terminal.agda b/src/Realizability/Assembly/Terminal.agda new file mode 100644 index 0000000..64fb1c6 --- /dev/null +++ b/src/Realizability/Assembly/Terminal.agda @@ -0,0 +1,49 @@ +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.HLevels +open import Cubical.Data.Sigma +open import Cubical.Data.FinData +open import Cubical.Data.Unit +open import Cubical.HITs.PropositionalTruncation hiding (map) +open import Cubical.HITs.PropositionalTruncation.Monad +open import Cubical.Categories.Limits.Terminal +open import Realizability.CombinatoryAlgebra +open import Realizability.ApplicativeStructure + +module Realizability.Assembly.Terminal {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) where + +open Realizability.CombinatoryAlgebra.Combinators ca renaming (i to Id; ia≡a to Ida≡a) +open import Realizability.Assembly.Base ca +open import Realizability.Assembly.Morphism ca +open CombinatoryAlgebra ca +open Assembly +open AssemblyMorphism + +terminalAsm : Assembly Unit* +(Assembly._⊩_ terminalAsm) a tt* = Unit* +Assembly.isSetX terminalAsm = isSetUnit* +(Assembly.⊩isPropValued terminalAsm) a tt* = isPropUnit* +Assembly.⊩surjective terminalAsm tt* = ∣ k , tt* ∣₁ + +isTerminalTerminalAsm : isTerminal ASM (Unit* , terminalAsm) +isTerminalTerminalAsm (X , asmX) = + inhProp→isContr + (makeAssemblyMorphism + (λ x → tt*) + (return + (k , (λ x r r⊩x → tt*)))) + (λ f g → + AssemblyMorphism≡ _ _ (funExt λ x → refl)) + +TerminalASM : Terminal ASM +fst TerminalASM = Unit* , terminalAsm +snd TerminalASM = isTerminalTerminalAsm + +-- global element +module _ {X : Type ℓ} (asmX : Assembly X) (x : X) (r : A) (r⊩x : r ⊩[ asmX ] x) where + + globalElement : AssemblyMorphism terminalAsm asmX + AssemblyMorphism.map globalElement tt* = x + AssemblyMorphism.tracker globalElement = + return + ((k ⨾ r) , + (λ { tt* a tt* → subst (λ r' → r' ⊩[ asmX ] x) (sym (kab≡a _ _)) r⊩x })) diff --git a/src/Realizability/Modest/Base.agda b/src/Realizability/Modest/Base.agda new file mode 100644 index 0000000..e2e9b1c --- /dev/null +++ b/src/Realizability/Modest/Base.agda @@ -0,0 +1,78 @@ +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.Structure using (⟨_⟩; str) +open import Cubical.Data.Sigma +open import Cubical.Data.FinData +open import Cubical.HITs.PropositionalTruncation hiding (map) +open import Cubical.HITs.PropositionalTruncation.Monad +open import Cubical.Reflection.RecordEquiv +open import Cubical.Categories.Category +open import Realizability.CombinatoryAlgebra +open import Realizability.ApplicativeStructure +open import Realizability.PropResizing + +module Realizability.Modest.Base {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) where + +open import Realizability.Assembly.Base ca +open import Realizability.Assembly.Morphism ca + +open Assembly +open CombinatoryAlgebra ca +open Realizability.CombinatoryAlgebra.Combinators ca renaming (i to Id; ia≡a to Ida≡a) + +module _ {X : Type ℓ} (asmX : Assembly X) where + + isModest : Type _ + isModest = ∀ (x y : X) (a : A) → a ⊩[ asmX ] x → a ⊩[ asmX ] y → x ≡ y + + 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) + +ModestSet : Type ℓ → Type (ℓ-suc ℓ) +ModestSet X = Σ[ xs ∈ Assembly X ] isModest xs + +MOD : Category (ℓ-suc ℓ) ℓ +MOD = ΣPropCat ASM λ { (X , asmX) → (Lift (isModest asmX)) , (isOfHLevelRespectEquiv 1 (LiftEquiv {A = isModest asmX}) (isPropIsModest asmX)) } + +-- Every modest set is isomorphic to a canonically modest set +module Canonical (X : Type ℓ) (asmX : Assembly X) (isModestAsmX : isModest asmX) (resizing : hPropResizing ℓ) where + open ResizedPowerset resizing + -- Replace every term of X by it's set of realisers + realisersOf : X → ℙ A + realisersOf x a = (a ⊩[ asmX ] x) , (asmX .⊩isPropValued a x) + + resizedRealisersOf : X → 𝓟 A + resizedRealisersOf x = ℙ→𝓟 A (realisersOf x) + + realiserSet : Type ℓ + realiserSet = Σ[ P ∈ 𝓟 A ] ∃[ x ∈ X ] P ≡ resizedRealisersOf x + + canonicalModestSet : Assembly realiserSet + Assembly._⊩_ canonicalModestSet r (P , ∃x) = r ϵ P + Assembly.isSetX canonicalModestSet = isSetΣ (isSet𝓟 A) (λ P → isProp→isSet isPropPropTrunc) + Assembly.⊩isPropValued canonicalModestSet r (P , ∃x) = isPropϵ r P + Assembly.⊩surjective canonicalModestSet (P , ∃x) = + do + (x , P≡⊩x) ← ∃x + (a , a⊩x) ← asmX .⊩surjective x + return + (a , + (subst + (λ P → a ϵ P) + (sym P≡⊩x) + (subst (λ P → a ∈ P) (sym (compIsIdFunc (realisersOf x))) a⊩x))) + {- + isModestCanonicalModestSet : isModest canonicalModestSet + isModestCanonicalModestSet x y a a⊩x a⊩y = + Σ≡Prop + (λ _ → isPropPropTrunc) + (𝓟≡ (x .fst) (y .fst) (⊆-extensionality (𝓟→ℙ A (x .fst)) (𝓟→ℙ A (y .fst)) ((λ b b⊩x → {!!}) , {!!}))) -} + + diff --git a/src/Realizability/Modest/FamilyOverAsm.agda b/src/Realizability/Modest/FamilyOverAsm.agda new file mode 100644 index 0000000..07acadf --- /dev/null +++ b/src/Realizability/Modest/FamilyOverAsm.agda @@ -0,0 +1,63 @@ +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.Structure using (⟨_⟩; str) +open import Cubical.Data.Sigma +open import Cubical.Data.FinData +open import Cubical.Data.Unit +open import Cubical.HITs.PropositionalTruncation hiding (map) +open import Cubical.HITs.PropositionalTruncation.Monad +open import Cubical.Reflection.RecordEquiv +open import Cubical.Categories.Category +open import Cubical.Categories.Displayed.Base +open import Cubical.Categories.Limits.Pullback +open import Realizability.CombinatoryAlgebra +open import Realizability.ApplicativeStructure +open import Realizability.PropResizing + +module Realizability.Modest.FamilyOverAsm {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) where + +open import Realizability.Assembly.Base ca +open import Realizability.Assembly.Morphism ca +open import Realizability.Assembly.Pullbacks ca +open import Realizability.Assembly.Terminal ca +open import Realizability.Modest.Base ca + +open Assembly +open CombinatoryAlgebra ca +open Realizability.CombinatoryAlgebra.Combinators ca renaming (i to Id; ia≡a to Ida≡a) +open Pullback + +module _ {X : Type ℓ} (asmX : Assembly X) (Y : Type ℓ) (asmY : Assembly Y) where + record FamilyOver : Type (ℓ-suc ℓ) where + no-eta-equality + constructor makeFamilyOver + field + fibration : AssemblyMorphism asmY asmX + {- + A[x] ------> A + |_| | + | | + | | fibration + | | + ↓ ↓ + 1 --------> X + x + + For any x the fiber over x is modest + -} + fiberOver : + ∀ (x : X) (a : A) → (a⊩x : a ⊩[ asmX ] x) → + Pullback + ASM + (cospan + (Unit* , terminalAsm) + (X , asmX) + (Y , asmY) + (globalElement asmX x a a⊩x) + fibration) + isModestFibreOver : ∀ (x : X) (a : A) (a⊩x : a ⊩[ asmX ] x) → isModest (fiberOver x a a⊩x .pbOb .snd) + diff --git a/src/Realizability/Modest/PartialSurjection.agda b/src/Realizability/Modest/PartialSurjection.agda new file mode 100644 index 0000000..7fb7aac --- /dev/null +++ b/src/Realizability/Modest/PartialSurjection.agda @@ -0,0 +1,150 @@ +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.Structure using (⟨_⟩; str) +open import Cubical.Foundations.Univalence +open import Cubical.Functions.Surjection +open import Cubical.Functions.FunExtEquiv +open import Cubical.Data.Sigma +open import Cubical.Data.FinData +open import Cubical.HITs.PropositionalTruncation as PT hiding (map) +open import Cubical.HITs.PropositionalTruncation.Monad +open import Cubical.Reflection.RecordEquiv +open import Cubical.Categories.Category +open import Realizability.CombinatoryAlgebra +open import Realizability.ApplicativeStructure +open import Realizability.PropResizing + +module Realizability.Modest.PartialSurjection {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) (resizing : hPropResizing ℓ) where + +open import Realizability.Assembly.Base ca +open import Realizability.Assembly.Morphism ca +open import Realizability.Modest.Base ca resizing + +open Assembly +open CombinatoryAlgebra ca +open Realizability.CombinatoryAlgebra.Combinators ca renaming (i to Id; ia≡a to Ida≡a) +open ResizedPowerset resizing + +record PartialSurjection (X : Type ℓ) : Type (ℓ-suc ℓ) where + no-eta-equality + constructor makePartialSurjection + field + support : A → Type ℓ + enumeration : Σ[ a ∈ A ] (support a) → X + isPropSupport : ∀ a → isProp (support a) + isSurjectionEnumeration : isSurjection enumeration + isSetX : isSet X -- potentially redundant? +open PartialSurjection + +-- let us derive a structure of identity principle for partial surjections +module _ (X : Type ℓ) where + + PartialSurjection≡Iso : + ∀ (p q : PartialSurjection X) + → Iso + (Σ[ suppPath ∈ p .support ≡ q .support ] + PathP (λ i → Σ[ a ∈ A ] (suppPath i a) → X) (p .enumeration) (q .enumeration)) + (p ≡ q) + support (Iso.fun (PartialSurjection≡Iso p q) (suppPath , enumPath) i) z = suppPath i z + enumeration (Iso.fun (PartialSurjection≡Iso p q) (suppPath , enumPath) i) (a , enum) = enumPath i (a , enum) + isPropSupport (Iso.fun (PartialSurjection≡Iso p q) (suppPath , enumPath) i) z = + isProp→PathP {B = λ j → isProp (suppPath j z)} (λ j → isPropIsProp) (p .isPropSupport z) (q .isPropSupport z) i + isSurjectionEnumeration (Iso.fun (PartialSurjection≡Iso p q) (suppPath , enumPath) i) b = + isProp→PathP + {B = λ j → ∥ fiber (enumeration (Iso.fun (PartialSurjection≡Iso p q) (suppPath , enumPath) j)) b ∥₁} + (λ j → isPropPropTrunc) + (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.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 + + {-# 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 + in fst answer + isPropSupport (ModestSet→PartialSurjection (xs , isModestXs)) r = isPropPropTrunc + isSurjectionEnumeration (ModestSet→PartialSurjection (xs , isModestXs)) x = + do + (a , a⊩x) ← xs .⊩surjective x + return ((a , ∣ x , a⊩x ∣₁) , refl) + isSetX (ModestSet→PartialSurjection (xs , isModestXs)) = xs .isSetX + + PartialSurjection→ModestSet : PartialSurjection X → ModestSet X + Assembly._⊩_ (fst (PartialSurjection→ModestSet surj)) r x = + Σ[ s ∈ surj .support r ] surj .enumeration (r , s) ≡ x + Assembly.isSetX (fst (PartialSurjection→ModestSet surj)) = surj .isSetX + Assembly.⊩isPropValued (fst (PartialSurjection→ModestSet surj)) a x (s , ≡x) (t , ≡x') = + Σ≡Prop (λ u → surj .isSetX (surj .enumeration (a , u)) x) (surj .isPropSupport a s t) + Assembly.⊩surjective (fst (PartialSurjection→ModestSet surj)) x = + do + ((a , s) , ≡x) ← surj .isSurjectionEnumeration x + return (a , (s , ≡x)) + snd (PartialSurjection→ModestSet surj) x y r (s , ≡x) (t , ≡x') = + x + ≡⟨ sym ≡x ⟩ + surj .enumeration (r , s) + ≡⟨ cong (λ s → surj .enumeration (r , s)) (surj .isPropSupport r s t) ⟩ + surj .enumeration (r , t) + ≡⟨ ≡x' ⟩ + y + ∎ + + opaque + rightInv : ∀ surj → ModestSet→PartialSurjection (PartialSurjection→ModestSet surj) ≡ surj + rightInv surj = + PartialSurjection≡ + X (ModestSet→PartialSurjection (PartialSurjection→ModestSet surj)) surj + (funExt supportEq , + funExtDep + {A = λ i → Σ-syntax A (funExt supportEq i)} + {B = λ _ _ → X} + {f = ModestSet→PartialSurjection (PartialSurjection→ModestSet surj) .enumeration} + {g = surj .enumeration} + λ { {r , ∃x} {s , supp} p → + PT.elim + {P = λ ∃x → fst + (PT.rec + (isUniqueRealised (fst (PartialSurjection→ModestSet surj)) + (snd (PartialSurjection→ModestSet surj)) r) + (λ t → t) ∃x) + ≡ surj .enumeration (s , supp)} + (λ ∃x → surj .isSetX _ _) + (λ { (x , r⊩x) → + let + ∃x' = transport (sym (supportEq s)) supp + in + equivFun + (propTruncIdempotent≃ {!!}) + (do + (x' , suppS , ≡x') ← ∃x' + return {!!}) }) + ∃x }) where + supportEq : ∀ r → (∃[ x ∈ X ] (Σ[ supp ∈ surj .support r ] (surj .enumeration (r , supp) ≡ x))) ≡ support surj r + supportEq = + (λ r → + hPropExt + isPropPropTrunc + (surj .isPropSupport r) + (λ ∃x → PT.rec (surj .isPropSupport r) (λ { (x , supp , ≡x) → supp }) ∃x) + (λ supp → return (surj .enumeration (r , supp) , supp , 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 = {!!} diff --git a/src/Realizability/PERs/#TerminalObject.agda# b/src/Realizability/PERs/#TerminalObject.agda# new file mode 100644 index 0000000..b573343 --- /dev/null +++ b/src/Realizability/PERs/#TerminalObject.agda# @@ -0,0 +1,43 @@ +open import Realizability.ApplicativeStructure +open import Realizability.CombinatoryAlgebra +open import Realizability.PropResizing +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Structure using (⟨_⟩; str) +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Univalence +open import Cubical.Foundations.Powerset +open import Cubical.Functions.FunExtEquiv +open import Cubical.Relation.Binary +open import Cubical.Data.Sigma +open import Cubical.Data.FinData +open import Cubical.Data.Unit +open import Cubical.Reflection.RecordEquiv +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.Categories.Category +open import Cubical.Categories.Limits.Terminal + +module Realizability.PERs.TerminalObject + {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) where + +open import Realizability.PERs.PER ca +open CombinatoryAlgebra ca +open Combinators ca renaming (i to Id; ia≡a to Ida≡a) +open PERMorphism + +terminalPER : PER +PER.relation terminalPER = (λ x y → Unit*) , λ x y → isPropUnit* +fst (PER.isPER terminalPER) = λ a b x → tt* +snd (PER.isPER terminalPER) = λ a b c x x₁ → tt* + +isTerminalTerminalPER : isTerminal PERCat terminalPER +isTerminalTerminalPER X = + inhProp→isContr + (makePERMorphism (λ x → [ k ]) (return (Id , (λ a aXa → (eq/ k (Id ⨾ a) tt*) , tt*)))) + λ x y → PERMorphism≡ x y (funExt λ q → {!effectiveOnDomain!}) + +terminal : Terminal PERCat +terminal = terminalPER , {!!} diff --git a/src/Realizability/PERs/.#TerminalObject.agda b/src/Realizability/PERs/.#TerminalObject.agda new file mode 120000 index 0000000..53126fa --- /dev/null +++ b/src/Realizability/PERs/.#TerminalObject.agda @@ -0,0 +1 @@ +rahul@Rahuls-MacBook-Air.local.1114:1710392191 \ No newline at end of file diff --git a/src/Realizability/PERs/PER.agda b/src/Realizability/PERs/PER.agda index 38bcb96..bd5adb7 100644 --- a/src/Realizability/PERs/PER.agda +++ b/src/Realizability/PERs/PER.agda @@ -17,10 +17,14 @@ 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.Categories.Category +open import Cubical.Categories.Functor hiding (Id) module Realizability.PERs.PER {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) where +open import Realizability.Assembly.Base ca +open import Realizability.Assembly.Morphism ca + open CombinatoryAlgebra ca open Combinators ca renaming (i to Id; ia≡a to Ida≡a) @@ -158,3 +162,16 @@ Category.⋆IdL PERCat f = idLPERMorphism f Category.⋆IdR PERCat f = idRPERMorphism f Category.⋆Assoc PERCat f g h = assocPERMorphism f g h Category.isSetHom PERCat = isSetPERMorphism + +open Assembly + +inclusion : Functor PERCat ASM +fst (Functor.F-ob inclusion per) = Σ[ a ∈ A ] ∣ per ∣ a a +(snd (Functor.F-ob inclusion per)) ._⊩_ r (a , aRa) = ∣ per ∣ r a +isSetX (snd (Functor.F-ob inclusion per)) = isSetΣ isSetA (λ x → isProp→isSet (isPropValued per x x)) +⊩isPropValued (snd (Functor.F-ob inclusion per)) r (a , aRa) = isPropValued per r a +⊩surjective (snd (Functor.F-ob inclusion per)) (a , aRa) = return (a , aRa) +AssemblyMorphism.map (Functor.F-hom inclusion morphism) (a , aRa) = {!!} +AssemblyMorphism.tracker (Functor.F-hom inclusion morphism) = {!!} +Functor.F-id inclusion = {!!} +Functor.F-seq inclusion = {!!} diff --git a/src/Realizability/PERs/TerminalObject.agda b/src/Realizability/PERs/TerminalObject.agda new file mode 100644 index 0000000..c3a6576 --- /dev/null +++ b/src/Realizability/PERs/TerminalObject.agda @@ -0,0 +1,43 @@ +open import Realizability.ApplicativeStructure +open import Realizability.CombinatoryAlgebra +open import Realizability.PropResizing +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Structure using (⟨_⟩; str) +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Univalence +open import Cubical.Foundations.Powerset +open import Cubical.Functions.FunExtEquiv +open import Cubical.Relation.Binary +open import Cubical.Data.Sigma +open import Cubical.Data.FinData +open import Cubical.Data.Unit +open import Cubical.Reflection.RecordEquiv +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.Categories.Category +open import Cubical.Categories.Limits.Terminal + +module Realizability.PERs.TerminalObject + {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) where + +open import Realizability.PERs.PER ca +open CombinatoryAlgebra ca +open Combinators ca renaming (i to Id; ia≡a to Ida≡a) +open PERMorphism + +terminalPER : PER +PER.relation terminalPER = (λ x y → Unit*) , λ x y → isPropUnit* +fst (PER.isPER terminalPER) = λ a b x → tt* +snd (PER.isPER terminalPER) = λ a b c x x₁ → tt* + +isTerminalTerminalPER : isTerminal PERCat terminalPER +isTerminalTerminalPER X = + inhProp→isContr + (makePERMorphism (λ x → [ k ]) (return (Id , (λ a aXa → (eq/ k (Id ⨾ a) tt*) , tt*)))) + λ x y → PERMorphism≡ x y (funExt λ q → {!!}) + +terminal : Terminal PERCat +terminal = terminalPER , {!!} diff --git a/src/Realizability/PropResizing.agda b/src/Realizability/PropResizing.agda index 5ba4076..1063210 100644 --- a/src/Realizability/PropResizing.agda +++ b/src/Realizability/PropResizing.agda @@ -1,7 +1,9 @@ open import Cubical.Foundations.Prelude open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Equiv.Properties open import Cubical.Foundations.HLevels open import Cubical.Foundations.Structure +open import Cubical.Foundations.Powerset open import Cubical.Data.Sigma module Realizability.PropResizing where @@ -21,3 +23,55 @@ copyEquiv = snd -- This we call hPropResizing hPropResizing : ∀ ℓ → Type _ hPropResizing ℓ = copyOf (hProp ℓ) ℓ + +-- We obtain a copy of the powerset using hPropResizing +module ResizedPowerset {ℓ} (resizing : hPropResizing ℓ) where + + smallHProp = resizing .fst + hProp≃smallHProp = resizing .snd + smallHProp≃hProp = invEquiv hProp≃smallHProp + + 𝓟 : Type ℓ → Type ℓ + 𝓟 X = X → smallHProp + + ℙ≃𝓟 : ∀ X → ℙ X ≃ 𝓟 X + ℙ≃𝓟 X = + ℙ X + ≃⟨ idEquiv (ℙ X) ⟩ + (X → hProp ℓ) + ≃⟨ equiv→ (idEquiv X) hProp≃smallHProp ⟩ + (X → smallHProp) + ≃⟨ idEquiv (𝓟 X) ⟩ + 𝓟 X + ■ + + 𝓟≃ℙ : ∀ X → 𝓟 X ≃ ℙ X + 𝓟≃ℙ X = invEquiv (ℙ≃𝓟 X) + + ℙ→𝓟 : ∀ X → ℙ X → 𝓟 X + ℙ→𝓟 X = equivFun (ℙ≃𝓟 X) + + 𝓟→ℙ : ∀ X → 𝓟 X → ℙ X + 𝓟→ℙ X = equivFun (invEquiv (ℙ≃𝓟 X)) + + compIsIdEquiv : ∀ X → compEquiv (ℙ≃𝓟 X) (invEquiv (ℙ≃𝓟 X)) ≡ idEquiv (ℙ X) + compIsIdEquiv X = invEquiv-is-rinv (ℙ≃𝓟 X) + + compIsIdFunc : ∀ {X} (p : ℙ X) → 𝓟→ℙ X (ℙ→𝓟 X p) ≡ p + compIsIdFunc {X} p i = equivFun (compIsIdEquiv X i) p + + _ϵ_ : ∀ {X} → X → 𝓟 X → Type ℓ + _ϵ_ {X} x P = x ∈ 𝓟→ℙ X P + + isPropϵ : ∀ {X} (x : X) P → isProp (x ϵ P) + isPropϵ {X} x P = ∈-isProp (𝓟→ℙ X P) x + + isSet𝓟 : ∀ X → isSet (𝓟 X) + isSet𝓟 X = isOfHLevelRespectEquiv 2 (ℙ≃𝓟 X) isSetℙ + + 𝓟≡Equiv : ∀ {X} (P Q : 𝓟 X) → (P ≡ Q) ≃ (𝓟→ℙ X P ≡ 𝓟→ℙ X Q) + 𝓟≡Equiv {X} P Q = congEquiv {x = P} {y = Q} (𝓟≃ℙ X) + + 𝓟≡ : ∀ {X} (P Q : 𝓟 X) → 𝓟→ℙ X P ≡ 𝓟→ℙ X Q → P ≡ Q + 𝓟≡ {X} P Q equ = equivFun (invEquiv (𝓟≡Equiv P Q)) equ +