diff --git a/docs/Categories.CartesianMorphism.html b/docs/Categories.CartesianMorphism.html
new file mode 100644
index 0000000..900f768
--- /dev/null
+++ b/docs/Categories.CartesianMorphism.html
@@ -0,0 +1,104 @@
+
+Categories.CartesianMorphism 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ᴰ
+Categories.GenericObject 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ᴰ
+Cubical.Categories.Displayed.Base
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Displayed.Base where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.Data.Sigma
+open import Cubical.Categories.Category.Base
+
+private
+ variable
+ ℓC ℓC' ℓCᴰ ℓCᴰ' ℓDᴰ ℓDᴰ' : Level
+
+
+record Categoryᴰ ( C : Category ℓC ℓC' ) ℓCᴰ ℓCᴰ' : Type ( ℓ-suc ( ℓ-max ( ℓ-max ℓC ℓC' ) ( ℓ-max ℓCᴰ ℓCᴰ' ))) where
+ no-eta-equality
+ open Category C
+ field
+ ob[_] : ob → Type ℓCᴰ
+ Hom[_][_,_] : { x y : ob } → Hom[ x , y ] → ob[ x ] → ob[ y ] → Type ℓCᴰ'
+ idᴰ : ∀ { x } { p : ob[ x ] } → Hom[ id ][ p , p ]
+ _⋆ᴰ_ : ∀ { x y z } { f : Hom[ x , y ] } { g : Hom[ y , z ] } { xᴰ yᴰ zᴰ }
+ → Hom[ f ][ xᴰ , yᴰ ] → Hom[ g ][ yᴰ , zᴰ ] → Hom[ f ⋆ g ][ xᴰ , zᴰ ]
+
+ infixr 9 _⋆ᴰ_
+ infixr 9 _∘ᴰ_
+
+ _≡[_]_ : ∀ { x y xᴰ yᴰ } { f g : Hom[ x , y ] } → Hom[ f ][ xᴰ , yᴰ ] → f ≡ g → Hom[ g ][ xᴰ , yᴰ ] → Type ℓCᴰ'
+ _≡[_]_ { x } { y } { xᴰ } { yᴰ } fᴰ p gᴰ = PathP (λ i → Hom[ p i ][ xᴰ , yᴰ ] ) fᴰ gᴰ
+
+ infix 2 _≡[_]_
+
+ field
+ ⋆IdLᴰ : ∀ { x y } { f : Hom[ x , y ] } { xᴰ yᴰ } ( fᴰ : Hom[ f ][ xᴰ , yᴰ ] ) → idᴰ ⋆ᴰ fᴰ ≡[ ⋆IdL f ] fᴰ
+ ⋆IdRᴰ : ∀ { x y } { f : Hom[ x , y ] } { xᴰ yᴰ } ( fᴰ : Hom[ f ][ xᴰ , yᴰ ] ) → fᴰ ⋆ᴰ idᴰ ≡[ ⋆IdR f ] fᴰ
+ ⋆Assocᴰ : ∀ { x y z w } { f : Hom[ x , y ] } { g : Hom[ y , z ] } { h : Hom[ z , w ] } { xᴰ yᴰ zᴰ wᴰ }
+ ( fᴰ : Hom[ f ][ xᴰ , yᴰ ] ) ( gᴰ : Hom[ g ][ yᴰ , zᴰ ] ) ( hᴰ : Hom[ h ][ zᴰ , wᴰ ] )
+ → ( fᴰ ⋆ᴰ gᴰ ) ⋆ᴰ hᴰ ≡[ ⋆Assoc f g h ] fᴰ ⋆ᴰ ( gᴰ ⋆ᴰ hᴰ )
+ isSetHomᴰ : ∀ { x y } { f : Hom[ x , y ] } { xᴰ yᴰ } → isSet Hom[ f ][ xᴰ , yᴰ ]
+
+
+ _∘ᴰ_ : ∀ { x y z } { f : Hom[ x , y ] } { g : Hom[ y , z ] } { xᴰ yᴰ zᴰ }
+ → Hom[ g ][ yᴰ , zᴰ ] → Hom[ f ][ xᴰ , yᴰ ] → Hom[ f ⋆ g ][ xᴰ , zᴰ ]
+ g ∘ᴰ f = f ⋆ᴰ g
+
+
+_[_][_,_] = Categoryᴰ.Hom[_][_,_]
+
+
+module _ { C : Category ℓC ℓC' } ( Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ' ) where
+
+ open Category
+ open Categoryᴰ Cᴰ
+ private
+ module C = Category C
+
+ ∫C : Category ( ℓ-max ℓC ℓCᴰ ) ( ℓ-max ℓC' ℓCᴰ' )
+ ∫C . ob = Σ _ ob[_]
+ ∫C . Hom[_,_] (_ , xᴰ ) (_ , yᴰ ) = Σ _ Hom[_][ xᴰ , yᴰ ]
+ ∫C . id = _ , idᴰ
+ ∫C . _⋆_ (_ , fᴰ ) (_ , gᴰ ) = _ , fᴰ ⋆ᴰ gᴰ
+ ∫C . ⋆IdL _ = ΣPathP (_ , ⋆IdLᴰ _)
+ ∫C . ⋆IdR _ = ΣPathP (_ , ⋆IdRᴰ _)
+ ∫C . ⋆Assoc _ _ _ = ΣPathP (_ , ⋆Assocᴰ _ _ _)
+ ∫C . isSetHom = isSetΣ C.isSetHom (λ _ → isSetHomᴰ )
+
+
+module _ { C : Category ℓC ℓC' }
+ ( Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ' )
+ ( Dᴰ : Categoryᴰ ( ∫C Cᴰ ) ℓDᴰ ℓDᴰ' )
+ where
+
+ open Categoryᴰ
+ private
+ module Cᴰ = Categoryᴰ Cᴰ
+ module Dᴰ = Categoryᴰ Dᴰ
+
+ ∫Cᴰ : Categoryᴰ C ( ℓ-max ℓCᴰ ℓDᴰ ) ( ℓ-max ℓCᴰ' ℓDᴰ' )
+ ∫Cᴰ . ob[_] x = Σ[ xᴰ ∈ Cᴰ.ob[ x ] ] Dᴰ.ob[ x , xᴰ ]
+ ∫Cᴰ . Hom[_][_,_] f (_ , zᴰ ) (_ , wᴰ ) = Σ[ fᴰ ∈ Cᴰ.Hom[ f ][ _ , _ ] ] Dᴰ.Hom[ f , fᴰ ][ zᴰ , wᴰ ]
+ ∫Cᴰ . idᴰ = Cᴰ.idᴰ , Dᴰ.idᴰ
+ ∫Cᴰ . _⋆ᴰ_ (_ , hᴰ ) (_ , kᴰ ) = _ , hᴰ Dᴰ.⋆ᴰ kᴰ
+ ∫Cᴰ . ⋆IdLᴰ _ = ΣPathP (_ , Dᴰ.⋆IdLᴰ _)
+ ∫Cᴰ . ⋆IdRᴰ _ = ΣPathP (_ , Dᴰ.⋆IdRᴰ _)
+ ∫Cᴰ . ⋆Assocᴰ _ _ _ = ΣPathP (_ , Dᴰ.⋆Assocᴰ _ _ _)
+ ∫Cᴰ . isSetHomᴰ = isSetΣ Cᴰ.isSetHomᴰ (λ _ → Dᴰ.isSetHomᴰ )
+
+module _ { C : Category ℓC ℓC' }
+ ( Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ' )
+ ( Dᴰ : Categoryᴰ C ℓDᴰ ℓDᴰ' )
+ where
+
+ open Categoryᴰ
+ private
+ module Dᴰ = Categoryᴰ Dᴰ
+
+ weakenᴰ : Categoryᴰ ( ∫C Cᴰ ) ℓDᴰ ℓDᴰ'
+ weakenᴰ . ob[_] ( x , _) = Dᴰ.ob[ x ]
+ weakenᴰ . Hom[_][_,_] ( f , _) = Dᴰ.Hom[ f ][_,_]
+ weakenᴰ . idᴰ = Dᴰ.idᴰ
+ weakenᴰ . _⋆ᴰ_ = Dᴰ._⋆ᴰ_
+ weakenᴰ . ⋆IdLᴰ = Dᴰ.⋆IdLᴰ
+ weakenᴰ . ⋆IdRᴰ = Dᴰ.⋆IdRᴰ
+ weakenᴰ . ⋆Assocᴰ = Dᴰ.⋆Assocᴰ
+ weakenᴰ . isSetHomᴰ = Dᴰ.isSetHomᴰ
+
+module _ { C : Category ℓC ℓC' } ( Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ' ) where
+ open Category C
+ open Categoryᴰ Cᴰ
+
+ record isIsoᴰ { a b : ob } { f : C [ a , b ] } ( f-isIso : isIso C f )
+ { aᴰ : ob[ a ] } { bᴰ : ob[ b ] } ( fᴰ : Hom[ f ][ aᴰ , bᴰ ] )
+ : Type ℓCᴰ'
+ where
+ constructor isisoᴰ
+ open isIso f-isIso
+ field
+ invᴰ : Hom[ inv ][ bᴰ , aᴰ ]
+ secᴰ : invᴰ ⋆ᴰ fᴰ ≡[ sec ] idᴰ
+ retᴰ : fᴰ ⋆ᴰ invᴰ ≡[ ret ] idᴰ
+
+ CatIsoᴰ : { a b : ob } → CatIso C a b → ob[ a ] → ob[ b ] → Type ℓCᴰ'
+ CatIsoᴰ ( f , f-isIso ) aᴰ bᴰ = Σ[ fᴰ ∈ Hom[ f ][ aᴰ , bᴰ ] ] isIsoᴰ f-isIso fᴰ
+
+ idᴰCatIsoᴰ : { x : ob } { xᴰ : ob[ x ] } → CatIsoᴰ idCatIso xᴰ xᴰ
+ idᴰCatIsoᴰ = idᴰ , isisoᴰ idᴰ ( ⋆IdLᴰ idᴰ ) ( ⋆IdLᴰ idᴰ )
+
\ No newline at end of file
diff --git a/docs/Cubical.Categories.Displayed.Reasoning.html b/docs/Cubical.Categories.Displayed.Reasoning.html
new file mode 100644
index 0000000..6e7e7da
--- /dev/null
+++ b/docs/Cubical.Categories.Displayed.Reasoning.html
@@ -0,0 +1,110 @@
+
+Cubical.Categories.Displayed.Reasoning {-# OPTIONS --safe #-}
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.GroupoidLaws
+open import Cubical.Foundations.Transport
+
+open import Cubical.Categories.Category.Base
+open import Cubical.Categories.Displayed.Base
+
+module Cubical.Categories.Displayed.Reasoning
+ { ℓC ℓ'C ℓCᴰ ℓ'Cᴰ : Level }
+ { C : Category ℓC ℓ'C }
+ ( Cᴰ : Categoryᴰ C ℓCᴰ ℓ'Cᴰ )
+ where
+
+ open Categoryᴰ Cᴰ
+ private module C = Category C
+ open Category hiding ( _∘_ )
+
+ reind : { a b : C.ob } { f g : C [ a , b ] } ( p : f ≡ g )
+ { aᴰ : ob[ a ] } { bᴰ : ob[ b ] }
+ → Hom[ f ][ aᴰ , bᴰ ] → Hom[ g ][ aᴰ , bᴰ ]
+ reind p = subst Hom[_][ _ , _ ] p
+
+ reind-filler : { a b : C.ob } { f g : C [ a , b ] } ( p : f ≡ g )
+ { aᴰ : ob[ a ] } { bᴰ : ob[ b ] }
+ ( f : Hom[ f ][ aᴰ , bᴰ ] )
+ → f ≡[ p ] reind p f
+ reind-filler p = subst-filler Hom[_][ _ , _ ] p
+
+ reind-filler-sym : { a b : C.ob } { f g : C [ a , b ] } ( p : f ≡ g )
+ { aᴰ : ob[ a ] } { bᴰ : ob[ b ] }
+ ( f : Hom[ g ][ aᴰ , bᴰ ] )
+ → reind ( sym p ) f ≡[ p ] f
+ reind-filler-sym p = symP ∘ reind-filler ( sym p )
+
+ ≡[]-rectify : { a b : C.ob } { f g : C [ a , b ] } { p p' : f ≡ g }
+ { aᴰ : ob[ a ] } { bᴰ : ob[ b ] }
+ { fᴰ : Hom[ f ][ aᴰ , bᴰ ] }
+ { gᴰ : Hom[ g ][ aᴰ , bᴰ ] }
+ → fᴰ ≡[ p ] gᴰ → fᴰ ≡[ p' ] gᴰ
+ ≡[]-rectify { fᴰ = fᴰ } { gᴰ = gᴰ } = subst ( fᴰ ≡[_] gᴰ ) ( C.isSetHom _ _ _ _)
+
+ ≡[]∙ : { a b : C.ob } { f g h : C [ a , b ] }
+ { aᴰ : ob[ a ] } { bᴰ : ob[ b ] }
+ { fᴰ : Hom[ f ][ aᴰ , bᴰ ] }
+ { gᴰ : Hom[ g ][ aᴰ , bᴰ ] }
+ { hᴰ : Hom[ h ][ aᴰ , bᴰ ] }
+ ( p : f ≡ g ) ( q : g ≡ h )
+ → fᴰ ≡[ p ] gᴰ
+ → gᴰ ≡[ q ] hᴰ → fᴰ ≡[ p ∙ q ] hᴰ
+ ≡[]∙ { fᴰ = fᴰ } { hᴰ = hᴰ } p q eq1 eq2 =
+ subst
+ (λ p → PathP (λ i → p i ) fᴰ hᴰ )
+ ( sym $ congFunct Hom[_][ _ , _ ] p q )
+ ( compPathP eq1 eq2 )
+
+ infixr 30 ≡[]∙
+ syntax ≡[]∙ p q eq1 eq2 = eq1 [ p ]∙[ q ] eq2
+
+ ≡[]⋆ : { a b c : C.ob } { f g : C [ a , b ] } { h i : C [ b , c ] }
+ { aᴰ : ob[ a ] } { bᴰ : ob[ b ] } { cᴰ : ob[ c ] }
+ { fᴰ : Hom[ f ][ aᴰ , bᴰ ] }
+ { gᴰ : Hom[ g ][ aᴰ , bᴰ ] }
+ { hᴰ : Hom[ h ][ bᴰ , cᴰ ] }
+ { iᴰ : Hom[ i ][ bᴰ , cᴰ ] }
+ ( p : f ≡ g ) ( q : h ≡ i )
+ → fᴰ ≡[ p ] gᴰ → hᴰ ≡[ q ] iᴰ → fᴰ ⋆ᴰ hᴰ ≡[ cong₂ C._⋆_ p q ] gᴰ ⋆ᴰ iᴰ
+ ≡[]⋆ _ _ = congP₂ (λ _ → _⋆ᴰ_ )
+
+ infixr 30 ≡[]⋆
+ syntax ≡[]⋆ p q eq1 eq2 = eq1 [ p ]⋆[ q ] eq2
+
+ reind-rectify : { a b : C.ob } { f g : C [ a , b ] } { p p' : f ≡ g }
+ { aᴰ : ob[ a ] } { bᴰ : ob[ b ] }
+ { fᴰ : Hom[ f ][ aᴰ , bᴰ ] }
+ → reind p fᴰ ≡ reind p' fᴰ
+ reind-rectify { fᴰ = fᴰ } = cong (λ p → reind p fᴰ ) ( C.isSetHom _ _ _ _)
+
+ reind-contractʳ : { a b c : C.ob } { f g : C [ a , b ] } { h : C [ b , c ] }
+ { p : f ≡ g }
+ { aᴰ : ob[ a ] } { bᴰ : ob[ b ] } { cᴰ : ob[ c ] }
+ { fᴰ : Hom[ f ][ aᴰ , bᴰ ] } { hᴰ : Hom[ h ][ bᴰ , cᴰ ] }
+ → reind ( cong ( C._⋆ h ) p ) ( fᴰ ⋆ᴰ hᴰ ) ≡ reind p fᴰ ⋆ᴰ hᴰ
+ reind-contractʳ { hᴰ = hᴰ } = fromPathP $
+ congP (λ _ → _⋆ᴰ hᴰ ) ( transport-filler _ _)
+
+ reind-comp : { a b : C.ob } { f g h : C [ a , b ] } { p : f ≡ g } { q : g ≡ h }
+ { aᴰ : ob[ a ] } { bᴰ : ob[ b ] }
+ { fᴰ : Hom[ f ][ aᴰ , bᴰ ] }
+ → reind ( p ∙ q ) fᴰ ≡ reind q ( reind p fᴰ )
+ reind-comp = substComposite Hom[_][ _ , _ ] _ _ _
+
+ reind-contractˡ : { a b c : C.ob } { f : C [ a , b ] } { g h : C [ b , c ] }
+ { p : g ≡ h }
+ { aᴰ : ob[ a ] } { bᴰ : ob[ b ] } { cᴰ : ob[ c ] }
+ { fᴰ : Hom[ f ][ aᴰ , bᴰ ] } { gᴰ : Hom[ g ][ bᴰ , cᴰ ] }
+ → reind ( cong ( f C.⋆_ ) p ) ( fᴰ ⋆ᴰ gᴰ ) ≡ fᴰ ⋆ᴰ reind p gᴰ
+ reind-contractˡ { fᴰ = fᴰ } = fromPathP $
+ congP (λ _ → fᴰ ⋆ᴰ_ ) ( transport-filler _ _)
+
+ ≡→≡[] : { a b : C.ob } { f g : C [ a , b ] } { p : f ≡ g }
+ { aᴰ : ob[ a ] } { bᴰ : ob[ b ] }
+ { fᴰ : Hom[ f ][ aᴰ , bᴰ ] }
+ { gᴰ : Hom[ g ][ aᴰ , bᴰ ] }
+ → reind p fᴰ ≡ gᴰ → fᴰ ≡[ p ] gᴰ
+ ≡→≡[] = toPathP
+elimProp : { f g : A → B } { C : SetCoequalizer f g → Type ℓ }
- → ( Cprop : ( x : SetCoequalizer f g ) → isProp ( C x ))
+ → ( Cprop : ( x : SetCoequalizer f g ) → isProp ( C x ))
→ ( Cinc : ( b : B ) → C ( inc b ))
→ ( x : SetCoequalizer f g ) → C x
elimProp Cprop Cinc ( inc x ) = Cinc x
elimProp { f = f } { g = g } Cprop Cinc ( coeq a i ) =
- isProp→PathP (λ i → Cprop ( coeq a i )) ( Cinc ( f a )) ( Cinc ( g a )) i
+ isProp→PathP (λ i → Cprop ( coeq a i )) ( Cinc ( f a )) ( Cinc ( g a )) i
elimProp Cprop Cinc ( squash x y p q i j ) =
- isOfHLevel→isOfHLevelDep
- 2 (λ x → isProp→isSet ( Cprop x )) ( g x ) ( g y ) ( cong g p ) ( cong g q ) ( squash x y p q ) i j
+ isOfHLevel→isOfHLevelDep
+ 2 (λ x → isProp→isSet ( Cprop x )) ( g x ) ( g y ) ( cong g p ) ( cong g q ) ( squash x y p q ) i j
where
g = elimProp Cprop Cinc
elimProp2 : { A' : Type ℓ } { B' : Type ℓ' } { f g : A → B } { f' g' : A' → B' }
{ C : SetCoequalizer f g → SetCoequalizer f' g' → Type ( ℓ-max ℓ ℓ' )}
- → ( Cprop : ( x : SetCoequalizer f g ) → ( y : SetCoequalizer f' g' ) → isProp ( C x y ))
+ → ( Cprop : ( x : SetCoequalizer f g ) → ( y : SetCoequalizer f' g' ) → isProp ( C x y ))
→ ( Cinc : ( b : B ) → ( b' : B' ) → C ( inc b ) ( inc b' ))
→ ( x : SetCoequalizer f g ) → ( y : SetCoequalizer f' g' ) → C x y
elimProp2 Cprop Cinc = elimProp (λ x → isPropΠ (λ y → Cprop x y ))
@@ -51,7 +51,7 @@
→ ( Cprop : ( x : SetCoequalizer f g )
→ ( y : SetCoequalizer f' g' )
→ ( z : SetCoequalizer f'' g'' )
- → isProp ( C x y z ))
+ → isProp ( C x y z ))
→ ( Cinc : ( b : B ) → ( b' : B' ) → ( b'' : B'' ) → C ( inc b ) ( inc b' ) ( inc b'' ))
→ ( x : SetCoequalizer f g ) → ( y : SetCoequalizer f' g' ) → ( z : SetCoequalizer f'' g'' )
→ C x y z
@@ -77,7 +77,7 @@
→ SetCoequalizer f g → SetCoequalizer f' g' → C
rec2 Cset h hcoeqsl hcoeqsr =
rec
- ( isSetΠ (λ _ → Cset ))
+ ( isSetΠ (λ _ → Cset ))
(λ b → rec Cset (λ b' → h b b' ) (λ a' → hcoeqsr a' b ))
(λ a → funExt ( elimProp (λ _ → Cset _ _) (λ b' → hcoeqsl a b' )))
diff --git a/docs/Realizability.ApplicativeStructure.html b/docs/Realizability.ApplicativeStructure.html
index 8499598..7fcf1d3 100644
--- a/docs/Realizability.ApplicativeStructure.html
+++ b/docs/Realizability.ApplicativeStructure.html
@@ -1,173 +1,238 @@
-Realizability.ApplicativeStructure open import Cubical.Core.Everything
-open import Cubical.Foundations.Prelude
-open import Cubical.Foundations.HLevels
-open import Cubical.Relation.Nullary
-open import Cubical.Data.Nat
-open import Cubical.Data.Nat.Order
-open import Cubical.Data.FinData
-open import Cubical.Data.Vec
-open import Cubical.Data.Empty renaming ( elim to ⊥elim )
-open import Cubical.Tactics.NatSolver
-
-module Realizability.ApplicativeStructure where
-
-private module _ { ℓ } { A : Type ℓ } where
-
- foldlOp : ∀ { ℓ' } ( B : ℕ → Type ℓ' ) → Type _
- foldlOp B = ∀ { n } → B n → A → B ( suc n )
-
- opaque
- foldl : ∀ { ℓ' } { n : ℕ } ( B : ℕ → Type ℓ' ) → foldlOp B → B zero → Vec A n → B n
- foldl { ℓ' } { . zero } B op acc emptyVec = acc
- foldl { ℓ' } { .( suc _) } B op acc ( x ∷vec vec ) = foldl (λ n → B ( suc n )) op ( op acc x ) vec
-
- opaque
- reverse : ∀ { n } → Vec A n → Vec A n
- reverse vec = foldl (λ n → Vec A n ) (λ acc curr → curr ∷ acc ) [] vec
-
- opaque
- chain : ∀ { n } → Vec A ( suc n ) → ( A → A → A ) → A
- chain { n } ( x ∷vec vec ) op = foldl (λ _ → A ) (λ acc curr → op acc curr ) x vec
-
-record ApplicativeStructure { ℓ } ( A : Type ℓ ) : Type ℓ where
- infixl 20 _⨾_
- field
- isSetA : isSet A
- _⨾_ : A → A → A
-
-module _ { ℓ } { A : Type ℓ } ( as : ApplicativeStructure A ) where
- open ApplicativeStructure as
- infix 23 `_
- infixl 22 _̇_
- data Term ( n : ℕ ) : Type ℓ where
- # : Fin n → Term n
- `_ : A → Term n
- _̇_ : Term n → Term n → Term n
-
- ⟦_⟧ : ∀ { n } → Term n → Vec A n → A
- ⟦_⟧ ( ` a ) _ = a
- ⟦_⟧ { n } ( # k ) subs = lookup k subs
- ⟦_⟧ ( a ̇ b ) subs = ( ⟦ a ⟧ subs ) ⨾ ( ⟦ b ⟧ subs )
-
- applicationChain : ∀ { n m } → Vec ( Term m ) ( suc n ) → Term m
- applicationChain { n } { m } vec = chain vec (λ x y → x ̇ y )
-
- apply : ∀ { n } → A → Vec A n → A
- apply { n } a vec = chain ( a ∷ vec ) (λ x y → x ⨾ y )
-
- private
- opaque
- unfolding reverse
- unfolding foldl
- unfolding chain
- applyWorks : ∀ K a b → apply K ( a ∷ b ∷ [] ) ≡ K ⨾ a ⨾ b
- applyWorks K a b = refl
-
- record Feferman : Type ℓ where
- field
- s : A
- k : A
- kab≡a : ∀ a b → k ⨾ a ⨾ b ≡ a
- sabc≡ac_bc : ∀ a b c → s ⨾ a ⨾ b ⨾ c ≡ ( a ⨾ c ) ⨾ ( b ⨾ c )
-
- module ComputationRules ( feferman : Feferman ) where
- open Feferman feferman
-
- opaque
- λ*abst : ∀ { n } → ( e : Term ( suc n )) → Term n
- λ*abst { n } ( # zero ) = ` s ̇ ` k ̇ ` k
- λ*abst { n } ( # ( suc x )) = ` k ̇ # x
- λ*abst { n } ( ` x ) = ` k ̇ ` x
- λ*abst { n } ( e ̇ e₁ ) = ` s ̇ λ*abst e ̇ λ*abst e₁
-
-
-
- λ* : Term one → A
- λ* t = ⟦ λ*abst t ⟧ []
-
- λ*2 : Term two → A
- λ*2 t = ⟦ λ*abst ( λ*abst t ) ⟧ []
-
- λ*3 : Term three → A
- λ*3 t = ⟦ λ*abst ( λ*abst ( λ*abst t )) ⟧ []
-
- λ*4 : Term four → A
- λ*4 t = ⟦ λ*abst ( λ*abst ( λ*abst ( λ*abst t ))) ⟧ []
-
- opaque
- unfolding λ*abst
- βreduction : ∀ { n } → ( body : Term ( suc n )) → ( prim : A ) → ( subs : Vec A n ) → ⟦ λ*abst body ̇ ` prim ⟧ subs ≡ ⟦ body ⟧ ( prim ∷ subs )
- βreduction { n } ( # zero ) prim subs =
- s ⨾ k ⨾ k ⨾ prim
- ≡⟨ sabc≡ac_bc _ _ _ ⟩
- k ⨾ prim ⨾ ( k ⨾ prim )
- ≡⟨ kab≡a _ _ ⟩
- prim
- ∎
- βreduction { n } ( # ( suc x )) prim subs = kab≡a _ _
- βreduction { n } ( ` x ) prim subs = kab≡a _ _
- βreduction { n } ( rator ̇ rand ) prim subs =
- s ⨾ ⟦ λ*abst rator ⟧ subs ⨾ ⟦ λ*abst rand ⟧ subs ⨾ prim
- ≡⟨ sabc≡ac_bc _ _ _ ⟩
- ⟦ λ*abst rator ⟧ subs ⨾ prim ⨾ ( ⟦ λ*abst rand ⟧ subs ⨾ prim )
- ≡⟨ cong₂ (λ x y → x ⨾ y ) ( βreduction rator prim subs ) ( βreduction rand prim subs ) ⟩
- ⟦ rator ⟧ ( prim ∷ subs ) ⨾ ⟦ rand ⟧ ( prim ∷ subs )
- ∎
-
- λ*chainTerm : ∀ n → Term n → Term zero
- λ*chainTerm zero t = t
- λ*chainTerm ( suc n ) t = λ*chainTerm n ( λ*abst t )
-
- λ*chain : ∀ { n } → Term n → A
- λ*chain { n } t = ⟦ λ*chainTerm n t ⟧ []
-
- opaque
- unfolding reverse
- unfolding foldl
- unfolding chain
-
- λ*ComputationRule : ∀ ( t : Term 1 ) ( a : A ) → λ* t ⨾ a ≡ ⟦ t ⟧ ( a ∷ [] )
- λ*ComputationRule t a =
- ⟦ λ*abst t ⟧ [] ⨾ a
- ≡⟨ βreduction t a [] ⟩
- ⟦ t ⟧ ( a ∷ [] )
- ∎
-
- λ*2ComputationRule : ∀ ( t : Term 2 ) ( a b : A ) → λ*2 t ⨾ a ⨾ b ≡ ⟦ t ⟧ ( b ∷ a ∷ [] )
- λ*2ComputationRule t a b =
- ⟦ λ*abst ( λ*abst t ) ⟧ [] ⨾ a ⨾ b
- ≡⟨ refl ⟩
- ⟦ λ*abst ( λ*abst t ) ⟧ [] ⨾ ⟦ ` a ⟧ [] ⨾ ⟦ ` b ⟧ []
- ≡⟨ refl ⟩
- ⟦ λ*abst ( λ*abst t ) ̇ ` a ⟧ [] ⨾ ⟦ ` b ⟧ []
- ≡⟨ cong (λ x → x ⨾ b ) ( βreduction ( λ*abst t ) a [] ) ⟩
- ⟦ λ*abst t ⟧ ( a ∷ [] ) ⨾ b
- ≡⟨ βreduction t b ( a ∷ [] ) ⟩
- ⟦ t ⟧ ( b ∷ a ∷ [] )
- ∎
+Realizability.ApplicativeStructure ---
+title: Applicative Structure
+author: Rahul Chhabra
+---
+# Applicative Structure
+
+In this module we define the notion of an _applicative structure_.
+
+A type $A$ has applicative structure if it has an "application operation" (here represented by `_⨾_`) and is a set.
+
+<details>
+ ```agda
+ open import Cubical.Core.Everything
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.Relation.Nullary
+open import Cubical.Data.Nat
+open import Cubical.Data.Nat.Order
+open import Cubical.Data.FinData
+open import Cubical.Data.Vec
+open import Cubical.Data.Empty renaming ( elim to ⊥elim )
+open import Cubical.Tactics.NatSolver
+
+module Realizability.ApplicativeStructure where
+
+private module _ { ℓ } { A : Type ℓ } where
+
+ foldlOp : ∀ { ℓ' } ( B : ℕ → Type ℓ' ) → Type _
+ foldlOp B = ∀ { n } → B n → A → B ( suc n )
+
+ opaque
+ foldl : ∀ { ℓ' } { n : ℕ } ( B : ℕ → Type ℓ' ) → foldlOp B → B zero → Vec A n → B n
+ foldl { ℓ' } { . zero } B op acc emptyVec = acc
+ foldl { ℓ' } { .( suc _) } B op acc ( x ∷vec vec ) = foldl (λ n → B ( suc n )) op ( op acc x ) vec
+
+ opaque
+ reverse : ∀ { n } → Vec A n → Vec A n
+ reverse vec = foldl (λ n → Vec A n ) (λ acc curr → curr ∷ acc ) [] vec
+
+ opaque
+ chain : ∀ { n } → Vec A ( suc n ) → ( A → A → A ) → A
+ chain { n } ( x ∷vec vec ) op = foldl (λ _ → A ) (λ acc curr → op acc curr ) x vec
+```
+ </details>
+
+ ```agda
+ record ApplicativeStructure { ℓ } ( A : Type ℓ ) : Type ℓ where
+ infixl 20 _⨾_
+ field
+ isSetA : isSet A
+ _⨾_ : A → A → A
+```
+
+Since being a set is a property - we will generally not have to think about it too much. Also, since `A` is a set - we can drop the relevance of paths and simply talk about "equality".
+
+We can define the notion of a term over an applicative structure.
+ ```agda
+ module _ { ℓ } { A : Type ℓ } ( as : ApplicativeStructure A ) where
+ open ApplicativeStructure as
+ infix 23 `_
+ infixl 22 _̇_
+ data Term ( n : ℕ ) : Type ℓ where
+ # : Fin n → Term n
+ `_ : A → Term n
+ _̇_ : Term n → Term n → Term n
+```
+
+These terms can be evaluated into $A$ if we can give the values of the free variables.
+
+ ```agda
+ ⟦_⟧ : ∀ { n } → Term n → Vec A n → A
+ ⟦_⟧ ( ` a ) _ = a
+ ⟦_⟧ { n } ( # k ) subs = lookup k subs
+ ⟦_⟧ ( a ̇ b ) subs = ( ⟦ a ⟧ subs ) ⨾ ( ⟦ b ⟧ subs )
+
+ applicationChain : ∀ { n m } → Vec ( Term m ) ( suc n ) → Term m
+ applicationChain { n } { m } vec = chain vec (λ x y → x ̇ y )
+
+ apply : ∀ { n } → A → Vec A n → A
+ apply { n } a vec = chain ( a ∷ vec ) (λ x y → x ⨾ y )
+```
+
+<details>
+ ```agda
+ private
+ opaque
+ unfolding reverse
+ unfolding foldl
+ unfolding chain
+ applyWorks : ∀ K a b → apply K ( a ∷ b ∷ [] ) ≡ K ⨾ a ⨾ b
+ applyWorks K a b = refl
+```
+ </details>
+
+On an applicative structure we can define Feferman structure (or SK structure). We call an applicative structure endowed with Feferman structure a **combinatory algebra**.
+
+ ```agda
+ record Feferman : Type ℓ where
+ field
+ s : A
+ k : A
+ kab≡a : ∀ a b → k ⨾ a ⨾ b ≡ a
+ sabc≡ac_bc : ∀ a b c → s ⨾ a ⨾ b ⨾ c ≡ ( a ⨾ c ) ⨾ ( b ⨾ c )
+```
+
+Feferman structure allows us to construct **combinatorial completeness** structure.
+
+Imagine we have a term `t : Term n` (for some `n : ℕ`). We can ask if `A` has a "copy" of `t` so that application would correspond to subsitution. That is, we may ask if we can find an `a : A` such that
+`a ⨾ < a¹ ⨾ a² ⨾ .... ⨾ aⁿ >` (here the `< ... >` notation represents a chain of applications) would be equal to `t [a¹ / # 0 , a² / # 1 , .... , aⁿ / # (pred n) ]`. If the applicative structure additionally can be endowed with Feferman structure - then the answer is yes.
+
+To get to such a term, we first need to define a function that takes `Term (suc n)` to `Term n` by "abstracting" the free variable represented by the index `# 0`.
+
+We will call this `λ*abst` and this will turn out to behave very similar to λ abstraction - and we will also show that it validates a kind of β reduction rule.
+
+ ```agda
+ module ComputationRules ( feferman : Feferman ) where
+ open Feferman feferman
+
+ opaque
+ λ*abst : ∀ { n } → ( e : Term ( suc n )) → Term n
+ λ*abst { n } ( # zero ) = ` s ̇ ` k ̇ ` k
+ λ*abst { n } ( # ( suc x )) = ` k ̇ # x
+ λ*abst { n } ( ` x ) = ` k ̇ ` x
+ λ*abst { n } ( e ̇ e₁ ) = ` s ̇ λ*abst e ̇ λ*abst e₁
+```
+
+**Remark** : It is important to note that in general, realizability is developed using **partial combinatory algebras** and **partial applicative structures**. In this case, `λ*abst` is not particularly well-behaved. The β reduction-esque rule we derive also does not behave *completely* like β reduction. See Jonh Longley's PhD thesis "Realizability Toposes and Language Semantics" Theorem 1.1.9.
+
+**Remark** : We declare the definition as `opaque` - this is important. If we let Agda unfold this definition all the way we ocassionally end up with unreadable goals containing a mess of `s` and `k`.
+
+We define meta-syntactic sugar for some of the more common cases :
+
+ ```agda
+ λ* : Term one → A
+ λ* t = ⟦ λ*abst t ⟧ []
+
+ λ*2 : Term two → A
+ λ*2 t = ⟦ λ*abst ( λ*abst t ) ⟧ []
+
+ λ*3 : Term three → A
+ λ*3 t = ⟦ λ*abst ( λ*abst ( λ*abst t )) ⟧ []
+
+ λ*4 : Term four → A
+ λ*4 t = ⟦ λ*abst ( λ*abst ( λ*abst ( λ*abst t ))) ⟧ []
+```
+
+We now show that we have a β-reduction-esque operation. We proceed by induction on the structure of the term and the number of free variables.
+
+For the particular combinatory algebra Λ/β (terms of the untyped λ calculus quotiented by β equality) - this β reduction actually coincides with the "actual" β reduction.
+TODO : Prove this.
+
+ ```agda
+ opaque
+ unfolding λ*abst
+ βreduction : ∀ { n } → ( body : Term ( suc n )) → ( prim : A ) → ( subs : Vec A n ) → ⟦ λ*abst body ̇ ` prim ⟧ subs ≡ ⟦ body ⟧ ( prim ∷ subs )
+ βreduction { n } ( # zero ) prim subs =
+ s ⨾ k ⨾ k ⨾ prim
+ ≡⟨ sabc≡ac_bc _ _ _ ⟩
+ k ⨾ prim ⨾ ( k ⨾ prim )
+ ≡⟨ kab≡a _ _ ⟩
+ prim
+ ∎
+ βreduction { n } ( # ( suc x )) prim subs = kab≡a _ _
+ βreduction { n } ( ` x ) prim subs = kab≡a _ _
+ βreduction { n } ( rator ̇ rand ) prim subs =
+ s ⨾ ⟦ λ*abst rator ⟧ subs ⨾ ⟦ λ*abst rand ⟧ subs ⨾ prim
+ ≡⟨ sabc≡ac_bc _ _ _ ⟩
+ ⟦ λ*abst rator ⟧ subs ⨾ prim ⨾ ( ⟦ λ*abst rand ⟧ subs ⨾ prim )
+ ≡⟨ cong₂ (λ x y → x ⨾ y ) ( βreduction rator prim subs ) ( βreduction rand prim subs ) ⟩
+ ⟦ rator ⟧ ( prim ∷ subs ) ⨾ ⟦ rand ⟧ ( prim ∷ subs )
+ ∎
+```
+
+<details>
+ ```agda
+ λ*chainTerm : ∀ n → Term n → Term zero
+ λ*chainTerm zero t = t
+ λ*chainTerm ( suc n ) t = λ*chainTerm n ( λ*abst t )
+
+ λ*chain : ∀ { n } → Term n → A
+ λ*chain { n } t = ⟦ λ*chainTerm n t ⟧ []
+```
+ </details>
+
+We provide useful reasoning combinators that are useful and frequent.
+
+ ```agda
+ opaque
+ unfolding reverse
+ unfolding foldl
+ unfolding chain
+
+ λ*ComputationRule : ∀ ( t : Term 1 ) ( a : A ) → λ* t ⨾ a ≡ ⟦ t ⟧ ( a ∷ [] )
+ λ*ComputationRule t a =
+ ⟦ λ*abst t ⟧ [] ⨾ a
+ ≡⟨ βreduction t a [] ⟩
+ ⟦ t ⟧ ( a ∷ [] )
+ ∎
+
+ λ*2ComputationRule : ∀ ( t : Term 2 ) ( a b : A ) → λ*2 t ⨾ a ⨾ b ≡ ⟦ t ⟧ ( b ∷ a ∷ [] )
+ λ*2ComputationRule t a b =
+ ⟦ λ*abst ( λ*abst t ) ⟧ [] ⨾ a ⨾ b
+ ≡⟨ refl ⟩
+ ⟦ λ*abst ( λ*abst t ) ⟧ [] ⨾ ⟦ ` a ⟧ [] ⨾ ⟦ ` b ⟧ []
+ ≡⟨ refl ⟩
+ ⟦ λ*abst ( λ*abst t ) ̇ ` a ⟧ [] ⨾ ⟦ ` b ⟧ []
+ ≡⟨ cong (λ x → x ⨾ b ) ( βreduction ( λ*abst t ) a [] ) ⟩
+ ⟦ λ*abst t ⟧ ( a ∷ [] ) ⨾ b
+ ≡⟨ βreduction t b ( a ∷ [] ) ⟩
+ ⟦ t ⟧ ( b ∷ a ∷ [] )
+ ∎
- λ*3ComputationRule : ∀ ( t : Term 3 ) ( a b c : A ) → λ*3 t ⨾ a ⨾ b ⨾ c ≡ ⟦ t ⟧ ( c ∷ b ∷ a ∷ [] )
- λ*3ComputationRule t a b c =
- ⟦ λ*abst ( λ*abst ( λ*abst t )) ⟧ [] ⨾ ⟦ ` a ⟧ [] ⨾ ⟦ ` b ⟧ [] ⨾ ⟦ ` c ⟧ []
- ≡⟨ cong (λ x → x ⨾ b ⨾ c ) ( βreduction ( λ*abst ( λ*abst t )) a [] ) ⟩
- ⟦ λ*abst ( λ*abst t ) ⟧ ( a ∷ [] ) ⨾ ⟦ ` b ⟧ ( a ∷ [] ) ⨾ ⟦ ` c ⟧ ( a ∷ [] )
- ≡⟨ cong (λ x → x ⨾ c ) ( βreduction ( λ*abst t ) b ( a ∷ [] )) ⟩
- ⟦ λ*abst t ⟧ ( b ∷ a ∷ [] ) ⨾ ⟦ ` c ⟧ ( b ∷ a ∷ [] )
- ≡⟨ βreduction t c ( b ∷ a ∷ [] ) ⟩
- ⟦ t ⟧ ( c ∷ b ∷ a ∷ [] )
- ∎
-
- λ*4ComputationRule : ∀ ( t : Term 4 ) ( a b c d : A ) → λ*4 t ⨾ a ⨾ b ⨾ c ⨾ d ≡ ⟦ t ⟧ ( d ∷ c ∷ b ∷ a ∷ [] )
- λ*4ComputationRule t a b c d =
- ⟦ λ*abst ( λ*abst ( λ*abst ( λ*abst t ))) ⟧ [] ⨾ ⟦ ` a ⟧ [] ⨾ ⟦ ` b ⟧ [] ⨾ ⟦ ` c ⟧ [] ⨾ ⟦ ` d ⟧ []
- ≡⟨ cong (λ x → x ⨾ b ⨾ c ⨾ d ) ( βreduction ( λ*abst ( λ*abst ( λ*abst t ))) a [] ) ⟩
- ⟦ λ*abst ( λ*abst ( λ*abst t )) ⟧ ( a ∷ [] ) ⨾ ⟦ ` b ⟧ ( a ∷ [] ) ⨾ ⟦ ` c ⟧ ( a ∷ [] ) ⨾ ⟦ ` d ⟧ ( a ∷ [] )
- ≡⟨ cong (λ x → x ⨾ c ⨾ d ) ( βreduction ( λ*abst ( λ*abst t )) b ( a ∷ [] )) ⟩
- ⟦ λ*abst ( λ*abst t ) ⟧ ( b ∷ a ∷ [] ) ⨾ ⟦ ` c ⟧ ( b ∷ a ∷ [] ) ⨾ ⟦ ` d ⟧ ( b ∷ a ∷ [] )
- ≡⟨ cong (λ x → x ⨾ d ) ( βreduction ( λ*abst t ) c ( b ∷ a ∷ [] )) ⟩
- ⟦ λ*abst t ⟧ ( c ∷ b ∷ a ∷ [] ) ⨾ ⟦ ` d ⟧ ( c ∷ b ∷ a ∷ [] )
- ≡⟨ βreduction t d ( c ∷ b ∷ a ∷ [] ) ⟩
- ⟦ t ⟧ ( d ∷ c ∷ b ∷ a ∷ [] )
- ∎
-λ*3ComputationRule : ∀ ( t : Term 3 ) ( a b c : A ) → λ*3 t ⨾ a ⨾ b ⨾ c ≡ ⟦ t ⟧ ( c ∷ b ∷ a ∷ [] )
+ λ*3ComputationRule t a b c =
+ ⟦ λ*abst ( λ*abst ( λ*abst t )) ⟧ [] ⨾ ⟦ ` a ⟧ [] ⨾ ⟦ ` b ⟧ [] ⨾ ⟦ ` c ⟧ []
+ ≡⟨ cong (λ x → x ⨾ b ⨾ c ) ( βreduction ( λ*abst ( λ*abst t )) a [] ) ⟩
+ ⟦ λ*abst ( λ*abst t ) ⟧ ( a ∷ [] ) ⨾ ⟦ ` b ⟧ ( a ∷ [] ) ⨾ ⟦ ` c ⟧ ( a ∷ [] )
+ ≡⟨ cong (λ x → x ⨾ c ) ( βreduction ( λ*abst t ) b ( a ∷ [] )) ⟩
+ ⟦ λ*abst t ⟧ ( b ∷ a ∷ [] ) ⨾ ⟦ ` c ⟧ ( b ∷ a ∷ [] )
+ ≡⟨ βreduction t c ( b ∷ a ∷ [] ) ⟩
+ ⟦ t ⟧ ( c ∷ b ∷ a ∷ [] )
+ ∎
+
+ λ*4ComputationRule : ∀ ( t : Term 4 ) ( a b c d : A ) → λ*4 t ⨾ a ⨾ b ⨾ c ⨾ d ≡ ⟦ t ⟧ ( d ∷ c ∷ b ∷ a ∷ [] )
+ λ*4ComputationRule t a b c d =
+ ⟦ λ*abst ( λ*abst ( λ*abst ( λ*abst t ))) ⟧ [] ⨾ ⟦ ` a ⟧ [] ⨾ ⟦ ` b ⟧ [] ⨾ ⟦ ` c ⟧ [] ⨾ ⟦ ` d ⟧ []
+ ≡⟨ cong (λ x → x ⨾ b ⨾ c ⨾ d ) ( βreduction ( λ*abst ( λ*abst ( λ*abst t ))) a [] ) ⟩
+ ⟦ λ*abst ( λ*abst ( λ*abst t )) ⟧ ( a ∷ [] ) ⨾ ⟦ ` b ⟧ ( a ∷ [] ) ⨾ ⟦ ` c ⟧ ( a ∷ [] ) ⨾ ⟦ ` d ⟧ ( a ∷ [] )
+ ≡⟨ cong (λ x → x ⨾ c ⨾ d ) ( βreduction ( λ*abst ( λ*abst t )) b ( a ∷ [] )) ⟩
+ ⟦ λ*abst ( λ*abst t ) ⟧ ( b ∷ a ∷ [] ) ⨾ ⟦ ` c ⟧ ( b ∷ a ∷ [] ) ⨾ ⟦ ` d ⟧ ( b ∷ a ∷ [] )
+ ≡⟨ cong (λ x → x ⨾ d ) ( βreduction ( λ*abst t ) c ( b ∷ a ∷ [] )) ⟩
+ ⟦ λ*abst t ⟧ ( c ∷ b ∷ a ∷ [] ) ⨾ ⟦ ` d ⟧ ( c ∷ b ∷ a ∷ [] )
+ ≡⟨ βreduction t d ( c ∷ b ∷ a ∷ [] ) ⟩
+ ⟦ t ⟧ ( d ∷ c ∷ b ∷ a ∷ [] )
+ ∎
+```
+ open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Structure
-open import Cubical.Data.Sigma
-open import Cubical.HITs.PropositionalTruncation
-open import Cubical.Reflection.RecordEquiv
-open import Realizability.CombinatoryAlgebra
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Univalence
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Functions.FunExtEquiv
+open import Cubical.Data.Sigma
+open import Cubical.HITs.PropositionalTruncation
+open import Cubical.Reflection.RecordEquiv
+open import Realizability.CombinatoryAlgebra
-module Realizability.Assembly.Base { ℓ } { A : Type ℓ } ( ca : CombinatoryAlgebra A ) where
- record Assembly ( X : Type ℓ ) : Type ( ℓ-suc ℓ ) where
- infix 25 _⊩_
- field
- isSetX : isSet X
- _⊩_ : A → X → Type ℓ
- ⊩isPropValued : ∀ a x → isProp ( a ⊩ x )
- ⊩surjective : ∀ x → ∃[ a ∈ A ] a ⊩ x
+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 ℓ
+ isSetX : isSet X
+ ⊩isPropValued : ∀ a x → isProp ( a ⊩ x )
+ ⊩surjective : ∀ x → ∃[ a ∈ A ] a ⊩ x
+ open Assembly public
+ _⊩[_]_ : ∀ { X : Type ℓ } → A → Assembly X → X → Type ℓ
+ a ⊩[ A ] x = A . _⊩_ a x
- AssemblyΣ : Type ℓ → Type _
- AssemblyΣ X =
- Σ[ isSetX ∈ isSet X ]
- Σ[ _⊩_ ∈ ( A → X → hProp ℓ ) ]
- (∀ x → ∃[ a ∈ A ] ⟨ a ⊩ x ⟩ )
+ AssemblyΣ : Type ℓ → Type _
+ AssemblyΣ X =
+ Σ[ _⊩_ ∈ ( A → X → hProp ℓ ) ]
+ (∀ x → ∃[ a ∈ A ] ⟨ a ⊩ x ⟩ ) ×
+ ( isSet X )
- AssemblyΣX→isSetX : ∀ X → AssemblyΣ X → isSet X
- AssemblyΣX→isSetX X ( isSetX , _ , _) = isSetX
-
- AssemblyΣX→⊩ : ∀ X → AssemblyΣ X → ( A → X → hProp ℓ )
- AssemblyΣX→⊩ X (_ , ⊩ , _) = ⊩
-
- AssemblyΣX→⊩surjective : ∀ X → ( asm : AssemblyΣ X ) → (∀ x → ∃[ a ∈ A ] ⟨ AssemblyΣX→⊩ X asm a x ⟩ )
- AssemblyΣX→⊩surjective X (_ , _ , ⊩surjective ) = ⊩surjective
-
- isSetAssemblyΣ : ∀ X → isSet ( AssemblyΣ X )
- isSetAssemblyΣ X = isSetΣ ( isProp→isSet isPropIsSet ) λ isSetX → isSetΣ ( isSetΠ (λ a → isSetΠ λ x → isSetHProp )) λ _⊩_ → isSetΠ λ x → isProp→isSet isPropPropTrunc
+ isSetAssemblyΣ : ∀ X → isSet ( AssemblyΣ X )
+ isSetAssemblyΣ X = isSetΣ ( isSetΠ2 λ _ _ → isSetHProp ) (λ rel → isSet× ( isSetΠ λ x → isProp→isSet isPropPropTrunc ) ( isProp→isSet isPropIsSet ))
- unquoteDecl AssemblyIsoΣ = declareRecordIsoΣ AssemblyIsoΣ ( quote Assembly )
+ AssemblyΣ≡Equiv : ∀ X → ( a b : AssemblyΣ X ) → ( a ≡ b ) ≃ (∀ r x → ⟨ a . fst r x ⟩ ≃ ⟨ b . fst r x ⟩ )
+ AssemblyΣ≡Equiv X a b =
+ a ≡ b
+ ≃⟨ invEquiv ( Σ≡PropEquiv (λ rel → isProp× ( isPropΠ λ x → isPropPropTrunc ) isPropIsSet ) { u = a } { v = b }) ⟩
+ a . fst ≡ b . fst
+ ≃⟨ invEquiv ( funExt₂Equiv { f = a . fst } { g = b . fst }) ⟩
+ (∀ ( r : A ) ( x : X ) → a . fst r x ≡ b . fst r x )
+ ≃⟨
+ equivΠCod
+ (λ r →
+ equivΠCod
+ λ x →
+ compEquiv
+ ( invEquiv ( Σ≡PropEquiv (λ _ → isPropIsProp ) { u = a . fst r x } { v = b . fst r x }))
+ ( univalence { A = a . fst r x . fst } { B = b . fst r x . fst }))
+ ⟩
+ (∀ ( r : A ) ( x : X ) → ⟨ a . fst r x ⟩ ≃ ⟨ b . fst r x ⟩ )
+ ■
- open Assembly public
+
+ AssemblyΣIsoAssembly : ∀ X → Iso ( AssemblyΣ X ) ( Assembly X )
+ _⊩_ ( Iso.fun ( AssemblyΣIsoAssembly X ) ( rel , surj , isSetX )) a x = ⟨ rel a x ⟩
+ Assembly.isSetX ( Iso.fun ( AssemblyΣIsoAssembly X ) ( rel , surj , isSetX )) = isSetX
+ ⊩isPropValued ( Iso.fun ( AssemblyΣIsoAssembly X ) ( rel , surj , isSetX )) a x = str ( rel a x )
+ ⊩surjective ( Iso.fun ( AssemblyΣIsoAssembly X ) ( rel , surj , isSetX )) x = surj x
+ Iso.inv ( AssemblyΣIsoAssembly X ) asm = (λ a x → ( a ⊩[ asm ] x ) , ( asm . ⊩isPropValued a x )) , (λ x → asm . ⊩surjective x ) , asm . isSetX
+ Iso.rightInv ( AssemblyΣIsoAssembly X ) asm = refl
+ Iso.leftInv ( AssemblyΣIsoAssembly X ) ( rel , surj , isSetX ) = refl
-
+ AssemblyΣ≃Assembly : ∀ X → AssemblyΣ X ≃ Assembly X
+ AssemblyΣ≃Assembly X = isoToEquiv ( AssemblyΣIsoAssembly X )
+
+ isSetAssembly : ∀ X → isSet ( Assembly X )
+ isSetAssembly X = isOfHLevelRespectEquiv 2 ( AssemblyΣ≃Assembly X ) ( isSetAssemblyΣ X )