From 2d33f50d6f9690618ee6b52b274af1f6fb43323a Mon Sep 17 00:00:00 2001 From: Rahul Chhabra Date: Thu, 4 Jul 2024 23:03:33 +0530 Subject: [PATCH] Subquotient modest set and canonical PER of a modest set --- src/Categories/CartesianMorphism.agda | 102 +++++++++++ src/Categories/FamiliesFibration.agda | 108 ++++++++++++ src/Categories/GenericObject.agda | 28 +++ src/Realizability/Modest/CanonicalPER.agda | 66 +++++++ .../Modest/GenericUniformFamily.agda | 164 ++++++++++++++++++ src/Realizability/PERs/ResizedPER.agda | 29 ++++ src/Realizability/PERs/SubQuotient.agda | 82 +++++++++ .../PERs/SubQuotientOfCanonicalPER.agda | 72 ++++++++ 8 files changed, 651 insertions(+) create mode 100644 src/Categories/CartesianMorphism.agda create mode 100644 src/Categories/FamiliesFibration.agda create mode 100644 src/Categories/GenericObject.agda create mode 100644 src/Realizability/Modest/CanonicalPER.agda create mode 100644 src/Realizability/Modest/GenericUniformFamily.agda create mode 100644 src/Realizability/PERs/SubQuotient.agda create mode 100644 src/Realizability/PERs/SubQuotientOfCanonicalPER.agda diff --git a/src/Categories/CartesianMorphism.agda b/src/Categories/CartesianMorphism.agda new file mode 100644 index 0000000..b7d9188 --- /dev/null +++ b/src/Categories/CartesianMorphism.agda @@ -0,0 +1,102 @@ +open import Cubical.Foundations.Prelude +open import Cubical.Categories.Category +open import Cubical.Categories.Displayed.Base +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.HLevels +open import Cubical.Data.Sigma +open import Cubical.HITs.PropositionalTruncation + +module Categories.CartesianMorphism where + +module Contravariant + {ℓB ℓ'B ℓE ℓ'E} + {B : Category ℓB ℓ'B} + (E : Categoryᴰ B ℓE ℓ'E) where + + open Category B + open Categoryᴰ E + + opaque + isCartesian : + {a b : ob} (f : B [ a , b ]) + {aᴰ : ob[ a ]} {bᴰ : ob[ b ]} + (fᴰ : Hom[ f ][ aᴰ , bᴰ ]) → + Type (ℓ-max (ℓ-max ℓB ℓ'B) (ℓ-max ℓE ℓ'E)) + isCartesian {a} {b} f {aᴰ} {bᴰ} fᴰ = + ∀ {c : ob} {cᴰ : ob[ c ]} (g : B [ c , a ]) → isEquiv λ (gᴰ : Hom[ g ][ cᴰ , aᴰ ]) → gᴰ ⋆ᴰ fᴰ + + opaque + unfolding isCartesian + isPropIsCartesian : + {a b : ob} (f : B [ a , b ]) + {aᴰ : ob[ a ]} {bᴰ : ob[ b ]} + (fᴰ : Hom[ f ][ aᴰ , bᴰ ]) → + isProp (isCartesian f fᴰ) + isPropIsCartesian f fᴰ = isPropImplicitΠ2 λ c cᴰ → isPropΠ λ g → isPropIsEquiv (_⋆ᴰ fᴰ) + + opaque + isCartesian' : + {a b : ob} (f : B [ a , b ]) + {aᴰ : ob[ a ]} {bᴰ : ob[ b ]} + (fᴰ : Hom[ f ][ aᴰ , bᴰ ]) → + Type (ℓ-max (ℓ-max ℓB ℓ'B) (ℓ-max ℓE ℓ'E)) + isCartesian' {a} {b} f {aᴰ} {bᴰ} fᴰ = + ∀ {c : ob} {cᴰ : ob[ c ]} (g : B [ c , a ]) → + (∀ (hᴰ : Hom[ g ⋆ f ][ cᴰ , bᴰ ]) → ∃![ gᴰ ∈ Hom[ g ][ cᴰ , aᴰ ] ] gᴰ ⋆ᴰ fᴰ ≡ hᴰ) + + opaque + unfolding isCartesian' + isPropIsCartesian' : + {a b : ob} {f : B [ a , b ]} + {aᴰ : ob[ a ]} {bᴰ : ob[ b ]} + (fᴰ : Hom[ f ][ aᴰ , bᴰ ]) → + isProp (isCartesian' f fᴰ) + isPropIsCartesian' {a} {b} {f} {aᴰ} {bᴰ} fᴰ = + isPropImplicitΠ2 λ c cᴰ → isPropΠ2 λ g hᴰ → isPropIsContr + + opaque + unfolding isCartesian + unfolding isCartesian' + isCartesian→isCartesian' : + {a b : ob} (f : B [ a , b ]) + {aᴰ : ob[ a ]} {bᴰ : ob[ b ]} + (fᴰ : Hom[ f ][ aᴰ , bᴰ ]) → + isCartesian f fᴰ → + isCartesian' f fᴰ + isCartesian→isCartesian' {a} {b} f {aᴰ} {bᴰ} fᴰ cartfᴰ g hᴰ = + ((invIsEq (cartfᴰ g) hᴰ) , (secIsEq (cartfᴰ g) hᴰ)) , + (λ { (gᴰ , gᴰ⋆fᴰ≡hᴰ) → cartfᴰ g .equiv-proof hᴰ .snd (gᴰ , gᴰ⋆fᴰ≡hᴰ) }) + + opaque + unfolding isCartesian + unfolding isCartesian' + isCartesian'→isCartesian : + {a b : ob} (f : B [ a , b ]) + {aᴰ : ob[ a ]} {bᴰ : ob[ b ]} + (fᴰ : Hom[ f ][ aᴰ , bᴰ ]) → + isCartesian' f fᴰ → + isCartesian f fᴰ + equiv-proof (isCartesian'→isCartesian {a} {b} f {aᴰ} {bᴰ} fᴰ cart'fᴰ g) hᴰ = (cart'fᴰ g hᴰ .fst) , (cart'fᴰ g hᴰ .snd) + + isCartesian≃isCartesian' : + {a b : ob} (f : B [ a , b ]) + {aᴰ : ob[ a ]} {bᴰ : ob[ b ]} + (fᴰ : Hom[ f ][ aᴰ , bᴰ ]) → + isCartesian f fᴰ ≃ isCartesian' f fᴰ + isCartesian≃isCartesian' {a} {b} f {aᴰ} {bᴰ} fᴰ = + propBiimpl→Equiv (isPropIsCartesian f fᴰ) (isPropIsCartesian' fᴰ) (isCartesian→isCartesian' f fᴰ) (isCartesian'→isCartesian f fᴰ) + + cartesianLift : {a b : ob} (f : B [ a , b ]) (bᴰ : ob[ b ]) → Type _ + cartesianLift {a} {b} f bᴰ = Σ[ aᴰ ∈ ob[ a ] ] Σ[ fᴰ ∈ Hom[ f ][ aᴰ , bᴰ ] ] isCartesian f fᴰ + + isCartesianFibration : Type _ + isCartesianFibration = + ∀ {a b : ob} {bᴰ : ob[ b ]} + → (f : Hom[ a , b ]) + → ∥ cartesianLift f bᴰ ∥₁ + + isPropIsCartesianFibration : isProp isCartesianFibration + isPropIsCartesianFibration = isPropImplicitΠ3 λ a b bᴰ → isPropΠ λ f → isPropPropTrunc + + cleavage : Type _ + cleavage = {a b : ob} (f : Hom[ a , b ]) (bᴰ : ob[ b ]) → cartesianLift f bᴰ diff --git a/src/Categories/FamiliesFibration.agda b/src/Categories/FamiliesFibration.agda new file mode 100644 index 0000000..8b2bfd1 --- /dev/null +++ b/src/Categories/FamiliesFibration.agda @@ -0,0 +1,108 @@ +open import Cubical.Foundations.Prelude +open import Cubical.Categories.Category +open import Cubical.Categories.Displayed.Base +open import Cubical.Categories.Instances.Sets +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.HLevels +open import Cubical.Data.Sigma +open import Cubical.HITs.PropositionalTruncation +open import Categories.CartesianMorphism +open import Categories.GenericObject +module Categories.FamiliesFibration where + +module FamiliesFibration + {ℓ ℓ'} + (C : Category ℓ ℓ') + (ℓ'' : Level) where + open Category C + Families : Categoryᴰ (SET ℓ'') (ℓ-max ℓ ℓ'') (ℓ-max ℓ' ℓ'') + Categoryᴰ.ob[ Families ] (I , isSetI) = I → ob + Categoryᴰ.Hom[_][_,_] Families {I , isSetI} {J , isSetJ} u X Y = (i : I) → Hom[ X i , Y (u i) ] + Categoryᴰ.idᴰ Families {I , isSetI} {X} i = id + Categoryᴰ._⋆ᴰ_ Families {I , isSetI} {J , isSetJ} {K , isSetK} {f} {g} {X} {Y} {Z} fᴰ gᴰ i = + fᴰ i ⋆ gᴰ (f i) + Categoryᴰ.⋆IdLᴰ Families {I , isSetI} {J , isSetJ} {f} {X} {Y} fᴰ = + funExt λ i → ⋆IdL (fᴰ i) + Categoryᴰ.⋆IdRᴰ Families {I , isSetI} {J , isSetJ} {f} {X} {Y} fᴰ = + funExt λ i → ⋆IdR (fᴰ i) + Categoryᴰ.⋆Assocᴰ Families {I , isSetI} {J , isSetJ} {K , isSetK} {L , isSetL} {f} {g} {h} {X} {Y} {Z} {W} fᴰ gᴰ hᴰ = + funExt λ i → ⋆Assoc (fᴰ i) (gᴰ (f i)) (hᴰ (g (f i))) + Categoryᴰ.isSetHomᴰ Families {I , isSetI} {J , isSetJ} {f} {X} {Y} = isSetΠ λ i → isSetHom + + open Contravariant Families + open Categoryᴰ Families + cleavageFamilies : cleavage + cleavageFamilies a@{I , isSetI} b@{J , isSetJ} f Y = + X , + fᴰ , + cart where + + X : I → ob + X i = Y (f i) + + fᴰ : (i : I) → Hom[ X i , Y (f i) ] + fᴰ i = id + + opaque + unfolding isCartesian' + cart' : isCartesian' {a = a} {b = b} f {bᴰ = Y} fᴰ + cart' k@{K , isSetK} {Z} g hᴰ = + (hᴰ , (funExt (λ k → ⋆IdR (hᴰ k)))) , + λ { (! , !comm) → + Σ≡Prop + (λ ! → isSetHomᴰ {x = k} {y = b} {xᴰ = Z} {yᴰ = Y} (λ k → ! k ⋆ fᴰ (g k)) hᴰ) + (funExt + (λ k → + sym + (! k + ≡⟨ sym (⋆IdR (! k)) ⟩ + (! k ⋆ fᴰ (g k)) + ≡[ i ]⟨ !comm i k ⟩ + hᴰ k + ∎))) } + + cart : isCartesian {a = a} {b = b} f {bᴰ = Y} fᴰ + cart = isCartesian'→isCartesian {a = a} {b = b} f {bᴰ = Y} fᴰ cart' + +module GenericFamily + {ℓ ℓ'} + (C : Category ℓ ℓ') + (isSetCOb : isSet (C .Category.ob)) where + + open FamiliesFibration C ℓ + open Category C + open Categoryᴰ Families + open Contravariant Families + genericFamily : GenericObject Families + GenericObject.base genericFamily = ob , isSetCOb + GenericObject.displayed genericFamily = λ x → x + GenericObject.isGeneric genericFamily i@{I , isSetI} X = + f , + fᴰ , + cart where + f : I → ob + f = X + + fᴰ : Hom[_][_,_] {x = i} {y = ob , isSetCOb} f X (λ x → x) + fᴰ i = id + + opaque + unfolding isCartesian' + cart' : isCartesian' {a = i} {b = ob , isSetCOb} f {bᴰ = λ x → x} fᴰ + cart' {J , isSetJ} {Z} g hᴰ = + (hᴰ , funExt λ j → ⋆IdR (hᴰ j)) , + λ { (! , !comm) → + Σ≡Prop + (λ ! → isSetHomᴰ {x = J , isSetJ} {y = i} {f = g} {xᴰ = Z} {yᴰ = f} (λ j → ! j ⋆ fᴰ (g j)) hᴰ) + (funExt + λ j → + sym + (! j + ≡⟨ sym (⋆IdR (! j)) ⟩ + ! j ⋆ fᴰ (g j) + ≡[ i ]⟨ !comm i j ⟩ + hᴰ j + ∎)) } + + cart : isCartesian {a = i} {b = ob , isSetCOb} f {bᴰ = λ x → x} fᴰ + cart = isCartesian'→isCartesian f fᴰ cart' diff --git a/src/Categories/GenericObject.agda b/src/Categories/GenericObject.agda new file mode 100644 index 0000000..0412bb1 --- /dev/null +++ b/src/Categories/GenericObject.agda @@ -0,0 +1,28 @@ +open import Cubical.Foundations.Prelude +open import Cubical.Categories.Category +open import Cubical.Categories.Displayed.Base +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.HLevels +open import Cubical.Data.Sigma +open import Cubical.HITs.PropositionalTruncation +open import Categories.CartesianMorphism + +module Categories.GenericObject where + +module _ + {ℓB ℓ'B ℓE ℓ'E} + {B : Category ℓB ℓ'B} + (E : Categoryᴰ B ℓE ℓ'E) where + + open Category B + open Categoryᴰ E + open Contravariant E + + record GenericObject : Type (ℓ-max (ℓ-max ℓB ℓ'B) (ℓ-max ℓE ℓ'E)) where + constructor makeGenericObject + field + base : ob + displayed : ob[ base ] + isGeneric : + ∀ {t : ob} (tᴰ : ob[ t ]) + → Σ[ f ∈ Hom[ t , base ] ] Σ[ fᴰ ∈ Hom[ f ][ tᴰ , displayed ] ] isCartesian f fᴰ diff --git a/src/Realizability/Modest/CanonicalPER.agda b/src/Realizability/Modest/CanonicalPER.agda new file mode 100644 index 0000000..30ade69 --- /dev/null +++ b/src/Realizability/Modest/CanonicalPER.agda @@ -0,0 +1,66 @@ +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.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.CanonicalPER {ℓ} {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.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 + + 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) + + diff --git a/src/Realizability/Modest/GenericUniformFamily.agda b/src/Realizability/Modest/GenericUniformFamily.agda new file mode 100644 index 0000000..50388b7 --- /dev/null +++ b/src/Realizability/Modest/GenericUniformFamily.agda @@ -0,0 +1,164 @@ +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.GenericUniformFamily {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) (resizing : hPropResizing ℓ) 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.ResizedPER ca resizing +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 + +uniformFamilyCleavage : cleavage +uniformFamilyCleavage {X , asmX} {Y , asmY} f N = + N' , fᴰ , cartfᴰ where + N' : UniformFamily asmX + UniformFamily.carriers N' x = N .carriers (f .map x) + UniformFamily.assemblies N' x = N .assemblies (f .map x) + UniformFamily.isModestFamily N' x = N .isModestFamily (f .map x) + + fᴰ : DisplayedUFamMap asmX asmY f N' N + DisplayedUFamMap.fibrewiseMap fᴰ x Nfx = Nfx + DisplayedUFamMap.isTracked fᴰ = + do + let + realizer : Term as 2 + realizer = # zero + return + (λ*2 realizer , + (λ x a a⊩x Nfx b b⊩Nfx → + subst + (_⊩[ N .assemblies (f .map x) ] Nfx) + (sym (λ*2ComputationRule realizer a b)) + b⊩Nfx)) + + opaque + unfolding isCartesian' + cart'fᴰ : isCartesian' f fᴰ + cart'fᴰ {Z , asmZ} {M} g hᴰ = + (! , !⋆fᴰ≡hᴰ) , + λ { (!' , !'comm) → + Σ≡Prop + (λ ! → UNIMOD .Categoryᴰ.isSetHomᴰ _ _) + (DisplayedUFamMapPathP + _ _ _ _ _ _ _ _ _ + λ z Mz → + sym + (!' .fibrewiseMap z Mz + ≡[ i ]⟨ !'comm i .fibrewiseMap z Mz ⟩ + hᴰ .fibrewiseMap z Mz + ∎)) } where + ! : DisplayedUFamMap asmZ asmX g M N' + DisplayedUFamMap.fibrewiseMap ! z Mz = hᴰ .fibrewiseMap z Mz + DisplayedUFamMap.isTracked ! = hᴰ .isTracked + + !⋆fᴰ≡hᴰ : composeDisplayedUFamMap asmZ asmX asmY g f M N' N ! fᴰ ≡ hᴰ + !⋆fᴰ≡hᴰ = + DisplayedUFamMapPathP + asmZ asmY _ _ + M N + (composeDisplayedUFamMap asmZ asmX asmY g f M N' N ! fᴰ) hᴰ refl + λ z Mz → refl + + cartfᴰ : isCartesian f fᴰ + cartfᴰ = isCartesian'→isCartesian f fᴰ cart'fᴰ + +∇PER = ∇ ⟅ ResizedPER , isSetResizedPER ⟆ +asm∇PER = ∇PER .snd + +genericUniformFamily : GenericObject UNIMOD +GenericObject.base genericUniformFamily = ∇PER +UniformFamily.carriers (GenericObject.displayed genericUniformFamily) per = subQuotient (enlargePER per) +UniformFamily.assemblies (GenericObject.displayed genericUniformFamily) per = subQuotientAssembly (enlargePER per) +UniformFamily.isModestFamily (GenericObject.displayed genericUniformFamily) per = isModestSubQuotientAssembly (enlargePER per) +GenericObject.isGeneric genericUniformFamily {X , asmX} M = + f , fᴰ , {!!} where + + f : AssemblyMorphism asmX asm∇PER + AssemblyMorphism.map f x = shrinkPER (canonicalPER (M .assemblies x) (M .isModestFamily x)) + AssemblyMorphism.tracker f = return (k , (λ _ _ _ → tt*)) + + subQuotientTargetType : (x : X) → M .carriers x → Type ℓ + subQuotientTargetType x Mx = subQuotient (canonicalPER (M .assemblies x) (M .isModestFamily x)) + + fᴰ : DisplayedUFamMap asmX asm∇PER f M (genericUniformFamily .GenericObject.displayed) + DisplayedUFamMap.fibrewiseMap fᴰ x Mx = + subst (λ x → subQuotient x) (sym equation) target module CartesianMapDefinition where + targetType : Type ℓ + targetType = subQuotient (canonicalPER (M .assemblies x) (M .isModestFamily x)) + + opaque + equation : enlargePER (shrinkPER (canonicalPER (M .assemblies x) (M .isModestFamily x))) ≡ canonicalPER (M .assemblies x) (M .isModestFamily x) + equation = enlargePER⋆shrinkPER≡id (canonicalPER (M .assemblies x) (M .isModestFamily x)) + + mainMap : Σ[ a ∈ A ] (a ⊩[ M .assemblies x ] Mx) → subQuotient (canonicalPER (M .assemblies x) (M .isModestFamily x)) + mainMap (a , a⊩Mx) = [ a ] + + mainMap2Constant : 2-Constant mainMap + mainMap2Constant (a , a⊩Mx) (b , b⊩Mx) = eq/ a b (return (Mx , a⊩Mx , b⊩Mx)) + + opaque + target : targetType + target = + PT.rec→Set + squash/ + mainMap + mainMap2Constant + (M .assemblies x .⊩surjective Mx) + + opaque + isTrackedCartesianMap : + ∀ (a : A) + → a ⊩[ asmX ] x + → (b : A) + → b ⊩[ M .assemblies x ] Mx + → ⟨ + subQuotientRealizability + (enlargePER (shrinkPER (canonicalPER (M .assemblies x) (M .isModestFamily x)))) + (λ*2 (# one) ⨾ a ⨾ b) + (subst subQuotient (sym equation) target) + ⟩ + isTrackedCartesianMap a a⊩x b b⊩Mx = + {!!} + DisplayedUFamMap.isTracked fᴰ = + do + return + (λ*2 (# one) , + λ x a a⊩x Mx b b⊩Mx → {!CartesianMapDefinition.isTrackedCartesianMap x Mx a a⊩x b b⊩Mx!}) + diff --git a/src/Realizability/PERs/ResizedPER.agda b/src/Realizability/PERs/ResizedPER.agda index c8b5b16..dc43ef1 100644 --- a/src/Realizability/PERs/ResizedPER.agda +++ b/src/Realizability/PERs/ResizedPER.agda @@ -27,6 +27,7 @@ module Realizability.PERs.ResizedPER open import Realizability.Assembly.Base ca open import Realizability.Assembly.Morphism ca open import Realizability.PERs.PER ca +open import Realizability.Modest.Base ca open CombinatoryAlgebra ca open Combinators ca renaming (i to Id; ia≡a to Ida≡a) @@ -162,5 +163,33 @@ Iso.leftInv ResizedPERIsoPER resizedPer = ResizedPER≡ _ _ λ a b → shrinkFromExtracted (resizedPer .relation a b) +opaque + shrinkPER : PER → ResizedPER + shrinkPER = ResizedPERIsoPER .Iso.inv + +opaque + enlargePER : ResizedPER → PER + enlargePER = ResizedPERIsoPER .Iso.fun + +opaque + unfolding shrinkPER + unfolding enlargePER + shrinkPER⋆enlargePER≡id : ∀ resized → shrinkPER (enlargePER resized) ≡ resized + shrinkPER⋆enlargePER≡id resized = ResizedPERIsoPER .Iso.leftInv resized + +opaque + unfolding shrinkPER + unfolding enlargePER + enlargePER⋆shrinkPER≡id : ∀ per → enlargePER (shrinkPER per) ≡ per + enlargePER⋆shrinkPER≡id per = ResizedPERIsoPER .Iso.rightInv per + ResizedPER≃PER : ResizedPER ≃ PER ResizedPER≃PER = isoToEquiv ResizedPERIsoPER + +opaque + transportFromSmall : ∀ {ℓ'} {P : ResizedPER → Type ℓ'} → (∀ per → P (shrinkPER per)) → ∀ resized → P resized + transportFromSmall {ℓ'} {P} small resized = subst P (shrinkPER⋆enlargePER≡id resized) (small (enlargePER resized)) + +opaque + transportFromLarge : ∀ {ℓ'} {P : PER → Type ℓ'} → (∀ resized → P (enlargePER resized)) → ∀ per → P per + transportFromLarge {ℓ'} {P} large per = subst P (enlargePER⋆shrinkPER≡id per) (large (shrinkPER per)) diff --git a/src/Realizability/PERs/SubQuotient.agda b/src/Realizability/PERs/SubQuotient.agda new file mode 100644 index 0000000..e28420a --- /dev/null +++ b/src/Realizability/PERs/SubQuotient.agda @@ -0,0 +1,82 @@ +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.Path +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.SubQuotient + {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) where + +open import Realizability.Assembly.Base ca +open import Realizability.Assembly.Morphism ca +open import Realizability.PERs.PER ca +open import Realizability.Modest.Base ca + +open CombinatoryAlgebra ca +open Combinators ca renaming (i to Id; ia≡a to Ida≡a) + +module _ + (per : PER) where + + subQuotient : Type ℓ + subQuotient = A / per .PER.relation + + subQuotientRealizability : A → subQuotient → hProp ℓ + subQuotientRealizability r [a] = + SQ.rec + isSetHProp + (λ a → ([ a ] ≡ [ r ]) , squash/ [ a ] [ r ]) + (λ a b a~b → + Σ≡Prop + (λ _ → isPropIsProp) + (hPropExt (squash/ [ a ] [ r ]) (squash/ [ b ] [ r ]) (λ [a]≡[r] → sym (eq/ a b a~b) ∙ [a]≡[r]) λ [b]≡[r] → sym (eq/ b a (per .PER.isPER .fst a b a~b)) ∙ [b]≡[r])) + [a] + + subQuotientAssembly : Assembly subQuotient + Assembly._⊩_ subQuotientAssembly r [a] = ⟨ subQuotientRealizability r [a] ⟩ + Assembly.isSetX subQuotientAssembly = squash/ + Assembly.⊩isPropValued subQuotientAssembly r [a] = str (subQuotientRealizability r [a]) + Assembly.⊩surjective subQuotientAssembly [a] = + do + (a , [a]≡[a]) ← []surjective [a] + return + (a , (subst (λ [a] → ⟨ subQuotientRealizability a [a] ⟩) [a]≡[a] refl)) + + isModestSubQuotientAssembly : isModest subQuotientAssembly + isModestSubQuotientAssembly x y a a⊩x a⊩y = + SQ.elimProp2 + {P = motive} + isPropMotive + coreMap + x y a a⊩x a⊩y where + motive : subQuotient → subQuotient → Type ℓ + motive x y = (a : A) → a ⊩[ subQuotientAssembly ] x → a ⊩[ subQuotientAssembly ] y → x ≡ y + + isPropMotive : ∀ x y → isProp (motive x y) + isPropMotive x y = isPropΠ3 λ _ _ _ → squash/ x y + + coreMap : (r s : A) → motive [ r ] [ s ] + coreMap r s a a⊩[r] a⊩[s] = + [ r ] + ≡⟨ a⊩[r] ⟩ + [ a ] + ≡⟨ sym a⊩[s] ⟩ + [ s ] + ∎ diff --git a/src/Realizability/PERs/SubQuotientOfCanonicalPER.agda b/src/Realizability/PERs/SubQuotientOfCanonicalPER.agda new file mode 100644 index 0000000..2037d7d --- /dev/null +++ b/src/Realizability/PERs/SubQuotientOfCanonicalPER.agda @@ -0,0 +1,72 @@ +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.Foundations.Univalence +open import Cubical.Functions.FunExtEquiv +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.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.PERs.SubQuotientOfCanonicalPER {ℓ} {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 + +module _ (per : PER) where + + theCanonicalPER : PER + theCanonicalPER = canonicalPER (subQuotientAssembly per) (isModestSubQuotientAssembly per) + + opaque + canonicalPEROfSubQuotientIsId : theCanonicalPER ≡ per + canonicalPEROfSubQuotientIsId = + PER≡ _ _ + (funExt₂ pointwise) where + opaque + effectiveness : (x : subQuotient per) (a b : A) → a ⊩[ subQuotientAssembly per ] x → b ⊩[ subQuotientAssembly per ] x → per .PER.relation a b + effectiveness x a b a⊩x b⊩x = {!!} + + opaque + dir1 : ∀ a b → theCanonicalPER .PER.relation a b → per .PER.relation a b + dir1 a b ∃x = + equivFun + (propTruncIdempotent≃ (per .PER.isPropValued a b)) + (do + (x , a⊩x , b⊩x) ← ∃x + return (effectiveness x a b a⊩x b⊩x)) + + opaque + pointwise : ∀ a b → theCanonicalPER .PER.relation a b ≡ per .PER.relation a b + pointwise a b = + hPropExt + (theCanonicalPER .PER.isPropValued a b) + (per .PER.isPropValued a b) + (dir1 a b) + {!!} +