Subquotient modest set and canonical PER of a modest set

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ᴰ

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'

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ᴰ

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)
+
+