From 73d04b5d95afbc6742a07a4b8359e1d893a05be8 Mon Sep 17 00:00:00 2001 From: Rahul Chhabra Date: Wed, 26 Jun 2024 22:02:10 +0530 Subject: [PATCH] Families of modest sets as displayed category --- src/Realizability/Modest/UniformFamily.agda | 220 +++++++++++++++--- src/Realizability/PERs/PER.agda | 7 +- src/Realizability/PERs/ResizedPER.agda | 91 ++++++++ src/Realizability/PERs/SystemF.agda | 6 + .../PERs/UniformFamiliesOverAsm.agda | 78 +++++++ 5 files changed, 362 insertions(+), 40 deletions(-) create mode 100644 src/Realizability/PERs/ResizedPER.agda create mode 100644 src/Realizability/PERs/UniformFamiliesOverAsm.agda diff --git a/src/Realizability/Modest/UniformFamily.agda b/src/Realizability/Modest/UniformFamily.agda index 805446a..d2aa9aa 100644 --- a/src/Realizability/Modest/UniformFamily.agda +++ b/src/Realizability/Modest/UniformFamily.agda @@ -4,6 +4,7 @@ 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 @@ -13,8 +14,9 @@ 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.Displayed.Reasoning open import Cubical.Categories.Limits.Pullback -open import Cubical.Categories.Functor +open import Cubical.Categories.Functor hiding (Id) open import Cubical.Categories.Constructions.Slice open import Realizability.CombinatoryAlgebra open import Realizability.ApplicativeStructure @@ -22,50 +24,194 @@ open import Realizability.PropResizing module Realizability.Modest.UniformFamily {ℓ} {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.LocallyCartesianClosed 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) -UNIMOD : Categoryᴰ ASM (ℓ-suc ℓ) ℓ -Categoryᴰ.ob[ UNIMOD ] (X , asmX) = Σ[ Y ∈ Type ℓ ] Σ[ asmY ∈ Assembly Y ] isModest asmY × AssemblyMorphism asmY asmX -Categoryᴰ.Hom[_][_,_] UNIMOD {X , asmX} {Y , asmY} reindex (V , asmV , isModestAsmV , m) (W , asmW , isModestAsmW , n) = Σ[ reindexᵈ ∈ (AssemblyMorphism asmV asmW) ] m ⊚ reindex ≡ reindexᵈ ⊚ n -Categoryᴰ.idᴰ UNIMOD {X , asmX} {V , asmV , isModestAsmV , m} = (identityMorphism asmV) , (Category.⋆IdR ASM m ∙ sym (Category.⋆IdL ASM m)) -Categoryᴰ._⋆ᴰ_ UNIMOD - {X , asmX} {Y , asmY} {Z , asmZ} {f} {g} - {U , asmU , isModestU , m} {V , asmV , isModestV , n} {W , asmW , isModestW , o} - (fᵈ , fᵈcomm) (gᵈ , gᵈcomm) = - (fᵈ ⊚ gᵈ) , - (m ⊚ (f ⊚ g) - ≡⟨ sym (Category.⋆Assoc ASM m f g) ⟩ - (m ⊚ f) ⊚ g - ≡⟨ cong (λ x → x ⊚ g) fᵈcomm ⟩ - fᵈ ⊚ n ⊚ g - ≡⟨ Category.⋆Assoc ASM fᵈ n g ⟩ - fᵈ ⊚ (n ⊚ g) - ≡⟨ cong (fᵈ ⊚_) gᵈcomm ⟩ - fᵈ ⊚ (gᵈ ⊚ o) - ≡⟨ sym (Category.⋆Assoc ASM fᵈ gᵈ o) ⟩ - fᵈ ⊚ gᵈ ⊚ o - ∎) -Categoryᴰ.⋆IdLᴰ UNIMOD {X , asmX} {Y , asmY} {f} {V , asmV , isModestAsmV , m} {W , asmW , isModestAsmW , n} (fᵈ , fᵈcomm) = - ΣPathPProp (λ fᵈ → isSetAssemblyMorphism asmV asmY _ _) (Category.⋆IdL ASM fᵈ) -Categoryᴰ.⋆IdRᴰ UNIMOD {X , asmX} {Y , asmY} {f} {V , asmV , isModestAsmV , m} {W , asmW , isModestAsmW , n} (fᵈ , fᵈcomm) = - ΣPathPProp (λ fᵈ → isSetAssemblyMorphism asmV asmY _ _) (Category.⋆IdR ASM fᵈ) -Categoryᴰ.⋆Assocᴰ UNIMOD - {X , asmX} {Y , asmY} {Z , asmZ} {W , asmW} {f} {g} {h} - {Xᴰ , asmXᴰ , isModestAsmXᴰ , pX} {Yᴰ , asmYᴰ , isModestAsmYᴰ , pY} {Zᴰ , asmZᴰ , isModestAsmZᴰ , pZ} {Wᴰ , asmWᴰ , isModestAsmWᴰ , pW} - (fᵈ , fᵈcomm) (gᵈ , gᵈcomm) (hᵈ , hᵈcomm) = - ΣPathPProp (λ comp → isSetAssemblyMorphism asmXᴰ asmW _ _) (Category.⋆Assoc ASM fᵈ gᵈ hᵈ ) -Categoryᴰ.isSetHomᴰ UNIMOD = isSetΣ (isSetAssemblyMorphism _ _) (λ f → isProp→isSet (isSetAssemblyMorphism _ _ _ _)) +record UniformFamily {I : Type ℓ} (asmI : Assembly I) : Type (ℓ-suc ℓ) where + no-eta-equality + field + carriers : I → Type ℓ + assemblies : ∀ i → Assembly (carriers i) + isModestFamily : ∀ i → isModest (assemblies i) +open UniformFamily +record DisplayedUFamMap {I J : Type ℓ} (asmI : Assembly I) (asmJ : Assembly J) (u : AssemblyMorphism asmI asmJ) (X : UniformFamily asmI) (Y : UniformFamily asmJ) : Type ℓ where + no-eta-equality + field + fibrewiseMap : ∀ i → X .carriers i → Y .carriers (u .map i) + isTracked : ∃[ e ∈ A ] (∀ (i : I) (a : A) (a⊩i : a ⊩[ asmI ] i) (x : X .carriers i) (b : A) (b⊩x : b ⊩[ X .assemblies i ] x) → (e ⨾ a ⨾ b) ⊩[ Y .assemblies (u .map i) ] (fibrewiseMap i x)) + +open DisplayedUFamMap + +DisplayedUFamMapPathP : + ∀ {I J} (asmI : Assembly I) (asmJ : Assembly J) → + ∀ u v X Y + → (uᴰ : DisplayedUFamMap asmI asmJ u X Y) + → (vᴰ : DisplayedUFamMap asmI asmJ v X Y) + → (p : u ≡ v) + → (∀ (i : I) (x : X .carriers i) → PathP (λ j → Y .carriers (p j .map i)) (uᴰ .fibrewiseMap i x) (vᴰ .fibrewiseMap i x)) + ----------------------------------------------------------------------------------------------------------------------- + → PathP (λ i → DisplayedUFamMap asmI asmJ (p i) X Y) uᴰ vᴰ +fibrewiseMap (DisplayedUFamMapPathP {I} {J} asmI asmJ u v X Y uᴰ vᴰ p pᴰ dimI) i x = pᴰ i x dimI +isTracked (DisplayedUFamMapPathP {I} {J} asmI asmJ u v X Y uᴰ vᴰ p pᴰ dimI) = + isProp→PathP + {B = λ dimJ → ∃[ e ∈ A ] ((i : I) (a : A) → a ⊩[ asmI ] i → (x : X .carriers i) (b : A) → b ⊩[ X .assemblies i ] x → (e ⨾ a ⨾ b) ⊩[ Y .assemblies (p dimJ .map i) ] pᴰ i x dimJ)} + (λ dimJ → isPropPropTrunc) + (uᴰ .isTracked) + (vᴰ .isTracked) + dimI + +isSetDisplayedUFamMap : ∀ {I J} (asmI : Assembly I) (asmJ : Assembly J) → ∀ u X Y → isSet (DisplayedUFamMap asmI asmJ u X Y) +fibrewiseMap (isSetDisplayedUFamMap {I} {J} asmI asmJ u X Y f g p q dimI dimJ) i x = + isSet→isSet' + (Y .assemblies (u .map i) .isSetX) + {a₀₀ = fibrewiseMap f i x} + {a₀₁ = fibrewiseMap f i x} + refl + {a₁₀ = fibrewiseMap g i x} + {a₁₁ = fibrewiseMap g i x} + refl + (λ dimK → fibrewiseMap (p dimK) i x) + (λ dimK → fibrewiseMap (q dimK) i x) + dimJ dimI +isTracked (isSetDisplayedUFamMap {I} {J} asmI asmJ u X Y f g p q dimI dimJ) = + isProp→SquareP + {B = λ dimI dimJ → + ∃[ e ∈ A ] + ((i : I) (a : A) → + a ⊩[ asmI ] i → + (x : X .carriers i) (b : A) → + b ⊩[ X .assemblies i ] x → + (e ⨾ a ⨾ b) ⊩[ Y .assemblies (u .map i) ] + isSet→isSet' + (Y .assemblies + (u .map i) + .isSetX) + (λ _ → fibrewiseMap f i x) (λ _ → fibrewiseMap g i x) + (λ dimK → fibrewiseMap (p dimK) i x) + (λ dimK → fibrewiseMap (q dimK) i x) dimJ dimI)} + (λ dimI dimJ → isPropPropTrunc) + {a = isTracked f} + {b = isTracked g} + {c = isTracked f} + {d = isTracked g} + refl + refl + (λ dimK → isTracked (p dimK)) + (λ dimK → isTracked (q dimK)) + dimI dimJ -open Categoryᴰ UNIMOD +DisplayedUFamMapPathPIso : + ∀ {I J} (asmI : Assembly I) (asmJ : Assembly J) → + ∀ u v X Y + → (uᴰ : DisplayedUFamMap asmI asmJ u X Y) + → (vᴰ : DisplayedUFamMap asmI asmJ v X Y) + → (p : u ≡ v) + → Iso + (∀ (i : I) (x : X .carriers i) → PathP (λ dimI → Y .carriers (p dimI .map i)) (uᴰ .fibrewiseMap i x) (vᴰ .fibrewiseMap i x)) + (PathP (λ dimI → DisplayedUFamMap asmI asmJ (p dimI) X Y) uᴰ vᴰ) +Iso.fun (DisplayedUFamMapPathPIso {I} {J} asmI asmJ u v X Y uᴰ vᴰ p) pᴰ = DisplayedUFamMapPathP asmI asmJ u v X Y uᴰ vᴰ p pᴰ +Iso.inv (DisplayedUFamMapPathPIso {I} {J} asmI asmJ u v X Y uᴰ vᴰ p) uᴰ≡vᴰ i x dimI = (uᴰ≡vᴰ dimI) .fibrewiseMap i x +Iso.rightInv (DisplayedUFamMapPathPIso {I} {J} asmI asmJ u v X Y uᴰ vᴰ p) uᴰ≡vᴰ dimI dimJ = + isSet→SquareP + {A = λ dimK dimL → DisplayedUFamMap asmI asmJ (p dimL) X Y} + (λ dimI dimJ → isSetDisplayedUFamMap asmI asmJ (p dimJ) X Y) + {a₀₀ = uᴰ} + {a₀₁ = vᴰ} + (λ dimK → DisplayedUFamMapPathP asmI asmJ u v X Y uᴰ vᴰ p (λ i x dimL → uᴰ≡vᴰ dimL .fibrewiseMap i x) dimK) + {a₁₀ = uᴰ} + {a₁₁ = vᴰ} + uᴰ≡vᴰ + refl + refl dimI dimJ +Iso.leftInv (DisplayedUFamMapPathPIso {I} {J} asmI asmJ u v X Y uᴰ vᴰ p) pᴰ = refl -UniformFamily : {X : Type ℓ} → (asmX : Assembly X) → Type (ℓ-suc ℓ) -UniformFamily {X} asmX = UNIMOD .Categoryᴰ.ob[_] (X , asmX) +idDisplayedUFamMap : ∀ {I} (asmI : Assembly I) (p : UniformFamily asmI) → DisplayedUFamMap asmI asmI (identityMorphism asmI) p p +DisplayedUFamMap.fibrewiseMap (idDisplayedUFamMap {I} asmI p) i pi = pi +DisplayedUFamMap.isTracked (idDisplayedUFamMap {I} asmI p) = + return + (λ*2 realizer , + λ i a a⊩i x b b⊩x → + subst + (λ r → r ⊩[ p .assemblies i ] x) + (sym (λ*2ComputationRule realizer a b)) + b⊩x) where + realizer : Term as 2 + realizer = # zero + +module _ + {I J K : Type ℓ} + (asmI : Assembly I) + (asmJ : Assembly J) + (asmK : Assembly K) + (f : AssemblyMorphism asmI asmJ) + (g : AssemblyMorphism asmJ asmK) + (X : UniformFamily asmI) + (Y : UniformFamily asmJ) + (Z : UniformFamily asmK) + (fᴰ : DisplayedUFamMap asmI asmJ f X Y) + (gᴰ : DisplayedUFamMap asmJ asmK g Y Z) where + + composeDisplayedUFamMap : DisplayedUFamMap asmI asmK (f ⊚ g) X Z + DisplayedUFamMap.fibrewiseMap composeDisplayedUFamMap i Xi = gᴰ .fibrewiseMap (f .map i) (fᴰ .fibrewiseMap i Xi) + DisplayedUFamMap.isTracked composeDisplayedUFamMap = + do + (gᴰ~ , isTrackedGᴰ) ← gᴰ .isTracked + (fᴰ~ , isTrackedFᴰ) ← fᴰ .isTracked + (f~ , isTrackedF) ← f .tracker + let + realizer : Term as 2 + realizer = ` gᴰ~ ̇ (` f~ ̇ # one) ̇ (` fᴰ~ ̇ # one ̇ # zero) + return + (λ*2 realizer , + (λ i a a⊩i x b b⊩x → + subst + (_⊩[ Z .assemblies (g .map (f .map i)) ] _) + (sym (λ*2ComputationRule realizer a b)) + (isTrackedGᴰ (f .map i) (f~ ⨾ a) (isTrackedF i a a⊩i) (fᴰ .fibrewiseMap i x) (fᴰ~ ⨾ a ⨾ b) (isTrackedFᴰ i a a⊩i x b b⊩x)))) + +UNIMOD : Categoryᴰ ASM (ℓ-suc ℓ) ℓ +Categoryᴰ.ob[ UNIMOD ] (I , asmI) = UniformFamily asmI +Categoryᴰ.Hom[_][_,_] UNIMOD {I , asmI} {J , asmJ} u X Y = DisplayedUFamMap asmI asmJ u X Y +Categoryᴰ.idᴰ UNIMOD {I , asmI} {X} = idDisplayedUFamMap asmI X +Categoryᴰ._⋆ᴰ_ UNIMOD {I , asmI} {J , asmJ} {K , asmK} {f} {g} {X} {Y} {Z} fᴰ gᴰ = composeDisplayedUFamMap asmI asmJ asmK f g X Y Z fᴰ gᴰ +Categoryᴰ.⋆IdLᴰ UNIMOD {I , asmI} {J , asmJ} {f} {X} {Y} fᴰ = + DisplayedUFamMapPathP + asmI asmJ + (identityMorphism asmI ⊚ f) f + X Y + (composeDisplayedUFamMap asmI asmI asmJ (Category.id ASM) f X X Y (idDisplayedUFamMap asmI X) fᴰ) + fᴰ + (Category.⋆IdL ASM f) + (λ i x → refl) +Categoryᴰ.⋆IdRᴰ UNIMOD {I , asmI} {J , asmJ} {f} {X} {Y} fᴰ = + DisplayedUFamMapPathP + asmI asmJ + (f ⊚ identityMorphism asmJ) f + X Y + (composeDisplayedUFamMap asmI asmJ asmJ f (Category.id ASM) X Y Y fᴰ (idDisplayedUFamMap asmJ Y)) + fᴰ + (Category.⋆IdR ASM f) + λ i x → refl +Categoryᴰ.⋆Assocᴰ UNIMOD {I , asmI} {J , asmJ} {K , asmK} {L , asmL} {f} {g} {h} {X} {Y} {Z} {W} fᴰ gᴰ hᴰ = + DisplayedUFamMapPathP + asmI asmL + ((f ⊚ g) ⊚ h) (f ⊚ (g ⊚ h)) + X W + (composeDisplayedUFamMap + asmI asmK asmL + (f ⊚ g) h X Z W + (composeDisplayedUFamMap asmI asmJ asmK f g X Y Z fᴰ gᴰ) + hᴰ) + (composeDisplayedUFamMap + asmI asmJ asmL + f (g ⊚ h) X Y W + fᴰ (composeDisplayedUFamMap asmJ asmK asmL g h Y Z W gᴰ hᴰ)) + (Category.⋆Assoc ASM f g h) + λ i x → refl +Categoryᴰ.isSetHomᴰ UNIMOD {I , asmI} {J , asmJ} {f} {X} {Y} = isSetDisplayedUFamMap asmI asmJ f X Y diff --git a/src/Realizability/PERs/PER.agda b/src/Realizability/PERs/PER.agda index 90ca204..236b9b4 100644 --- a/src/Realizability/PERs/PER.agda +++ b/src/Realizability/PERs/PER.agda @@ -1,6 +1,5 @@ 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) @@ -70,8 +69,10 @@ isEquivTracker R S (a , _) (b , _) = (∀ r → r ~[ R ] r → (a ⨾ r) ~[ S ] isEquivRelIsEquivTracker : (R S : PER) → BR.isEquivRel (isEquivTracker R S) BinaryRelation.isEquivRel.reflexive (isEquivRelIsEquivTracker R S) (a , isTrackerA) r r~r = isTrackerA r r r~r -BinaryRelation.isEquivRel.symmetric (isEquivRelIsEquivTracker R S) (a , isTrackerA) (b , isTrackerB) a~b r r~r = isSymmetric S (a ⨾ r) (b ⨾ r) (a~b r r~r) -BinaryRelation.isEquivRel.transitive (isEquivRelIsEquivTracker R S) (a , isTrackerA) (b , isTrackerB) (c , isTrackerC) a~b b~c r r~r = isTransitive S (a ⨾ r) (b ⨾ r) (c ⨾ r) (a~b r r~r) (b~c r r~r) +BinaryRelation.isEquivRel.symmetric (isEquivRelIsEquivTracker R S) (a , isTrackerA) (b , isTrackerB) a~b r r~r = + isSymmetric S (a ⨾ r) (b ⨾ r) (a~b r r~r) +BinaryRelation.isEquivRel.transitive (isEquivRelIsEquivTracker R S) (a , isTrackerA) (b , isTrackerB) (c , isTrackerC) a~b b~c r r~r = + isTransitive S (a ⨾ r) (b ⨾ r) (c ⨾ r) (a~b r r~r) (b~c r r~r) isPropIsEquivTracker : ∀ R S a b → isProp (isEquivTracker R S a b) isPropIsEquivTracker R S (a , isTrackerA) (b , isTrackerB) = isPropΠ2 λ r r~r → isPropValued S (a ⨾ r) (b ⨾ r) diff --git a/src/Realizability/PERs/ResizedPER.agda b/src/Realizability/PERs/ResizedPER.agda new file mode 100644 index 0000000..4575301 --- /dev/null +++ b/src/Realizability/PERs/ResizedPER.agda @@ -0,0 +1,91 @@ +open import Realizability.ApplicativeStructure +open import Realizability.CombinatoryAlgebra +open import Realizability.PropResizing +open import Cubical.Foundations.Prelude +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.Foundations.HLevels +open import Cubical.Foundations.Equiv.HalfAdjoint +open import Cubical.Functions.FunExtEquiv +open import Cubical.Relation.Binary +open import Cubical.Data.Sigma +open import Cubical.Data.FinData +open import Cubical.Data.Vec +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.Functor hiding (Id) + +module Realizability.PERs.ResizedPER + {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) (resizing : hPropResizing ℓ) where + +open import Realizability.Assembly.Base ca +open import Realizability.Assembly.Morphism ca +open import Realizability.PERs.PER ca + +open CombinatoryAlgebra ca +open Combinators ca renaming (i to Id; ia≡a to Ida≡a) + +smallHProp = resizing .fst +hProp≃smallHProp = resizing .snd +smallHProp≃hProp = invEquiv hProp≃smallHProp + +hPropIsoSmallHProp : Iso (hProp ℓ) smallHProp +hPropIsoSmallHProp = equivToIso hProp≃smallHProp + +shrink : hProp ℓ → smallHProp +shrink = Iso.fun hPropIsoSmallHProp + +enlarge : smallHProp → hProp ℓ +enlarge = Iso.inv hPropIsoSmallHProp + +enlarge⋆shrink≡id : section shrink enlarge +enlarge⋆shrink≡id = Iso.rightInv hPropIsoSmallHProp + +shrink⋆enlarge≡id : retract shrink enlarge +shrink⋆enlarge≡id = Iso.leftInv hPropIsoSmallHProp + +extractType : smallHProp → Type ℓ +extractType p = ⟨ enlarge p ⟩ + +extractFromShrunk : ∀ p isPropP → extractType (shrink (p , isPropP)) ≡ p +extractFromShrunk p isPropP = + extractType (shrink (p , isPropP)) + ≡⟨ refl ⟩ + ⟨ enlarge (shrink (p , isPropP)) ⟩ + ≡⟨ cong ⟨_⟩ (shrink⋆enlarge≡id (p , isPropP)) ⟩ + p + ∎ + +record ResizedPER : Type ℓ where + no-eta-equality + constructor makeResizedPER + field + relation : A → A → smallHProp + isSymmetric : ∀ a b → extractType (relation a b) → extractType (relation b a) + isTransitive : ∀ a b c → extractType (relation a b) → extractType (relation b c) → extractType (relation a c) + +open ResizedPER + +ResizedPERHAEquivPER : HAEquiv ResizedPER PER +PER.relation (fst ResizedPERHAEquivPER resized) = + (λ a b → extractType (resized .relation a b)) , + λ a b → str (enlarge (resized .relation a b)) +fst (PER.isPER (fst ResizedPERHAEquivPER resized)) a b a~b = resized .isSymmetric a b a~b +snd (PER.isPER (fst ResizedPERHAEquivPER resized)) a b c a~b b~c = resized .isTransitive a b c a~b b~c +relation (isHAEquiv.g (snd ResizedPERHAEquivPER) per) a b = + shrink ((per .PER.relation .fst a b) , (per .PER.relation .snd a b)) +isSymmetric (isHAEquiv.g (snd ResizedPERHAEquivPER) per) a b a~b = + subst _ (sym (extractFromShrunk (per .PER.relation .fst b a) (per .PER.relation .snd b a))) {!per .PER.isPER .fst a b a~b!} +isTransitive (isHAEquiv.g (snd ResizedPERHAEquivPER) per) a b c a~b b~c = {!!} +isHAEquiv.linv (snd ResizedPERHAEquivPER) resized = {!!} +isHAEquiv.rinv (snd ResizedPERHAEquivPER) per = {!!} +isHAEquiv.com (snd ResizedPERHAEquivPER) resized = {!!} + +ResizedPER≃PER : ResizedPER ≃ PER +ResizedPER≃PER = ResizedPERHAEquivPER .fst , isHAEquiv→isEquiv (ResizedPERHAEquivPER .snd) diff --git a/src/Realizability/PERs/SystemF.agda b/src/Realizability/PERs/SystemF.agda index 70a186b..5bca5ba 100644 --- a/src/Realizability/PERs/SystemF.agda +++ b/src/Realizability/PERs/SystemF.agda @@ -33,6 +33,12 @@ module Syntax where Ren* : TypeCtxt → TypeCtxt → Type Ren* Γ Δ = ∀ {K} → K ∈* Γ → K ∈* Δ + lift* : ∀ {Γ Δ k} → Ren* Γ Δ → Ren* (Γ , k) (Δ , k) + lift* {Γ} {Δ} {k} ρ {.k} here = here + lift* {Γ} {Δ} {k} ρ {K} (there inm) = there (ρ inm) + + ren* : ∀ {Γ Δ} → + data _∈_ : ∀ {Γ} → Tp Γ tp → TermCtxt Γ → Type where here : ∀ {Γ} {A : Tp Γ tp} {Θ : TermCtxt Γ} → A ∈ (Θ , A) thereType : ∀ {Γ} {A B : Tp Γ tp} {Θ : TermCtxt Γ} → A ∈ Θ → A ∈ (Θ , B) diff --git a/src/Realizability/PERs/UniformFamiliesOverAsm.agda b/src/Realizability/PERs/UniformFamiliesOverAsm.agda new file mode 100644 index 0000000..5b9bf3f --- /dev/null +++ b/src/Realizability/PERs/UniformFamiliesOverAsm.agda @@ -0,0 +1,78 @@ +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.Displayed.Base + +module Realizability.PERs.UniformFamiliesOverAsm + {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) where + +open CombinatoryAlgebra ca +open Combinators ca renaming (i to Id; ia≡a to Ida≡a) +open import Realizability.PERs.PER ca +open import Realizability.Assembly.Base ca +open import Realizability.Assembly.Morphism ca + +module _ + {I J : Type ℓ} {asmI : Assembly I} {asmJ : Assembly J} (u : AssemblyMorphism asmI asmJ) (R : I → PER) (S : J → PER) where + + isDisplayedTracker : A → Type _ + isDisplayedTracker a = ∀ (i : I) (b : A) → b ⊩[ asmI ] i → isTracker (R i) (S (u .map i)) (a ⨾ b) + + isPropIsDisplayedTracker : ∀ a → isProp (isDisplayedTracker a) + isPropIsDisplayedTracker a = isPropΠ3 λ i b b⊩i → isPropΠ3 λ r r' r~r' → isProp~ _ (S (u .map i)) _ + + displayedTracker : Type _ + displayedTracker = Σ[ a ∈ A ] isDisplayedTracker a + + isSetDisplayedTracker : isSet displayedTracker + isSetDisplayedTracker = isSetΣ isSetA (λ a → isProp→isSet (isPropIsDisplayedTracker a)) + + isEquivDisplayedTracker : displayedTracker → displayedTracker → Type _ + isEquivDisplayedTracker (f , f⊩f) (g , g⊩g) = ∀ (i : I) (a : A) (a⊩i : a ⊩[ asmI ] i) → isEquivTracker (R i) (S (u .map i)) (f ⨾ a , f⊩f i a a⊩i) (g ⨾ a , g⊩g i a a⊩i) + + displayedPerMorphism : Type _ + displayedPerMorphism = displayedTracker / isEquivDisplayedTracker + +idDisplayedTracker : {I : Type ℓ} → (asmI : Assembly I) → (R : I → PER) → displayedTracker (identityMorphism asmI) R R +idDisplayedTracker {I} asmI R = λ*2 (# zero) , (λ i a a⊩i r r' r~r' → subst2 _~[ R i ]_ (sym (λ*2ComputationRule (# zero) a r)) (sym (λ*2ComputationRule (# zero) a r')) r~r' ) + +open Category ASM +module _ + {I J K : Type ℓ} + {asmI : Assembly I} + {asmJ : Assembly J} + {asmK : Assembly K} + (f : AssemblyMorphism asmI asmJ) + (g : AssemblyMorphism asmJ asmK) + (R : I → PER) + (S : J → PER) + (T : K → PER) + (fᴰ : displayedPerMorphism f R S) + (gᴰ : displayedPerMorphism g S T) where + +UFAMPER : Categoryᴰ ASM (ℓ-suc ℓ) ℓ +Categoryᴰ.ob[ UFAMPER ] (X , asmX) = X → PER +Categoryᴰ.Hom[_][_,_] UFAMPER {I , asmI} {J , asmJ} u R S = displayedPerMorphism u R S +Categoryᴰ.idᴰ UFAMPER {I , asmI} {R} = [ idDisplayedTracker asmI R ] +Categoryᴰ._⋆ᴰ_ UFAMPER {I , asmI} {J , asmJ} {K , asmK} {f} {g} {R} {S} {T} fᴰ gᴰ = {!!} +Categoryᴰ.⋆IdLᴰ UFAMPER = {!!} +Categoryᴰ.⋆IdRᴰ UFAMPER = {!!} +Categoryᴰ.⋆Assocᴰ UFAMPER = {!!} +Categoryᴰ.isSetHomᴰ UFAMPER = {!!}