Dependent type theories
{-# OPTIONS --guardedness #-} module type-theories.dependent-type-theories where
Imports
open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.functions open import foundation.homotopies open import foundation.identity-types open import foundation.propositions open import foundation.universe-levels
Idea
We introduce the cagegory of dependent type theories, following Voevodsky's notion of -systems. The category of generalised algebraic theories is defined to be this category. It should be equivalent to the category of essentially algebraic theories.
(Dependency) systems
(Dependency) systems are the structure around which a dependent type theory is built.
Ã₀ Ã₁ Ã₂
| | |
| | |
V V V
A₀ <---- A₁ <---- A₂ <---- ⋯
module dependent where record system (l1 l2 : Level) : UU (lsuc l1 ⊔ lsuc l2) where coinductive field type : UU l1 element : type → UU l2 slice : (X : type) → system l1 l2 record fibered-system {l1 l2 : Level} (l3 l4 : Level) (A : system l1 l2) : UU (l1 ⊔ l2 ⊔ lsuc l3 ⊔ lsuc l4) where coinductive field type : system.type A → UU l3 element : {X : system.type A} → type X → system.element A X → UU l4 slice : {X : system.type A} → type X → fibered-system l3 l4 (system.slice A X) record section-system {l1 l2 l3 l4 : Level} {A : system l1 l2} (B : fibered-system l3 l4 A) : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) where coinductive field type : (X : system.type A) → fibered-system.type B X element : {X : system.type A} (x : system.element A X) → fibered-system.element B (type X) x slice : (X : system.type A) → section-system (fibered-system.slice B (type X))
Heterogeneous homotopies of sections of fibered systems
will introduce homotopies of sections of fibered systems. However, in order to define concatenation of those homotopies, we will first define heterogeneous homotopies of sections of fibered systems.
tr-fibered-system-slice : {l1 l2 l3 l4 : Level} {A : system l1 l2} {B B' : fibered-system l3 l4 A} (α : Id B B') (f : section-system B) (X : system.type A) → Id ( fibered-system.slice B (section-system.type f X)) ( fibered-system.slice B' ( section-system.type (tr section-system α f) X)) tr-fibered-system-slice refl f X = refl Eq-fibered-system' : {l1 l2 l3 l4 : Level} {A : system l1 l2} {B B' : fibered-system l3 l4 A} (α : Id B B') (f : section-system B) (g : section-system B') → fibered-system l3 l4 A fibered-system.type (Eq-fibered-system' {A = A} α f g) X = Id ( section-system.type (tr section-system α f) X) ( section-system.type g X) fibered-system.element (Eq-fibered-system' {A = A} {B} {B'} α f g) p x = Id ( tr (λ t → fibered-system.element B' t x) ( p) ( section-system.element (tr section-system α f) x)) ( section-system.element g x) fibered-system.slice (Eq-fibered-system' {A = A} {B} {B'} α f g) {X} p = Eq-fibered-system' ( tr-fibered-system-slice α f X ∙ ap (fibered-system.slice B') p) ( section-system.slice f X) ( section-system.slice g X) htpy-section-system' : {l1 l2 l3 l4 : Level} {A : system l1 l2} {B B' : fibered-system l3 l4 A} (α : Id B B') (f : section-system B) (g : section-system B') → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) htpy-section-system' {A = A} α f g = section-system (Eq-fibered-system' α f g) concat-htpy-section-system' : {l1 l2 l3 l4 : Level} {A : system l1 l2} {B B' B'' : fibered-system l3 l4 A} {α : Id B B'} {β : Id B' B''} (γ : Id B B'') (δ : Id (α ∙ β) γ) {f : section-system B} {g : section-system B'} {h : section-system B''} (G : htpy-section-system' α f g) (H : htpy-section-system' β g h) → htpy-section-system' γ f h section-system.type ( concat-htpy-section-system' {α = refl} {refl} refl refl G H) = section-system.type G ∙h section-system.type H section-system.element ( concat-htpy-section-system' {B = B} {α = refl} {refl} refl refl {f} G H) {X} x = ( tr-concat { B = λ t → fibered-system.element B t x} ( section-system.type G X) ( section-system.type H X) ( section-system.element f x)) ∙ ( ( ap ( tr ( λ t → fibered-system.element B t x) ( section-system.type H X)) ( section-system.element G x)) ∙ ( section-system.element H x)) section-system.slice ( concat-htpy-section-system' {B = B} {α = refl} {refl} refl refl G H) X = concat-htpy-section-system' ( ap ( fibered-system.slice B) ( section-system.type G X ∙ section-system.type H X)) ( inv ( ap-concat ( fibered-system.slice B) ( section-system.type G X) ( section-system.type H X))) ( section-system.slice G X) ( section-system.slice H X) inv-htpy-section-system' : {l1 l2 l3 l4 : Level} {A : system l1 l2} {B B' : fibered-system l3 l4 A} {α : Id B B'} (β : Id B' B) (γ : Id (inv α) β) {f : section-system B} {g : section-system B'} → htpy-section-system' α f g → htpy-section-system' β g f section-system.type (inv-htpy-section-system' {α = refl} .refl refl H) X = inv (section-system.type H X) section-system.element ( inv-htpy-section-system' {α = refl} .refl refl H) {X} x = eq-transpose-tr ( section-system.type H X) ( inv (section-system.element H x)) section-system.slice ( inv-htpy-section-system' {B = B} {α = refl} .refl refl H) X = inv-htpy-section-system' ( ap (fibered-system.slice B) (inv (section-system.type H X))) ( inv (ap-inv (fibered-system.slice B) (section-system.type H X))) ( section-system.slice H X)
Nonhomogenous homotopies
We specialize the above definitions to nonhomogenous homotopies.
htpy-section-system : {l1 l2 l3 l4 : Level} {A : system l1 l2} {B : fibered-system l3 l4 A} (f g : section-system B) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) htpy-section-system {A = A} {B} f g = htpy-section-system' refl f g refl-htpy-section-system : {l1 l2 l3 l4 : Level} {A : system l1 l2} {B : fibered-system l3 l4 A} (f : section-system B) → htpy-section-system f f section-system.type (refl-htpy-section-system f) X = refl section-system.element (refl-htpy-section-system f) x = refl section-system.slice (refl-htpy-section-system f) X = refl-htpy-section-system (section-system.slice f X) concat-htpy-section-system : {l1 l2 l3 l4 : Level} {A : system l1 l2} {B : fibered-system l3 l4 A} {f g h : section-system B} (G : htpy-section-system f g) (H : htpy-section-system g h) → htpy-section-system f h concat-htpy-section-system G H = concat-htpy-section-system' refl refl G H inv-htpy-section-system : {l1 l2 l3 l4 : Level} {A : system l1 l2} {B : fibered-system l3 l4 A} {f g : section-system B} (H : htpy-section-system f g) → htpy-section-system g f inv-htpy-section-system H = inv-htpy-section-system' refl refl H
total system of a fibered dependency system
total-system : {l1 l2 l3 l4 : Level} (A : system l1 l2) (B : fibered-system l3 l4 A) → system (l1 ⊔ l3) (l2 ⊔ l4) system.type (total-system A B) = Σ (system.type A) (fibered-system.type B) system.element (total-system A B) (pair X Y) = Σ (system.element A X) (fibered-system.element B Y) system.slice (total-system A B) (pair X Y) = total-system (system.slice A X) (fibered-system.slice B Y)
Morphisms of systems
constant-fibered-system : {l1 l2 l3 l4 : Level} (A : system l1 l2) (B : system l3 l4) → fibered-system l3 l4 A fibered-system.type (constant-fibered-system A B) X = system.type B fibered-system.element (constant-fibered-system A B) Y x = system.element B Y fibered-system.slice (constant-fibered-system A B) {X} Y = constant-fibered-system (system.slice A X) (system.slice B Y) hom-system : {l1 l2 l3 l4 : Level} (A : system l1 l2) (B : system l3 l4) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) hom-system A B = section-system (constant-fibered-system A B)
Homotopies of morphisms of systems
Homotopies of morphisms of systems are defined as an instance of homotopies of sections of fibered systems.
htpy-hom-system : {l1 l2 l3 l4 : Level} {A : system l1 l2} {B : system l3 l4} (f g : hom-system A B) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) htpy-hom-system f g = htpy-section-system f g refl-htpy-hom-system : {l1 l2 l3 l4 : Level} {A : system l1 l2} {B : system l3 l4} (f : hom-system A B) → htpy-hom-system f f refl-htpy-hom-system f = refl-htpy-section-system f concat-htpy-hom-system : {l1 l2 l3 l4 : Level} {A : system l1 l2} {B : system l3 l4} {f g h : hom-system A B} → htpy-hom-system f g → htpy-hom-system g h → htpy-hom-system f h concat-htpy-hom-system G H = concat-htpy-section-system G H inv-htpy-hom-system : {l1 l2 l3 l4 : Level} {A : system l1 l2} {B : system l3 l4} {f g : hom-system A B} → htpy-hom-system f g → htpy-hom-system g f inv-htpy-hom-system H = inv-htpy-section-system H
The category of systems
We show that systems form a category.
id-hom-system : {l1 l2 : Level} (A : system l1 l2) → hom-system A A section-system.type (id-hom-system A) X = X section-system.element (id-hom-system A) x = x section-system.slice (id-hom-system A) X = id-hom-system (system.slice A X) comp-hom-system : {l1 l2 l3 l4 l5 l6 : Level} {A : system l1 l2} {B : system l3 l4} {C : system l5 l6} (g : hom-system B C) (f : hom-system A B) → hom-system A C section-system.type (comp-hom-system g f) = section-system.type g ∘ section-system.type f section-system.element (comp-hom-system g f) = ( section-system.element g) ∘ (section-system.element f) section-system.slice (comp-hom-system g f) X = comp-hom-system ( section-system.slice g (section-system.type f X)) ( section-system.slice f X) left-unit-law-comp-hom-system : {l1 l2 l3 l4 : Level} {A : system l1 l2} {B : system l3 l4} (f : hom-system A B) → htpy-hom-system (comp-hom-system (id-hom-system B) f) f section-system.type (left-unit-law-comp-hom-system f) = refl-htpy section-system.element (left-unit-law-comp-hom-system f) = refl-htpy section-system.slice (left-unit-law-comp-hom-system f) X = left-unit-law-comp-hom-system (section-system.slice f X) right-unit-law-comp-hom-system : {l1 l2 l3 l4 : Level} {A : system l1 l2} {B : system l3 l4} (f : hom-system A B) → htpy-hom-system (comp-hom-system f (id-hom-system A)) f section-system.type (right-unit-law-comp-hom-system f) = refl-htpy section-system.element (right-unit-law-comp-hom-system f) = refl-htpy section-system.slice (right-unit-law-comp-hom-system f) X = right-unit-law-comp-hom-system (section-system.slice f X) associative-comp-hom-system : {l1 l2 l3 l4 l5 l6 l7 l8 : Level} {A : system l1 l2} {B : system l3 l4} {C : system l5 l6} {D : system l7 l8} (h : hom-system C D) (g : hom-system B C) (f : hom-system A B) → htpy-hom-system ( comp-hom-system (comp-hom-system h g) f) ( comp-hom-system h (comp-hom-system g f)) section-system.type (associative-comp-hom-system h g f) = refl-htpy section-system.element (associative-comp-hom-system h g f) = refl-htpy section-system.slice (associative-comp-hom-system h g f) X = associative-comp-hom-system ( section-system.slice h ( section-system.type g (section-system.type f X))) ( section-system.slice g ( section-system.type f X)) ( section-system.slice f X) left-whisker-htpy-hom-system' : {l1 l2 l3 l4 l5 l6 : Level} {A : system l1 l2} {B B' : system l3 l4} {C C' : system l5 l6} {g : hom-system B C} {g' : hom-system B' C'} (p : Id B B') {p' : Id (constant-fibered-system A B) (constant-fibered-system A B')} (α : Id (ap (constant-fibered-system A) p) p') (q : Id C C') {q' : Id (constant-fibered-system A C) (constant-fibered-system A C')} (β : Id (ap (constant-fibered-system A) q) q') (r : Id (tr (λ t → t) (ap-binary hom-system p q) g) g') {f : hom-system A B} {f' : hom-system A B'} → htpy-section-system' p' f f' → htpy-section-system' q' (comp-hom-system g f) (comp-hom-system g' f') section-system.type ( left-whisker-htpy-hom-system' {g = g} refl refl refl refl refl H) X = ap (section-system.type g) (section-system.type H X) section-system.element ( left-whisker-htpy-hom-system' {A = A} {B = B} {g = g} refl refl refl refl refl {f} {f'} H) {X} x = ( tr-ap ( section-system.type g) ( λ X' → section-system.element g {X'}) ( section-system.type H X) ( section-system.element f x)) ∙ ( ap (section-system.element g) (section-system.element H x)) section-system.slice ( left-whisker-htpy-hom-system' {A = A} {B = B} {C = C} {g = g} refl refl refl refl refl H) X = left-whisker-htpy-hom-system' ( ap (system.slice B) (section-system.type H X)) ( inv ( ap-comp ( constant-fibered-system (system.slice A X)) ( system.slice B) ( section-system.type H X))) ( ap (system.slice C ∘ section-system.type g) (section-system.type H X)) ( ( ap ( ap (constant-fibered-system (system.slice A X))) ( ap-comp ( system.slice C) ( section-system.type g) ( section-system.type H X))) ∙ ( inv ( ap-comp ( constant-fibered-system (system.slice A X)) ( system.slice C) ( ap (section-system.type g) (section-system.type H X))))) ( γ (section-system.type H X)) ( section-system.slice H X) where γ : {Y Y' : system.type B} (p : Id Y Y') → Id ( tr ( λ t → t) ( ap-binary hom-system ( ap (system.slice B) p) ( ap (system.slice C ∘ section-system.type g) p)) ( section-system.slice g Y)) ( section-system.slice g Y') γ refl = refl left-whisker-htpy-hom-system : {l1 l2 l3 l4 l5 l6 : Level} {A : system l1 l2} {B : system l3 l4} {C : system l5 l6} (g : hom-system B C) {f f' : hom-system A B} → htpy-hom-system f f' → htpy-hom-system (comp-hom-system g f) (comp-hom-system g f') left-whisker-htpy-hom-system g H = left-whisker-htpy-hom-system' refl refl refl refl refl H right-whisker-htpy-hom-system' : {l1 l2 l3 l4 l5 l6 : Level} {A : system l1 l2} {B : system l3 l4} {C C' : system l5 l6} (p : Id C C') {g : hom-system B C} {g' : hom-system B C'} {p' : Id (constant-fibered-system B C) (constant-fibered-system B C')} (α : Id (ap (constant-fibered-system B) p) p') {q' : Id (constant-fibered-system A C) (constant-fibered-system A C')} (β : Id (ap (constant-fibered-system A) p) q') (H : htpy-section-system' p' g g') → (f : hom-system A B) → htpy-section-system' q' (comp-hom-system g f) (comp-hom-system g' f) section-system.type (right-whisker-htpy-hom-system' refl refl refl H f) X = section-system.type H (section-system.type f X) section-system.element ( right-whisker-htpy-hom-system' refl refl refl H f) x = section-system.element H (section-system.element f x) section-system.slice ( right-whisker-htpy-hom-system' {A = A} {B = B} {C = C} refl refl refl H f) X = right-whisker-htpy-hom-system' ( ap (system.slice C) (section-system.type H (section-system.type f X))) ( inv ( ap-comp ( constant-fibered-system (system.slice B (section-system.type f X))) ( system.slice C) ( section-system.type H (section-system.type f X)))) ( inv ( ap-comp ( constant-fibered-system (system.slice A X)) ( system.slice C) ( section-system.type H (section-system.type f X)))) ( section-system.slice H (section-system.type f X)) ( section-system.slice f X) right-whisker-htpy-hom-system : {l1 l2 l3 l4 l5 l6 : Level} {A : system l1 l2} {B : system l3 l4} {C : system l5 l6} {g g' : hom-system B C} (H : htpy-section-system g g') → (f : hom-system A B) → htpy-section-system (comp-hom-system g f) (comp-hom-system g' f) right-whisker-htpy-hom-system H f = right-whisker-htpy-hom-system' refl refl refl H f
Structures on dependent type theories
Dependent type theories are systems equipped with weakening and substitution structure, and with the structure of generic elements (the variable rule).
Weakening structure on systems
record weakening {l1 l2 : Level} (A : system l1 l2) : UU (lsuc l1 ⊔ lsuc l2) where coinductive field type : (X : system.type A) → hom-system A (system.slice A X) slice : (X : system.type A) → weakening (system.slice A X)
Morphisms preserving weakening structure
We state what it means for a morphism to preserve weakening structure.
record preserves-weakening {l1 l2 l3 l4 : Level} {A : system l1 l2} {B : system l3 l4} (WA : weakening A) (WB : weakening B) (h : hom-system A B) : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) where coinductive field type : (X : system.type A) → htpy-hom-system ( comp-hom-system ( section-system.slice h X) ( weakening.type WA X)) ( comp-hom-system ( weakening.type WB (section-system.type h X)) ( h)) slice : (X : system.type A) → preserves-weakening ( weakening.slice WA X) ( weakening.slice WB (section-system.type h X)) ( section-system.slice h X)
Substitution structure on systems
We introduce substitution structure on a system.
record substitution {l1 l2 : Level} (A : system l1 l2) : UU (lsuc l1 ⊔ lsuc l2) where coinductive field type : {X : system.type A} (x : system.element A X) → hom-system (system.slice A X) A slice : (X : system.type A) → substitution (system.slice A X)
Morphisms preserving substitution structure
We state what it means for a morphism to preserve substitution structure.
record preserves-substitution {l1 l2 l3 l4 : Level} {A : system l1 l2} {B : system l3 l4} (SA : substitution A) (SB : substitution B) (h : hom-system A B) : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) where coinductive field type : {X : system.type A} (x : system.element A X) → htpy-hom-system ( comp-hom-system ( h) ( substitution.type SA x)) ( comp-hom-system ( substitution.type SB ( section-system.element h x)) ( section-system.slice h X)) slice : (X : system.type A) → preserves-substitution ( substitution.slice SA X) ( substitution.slice SB (section-system.type h X)) ( section-system.slice h X)
The structure of a generic element on a system equipped with weakening structure
We introduce the structure of a generic element on a system equipped with weakening structure.
record generic-element {l1 l2 : Level} {A : system l1 l2} (W : weakening A) : UU (l1 ⊔ l2) where coinductive field type : (X : system.type A) → system.element ( system.slice A X) ( section-system.type (weakening.type W X) X) slice : (X : system.type A) → generic-element (weakening.slice W X) record preserves-generic-element {l1 l2 l3 l4 : Level} {A : system l1 l2} {B : system l3 l4} {WA : weakening A} (δA : generic-element WA) {WB : weakening B} (δB : generic-element WB) {h : hom-system A B} (Wh : preserves-weakening WA WB h) : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) where coinductive field type : (X : system.type A) → Id ( tr ( system.element (system.slice B (section-system.type h X))) ( section-system.type ( preserves-weakening.type Wh X) ( X)) ( section-system.element ( section-system.slice h X) ( generic-element.type δA X))) ( generic-element.type δB (section-system.type h X)) slice : (X : system.type A) → preserves-generic-element ( generic-element.slice δA X) ( generic-element.slice δB (section-system.type h X)) ( preserves-weakening.slice Wh X)
Weakening and substitution morphisms preserve weakening, substitution, and generic elements
In a dependent type theory, every weakening morphism and every substitution morphism preserve both the weakening and substitution structure, and they also preserve generic elements.
For example, the rule that states that weakening preserves weakening (on types) can be displayed as follows:
Γ ⊢ A type Γ,Δ ⊢ B type Γ,Δ,Ε ⊢ C type
------------------------------------------------------------------------
Γ,A,W(A,Δ),W(A,B),W(W(A,B),W(A,E)) ⊢ W(W(A,B),W(A,C))=W(A,W(B,C)) type
Furthermore, there are laws that state that substitution by a : A cancels
weakening by A, that substituting a:A in the generic element of A gives us
the element a back, and that substituting by the generic element of A cancels
weakening by A.
We will now state these laws.
record weakening-preserves-weakening {l1 l2 : Level} {A : system l1 l2} (W : weakening A) : UU (l1 ⊔ l2) where coinductive field type : (X : system.type A) → preserves-weakening W (weakening.slice W X) (weakening.type W X) slice : (X : system.type A) → weakening-preserves-weakening (weakening.slice W X) record substitution-preserves-substitution {l1 l2 : Level} {A : system l1 l2} (S : substitution A) : UU (l1 ⊔ l2) where coinductive field type : {X : system.type A} (x : system.element A X) → preserves-substitution ( substitution.slice S X) ( S) ( substitution.type S x) slice : (X : system.type A) → substitution-preserves-substitution (substitution.slice S X) record weakening-preserves-substitution {l1 l2 : Level} {A : system l1 l2} (S : substitution A) (W : weakening A) : UU (l1 ⊔ l2) where coinductive field type : (X : system.type A) → preserves-substitution ( S) ( substitution.slice S X) ( weakening.type W X) slice : (X : system.type A) → weakening-preserves-substitution ( substitution.slice S X) ( weakening.slice W X) record substitution-preserves-weakening {l1 l2 : Level} {A : system l1 l2} (W : weakening A) (S : substitution A) : UU (l1 ⊔ l2) where coinductive field type : {X : system.type A} (x : system.element A X) → preserves-weakening ( weakening.slice W X) ( W) ( substitution.type S x) slice : (X : system.type A) → substitution-preserves-weakening ( weakening.slice W X) ( substitution.slice S X) record weakening-preserves-generic-element {l1 l2 : Level} {A : system l1 l2} (W : weakening A) (WW : weakening-preserves-weakening W) (δ : generic-element W) : UU (l1 ⊔ l2) where coinductive field type : (X : system.type A) → preserves-generic-element ( δ) ( generic-element.slice δ X) ( weakening-preserves-weakening.type WW X) slice : (X : system.type A) → weakening-preserves-generic-element ( weakening.slice W X) ( weakening-preserves-weakening.slice WW X) ( generic-element.slice δ X) record substitution-preserves-generic-element {l1 l2 : Level} {A : system l1 l2} (W : weakening A) (δ : generic-element W) (S : substitution A) (SW : substitution-preserves-weakening W S) : UU (l1 ⊔ l2) where coinductive field type : {X : system.type A} (x : system.element A X) → preserves-generic-element ( generic-element.slice δ X) ( δ) ( substitution-preserves-weakening.type SW x) slice : (X : system.type A) → substitution-preserves-generic-element ( weakening.slice W X) ( generic-element.slice δ X) ( substitution.slice S X) ( substitution-preserves-weakening.slice SW X) record substitution-cancels-weakening {l1 l2 : Level} {A : system l1 l2} (W : weakening A) (S : substitution A) : UU (l1 ⊔ l2) where coinductive field type : {X : system.type A} (x : system.element A X) → htpy-hom-system ( comp-hom-system ( substitution.type S x) ( weakening.type W X)) ( id-hom-system A) slice : (X : system.type A) → substitution-cancels-weakening ( weakening.slice W X) ( substitution.slice S X) record generic-element-is-identity {l1 l2 : Level} {A : system l1 l2} (W : weakening A) (S : substitution A) (δ : generic-element W) (S!W : substitution-cancels-weakening W S) : UU (l1 ⊔ l2) where coinductive field type : {X : system.type A} (x : system.element A X) → Id ( tr ( system.element A) ( section-system.type ( substitution-cancels-weakening.type S!W x) X) ( section-system.element ( substitution.type S x) ( generic-element.type δ X))) ( x) slice : (X : system.type A) → generic-element-is-identity ( weakening.slice W X) ( substitution.slice S X) ( generic-element.slice δ X) ( substitution-cancels-weakening.slice S!W X) record substitution-by-generic-element {l1 l2 : Level} {A : system l1 l2} (W : weakening A) (S : substitution A) (δ : generic-element W) : UU (l1 ⊔ l2) where coinductive field type : (X : system.type A) → htpy-hom-system ( comp-hom-system ( substitution.type ( substitution.slice S X) ( generic-element.type δ X)) ( weakening.type ( weakening.slice W X) ( section-system.type (weakening.type W X) X))) ( id-hom-system (system.slice A X)) slice : (X : system.type A) → substitution-by-generic-element ( weakening.slice W X) ( substitution.slice S X) ( generic-element.slice δ X)
Complete definition of a dependent type theory
We complete the definition of a dependent type theory.
record type-theory (l1 l2 : Level) : UU (lsuc l1 ⊔ lsuc l2) where field sys : system l1 l2 W : weakening sys S : substitution sys δ : generic-element W WW : weakening-preserves-weakening W SS : substitution-preserves-substitution S WS : weakening-preserves-substitution S W SW : substitution-preserves-weakening W S Wδ : weakening-preserves-generic-element W WW δ Sδ : substitution-preserves-generic-element W δ S SW S!W : substitution-cancels-weakening W S δid : generic-element-is-identity W S δ S!W Sδ! : substitution-by-generic-element W S δ closed-type-dtt : {l1 l2 : Level} (A : type-theory l1 l2) → UU l1 closed-type-dtt A = system.type (type-theory.sys A) global-element-dtt : {l1 l2 : Level} (A : type-theory l1 l2) → closed-type-dtt A → UU l2 global-element-dtt A = system.element (type-theory.sys A) weakening-dtt : {l1 l2 : Level} (A : type-theory l1 l2) (X : closed-type-dtt A) → hom-system ( type-theory.sys A) ( system.slice (type-theory.sys A) X) weakening-dtt A = weakening.type (type-theory.W A)
The slice of a dependent type theory
We introduce the slice of a dependent type theory.
slice-dtt : {l1 l2 : Level} (A : type-theory l1 l2) (X : system.type (type-theory.sys A)) → type-theory l1 l2 type-theory.sys (slice-dtt A X) = system.slice (type-theory.sys A) X type-theory.W (slice-dtt A X) = weakening.slice (type-theory.W A) X type-theory.S (slice-dtt A X) = substitution.slice (type-theory.S A) X type-theory.δ (slice-dtt A X) = generic-element.slice (type-theory.δ A) X type-theory.WW (slice-dtt A X) = weakening-preserves-weakening.slice (type-theory.WW A) X type-theory.SS (slice-dtt A X) = substitution-preserves-substitution.slice (type-theory.SS A) X type-theory.WS (slice-dtt A X) = weakening-preserves-substitution.slice (type-theory.WS A) X type-theory.SW (slice-dtt A X) = substitution-preserves-weakening.slice (type-theory.SW A) X type-theory.Wδ (slice-dtt A X) = weakening-preserves-generic-element.slice (type-theory.Wδ A) X type-theory.Sδ (slice-dtt A X) = substitution-preserves-generic-element.slice (type-theory.Sδ A) X type-theory.S!W (slice-dtt A X) = substitution-cancels-weakening.slice (type-theory.S!W A) X type-theory.δid (slice-dtt A X) = generic-element-is-identity.slice (type-theory.δid A) X type-theory.Sδ! (slice-dtt A X) = substitution-by-generic-element.slice (type-theory.Sδ! A) X
Morphisms of dependent type theories
record hom-dtt {l1 l2 l3 l4 : Level} (A : type-theory l1 l2) (B : type-theory l3 l4) : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) where field sys : hom-system ( type-theory.sys A) ( type-theory.sys B) W : preserves-weakening ( type-theory.W A) ( type-theory.W B) ( sys) S : preserves-substitution ( type-theory.S A) ( type-theory.S B) ( sys) δ : preserves-generic-element ( type-theory.δ A) ( type-theory.δ B) ( W) hom-slice-dtt : {l1 l2 l3 l4 : Level} {A : type-theory l1 l2} {B : type-theory l3 l4} (f : hom-dtt A B) (X : system.type (type-theory.sys A)) → hom-dtt ( slice-dtt A X) ( slice-dtt B (section-system.type (hom-dtt.sys f) X)) hom-dtt.sys (hom-slice-dtt f X) = section-system.slice (hom-dtt.sys f) X hom-dtt.W (hom-slice-dtt f X) = preserves-weakening.slice (hom-dtt.W f) X hom-dtt.S (hom-slice-dtt f X) = preserves-substitution.slice (hom-dtt.S f) X hom-dtt.δ (hom-slice-dtt f X) = preserves-generic-element.slice (hom-dtt.δ f) X
The identity morphism of a dependent type theory
preserves-weakening-id-hom-system : {l1 l2 : Level} {A : system l1 l2} (W : weakening A) → preserves-weakening W W (id-hom-system A) preserves-weakening.type (preserves-weakening-id-hom-system W) X = concat-htpy-hom-system ( left-unit-law-comp-hom-system (weakening.type W X)) ( inv-htpy-hom-system ( right-unit-law-comp-hom-system (weakening.type W X))) preserves-weakening.slice (preserves-weakening-id-hom-system W) X = preserves-weakening-id-hom-system (weakening.slice W X) preserves-substitution-id-hom-system : {l1 l2 : Level} {A : system l1 l2} (S : substitution A) → preserves-substitution S S (id-hom-system A) preserves-substitution.type (preserves-substitution-id-hom-system S) x = concat-htpy-hom-system ( left-unit-law-comp-hom-system (substitution.type S x)) ( inv-htpy-hom-system ( right-unit-law-comp-hom-system (substitution.type S x))) preserves-substitution.slice (preserves-substitution-id-hom-system S) X = preserves-substitution-id-hom-system (substitution.slice S X) preserves-generic-element-id-hom-system : {l1 l2 : Level} {A : system l1 l2} {W : weakening A} (δ : generic-element W) → preserves-generic-element δ δ ( preserves-weakening-id-hom-system W) preserves-generic-element.type ( preserves-generic-element-id-hom-system δ) X = refl preserves-generic-element.slice ( preserves-generic-element-id-hom-system δ) X = preserves-generic-element-id-hom-system (generic-element.slice δ X) id-hom-dtt : {l1 l2 : Level} (A : type-theory l1 l2) → hom-dtt A A hom-dtt.sys (id-hom-dtt A) = id-hom-system (type-theory.sys A) hom-dtt.W (id-hom-dtt A) = preserves-weakening-id-hom-system (type-theory.W A) hom-dtt.S (id-hom-dtt A) = preserves-substitution-id-hom-system (type-theory.S A) hom-dtt.δ (id-hom-dtt A) = preserves-generic-element-id-hom-system (type-theory.δ A)
The composition of morphisms of type theories
preserves-weakening-comp-hom-system : {l1 l2 l3 l4 l5 l6 : Level} {A : system l1 l2} {B : system l3 l4} {C : system l5 l6} {g : hom-system B C} {f : hom-system A B} {WA : weakening A} {WB : weakening B} {WC : weakening C} → preserves-weakening WB WC g → preserves-weakening WA WB f → preserves-weakening WA WC (comp-hom-system g f) preserves-weakening.type ( preserves-weakening-comp-hom-system {g = g} {f} {WA} {WB} {WC} Wg Wf) ( X) = concat-htpy-hom-system ( associative-comp-hom-system ( section-system.slice g (section-system.type f X)) ( section-system.slice f X) ( weakening.type WA X)) ( concat-htpy-hom-system ( left-whisker-htpy-hom-system ( section-system.slice g (section-system.type f X)) ( preserves-weakening.type Wf X)) ( concat-htpy-hom-system ( inv-htpy-hom-system ( associative-comp-hom-system ( section-system.slice g (section-system.type f X)) ( weakening.type WB (section-system.type f X)) ( f))) ( concat-htpy-hom-system ( right-whisker-htpy-hom-system ( preserves-weakening.type Wg (section-system.type f X)) ( f)) ( associative-comp-hom-system ( weakening.type WC ( section-system.type g (section-system.type f X))) ( g) ( f))))) preserves-weakening.slice ( preserves-weakening-comp-hom-system {f = f} Wg Wf) X = preserves-weakening-comp-hom-system ( preserves-weakening.slice Wg (section-system.type f X)) ( preserves-weakening.slice Wf X) preserves-substitution-comp-hom-system : {l1 l2 l3 l4 l5 l6 : Level} {A : system l1 l2} {B : system l3 l4} {C : system l5 l6} {g : hom-system B C} {f : hom-system A B} {SA : substitution A} {SB : substitution B} {SC : substitution C} → preserves-substitution SB SC g → preserves-substitution SA SB f → preserves-substitution SA SC (comp-hom-system g f) preserves-substitution.type ( preserves-substitution-comp-hom-system {g = g} {f} {SA} {SB} {SC} Sg Sf) {X} x = concat-htpy-hom-system ( associative-comp-hom-system g f (substitution.type SA x)) ( concat-htpy-hom-system ( left-whisker-htpy-hom-system g ( preserves-substitution.type Sf x)) ( concat-htpy-hom-system ( inv-htpy-hom-system ( associative-comp-hom-system g ( substitution.type SB ( section-system.element f x)) ( section-system.slice f X))) ( concat-htpy-hom-system ( right-whisker-htpy-hom-system ( preserves-substitution.type Sg ( section-system.element f x)) ( section-system.slice f X)) ( associative-comp-hom-system ( substitution.type SC ( section-system.element g (section-system.element f x))) ( section-system.slice g (section-system.type f X)) ( section-system.slice f X))))) preserves-substitution.slice ( preserves-substitution-comp-hom-system {f = f} Sg Sf) X = preserves-substitution-comp-hom-system ( preserves-substitution.slice Sg (section-system.type f X)) ( preserves-substitution.slice Sf X) preserves-generic-element-comp-hom-system : {l1 l2 l3 l4 l5 l6 : Level} {A : system l1 l2} {B : system l3 l4} {C : system l5 l6} {g : hom-system B C} {f : hom-system A B} {WA : weakening A} {WB : weakening B} {WC : weakening C} → {δA : generic-element WA} {δB : generic-element WB} {δC : generic-element WC} → {Wg : preserves-weakening WB WC g} {Wf : preserves-weakening WA WB f} → (δg : preserves-generic-element δB δC Wg) (δf : preserves-generic-element δA δB Wf) → preserves-generic-element δA δC (preserves-weakening-comp-hom-system Wg Wf) preserves-generic-element.type ( preserves-generic-element-comp-hom-system {A = A} {B} {C} {g} {f} {WA} {WB} {WC} {δA} {δB} {δC} {Wg} {Wf} δg δf) X = ( ap ( λ t → tr ( system.element ( system.slice C (section-system.type (comp-hom-system g f) X))) ( t) ( section-system.element ( section-system.slice (comp-hom-system g f) X) ( generic-element.type δA X))) ( ap (α ∙_) (right-unit))) ∙ ( ( tr-concat { B = system.element ( system.slice C (section-system.type (comp-hom-system g f) X))} ( α) ( β) ( section-system.element ( section-system.slice (comp-hom-system g f) X) ( generic-element.type δA X))) ∙ ( ( ap ( tr ( system.element ( system.slice C ( section-system.type (comp-hom-system g f) X))) ( β)) ( ( γ ( section-system.type (preserves-weakening.type Wf X) X) ( section-system.element ( section-system.slice f X) ( generic-element.type δA X))) ∙ ( ap ( section-system.element ( section-system.slice g (section-system.type f X))) ( preserves-generic-element.type δf X)))) ∙ ( preserves-generic-element.type δg (section-system.type f X)))) where α = ap ( section-system.type ( section-system.slice g (section-system.type f X))) ( section-system.type (preserves-weakening.type Wf X) X) β = section-system.type ( preserves-weakening.type Wg (section-system.type f X)) ( section-system.type f X) γ : { Y : system.type (system.slice B (section-system.type f X))} ( p : Id ( Y) ( section-system.type ( comp-hom-system ( weakening.type WB (section-system.type f X)) ( f)) ( X))) ( u : system.element (system.slice B (section-system.type f X)) Y) → Id ( tr ( system.element ( system.slice ( C) ( section-system.type (comp-hom-system g f) X))) ( ap ( section-system.type ( section-system.slice g (section-system.type f X))) ( p)) ( section-system.element ( section-system.slice g (section-system.type f X)) ( u))) ( section-system.element ( section-system.slice g (section-system.type f X)) ( tr ( system.element (system.slice B (section-system.type f X))) ( p) ( u))) γ refl u = refl preserves-generic-element.slice ( preserves-generic-element-comp-hom-system {f = f} δg δf) X = preserves-generic-element-comp-hom-system ( preserves-generic-element.slice δg (section-system.type f X)) ( preserves-generic-element.slice δf X) comp-hom-dtt : {l1 l2 l3 l4 l5 l6 : Level} {A : type-theory l1 l2} {B : type-theory l3 l4} {C : type-theory l5 l6} → hom-dtt B C → hom-dtt A B → hom-dtt A C hom-dtt.sys (comp-hom-dtt g f) = comp-hom-system (hom-dtt.sys g) (hom-dtt.sys f) hom-dtt.W (comp-hom-dtt g f) = preserves-weakening-comp-hom-system (hom-dtt.W g) (hom-dtt.W f) hom-dtt.S (comp-hom-dtt g f) = preserves-substitution-comp-hom-system (hom-dtt.S g) (hom-dtt.S f) hom-dtt.δ (comp-hom-dtt g f) = preserves-generic-element-comp-hom-system (hom-dtt.δ g) (hom-dtt.δ f)
Homotopies of morphisms of dependent type theories
htpy-hom-dtt : {l1 l2 l3 l4 : Level} {A : type-theory l1 l2} {B : type-theory l3 l4} (f g : hom-dtt A B) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) htpy-hom-dtt f g = htpy-hom-system (hom-dtt.sys f) (hom-dtt.sys g) left-unit-law-comp-hom-dtt : {l1 l2 l3 l4 : Level} {A : type-theory l1 l2} {B : type-theory l3 l4} (f : hom-dtt A B) → htpy-hom-dtt (comp-hom-dtt (id-hom-dtt B) f) f left-unit-law-comp-hom-dtt f = left-unit-law-comp-hom-system (hom-dtt.sys f) right-unit-law-comp-hom-dtt : {l1 l2 l3 l4 : Level} {A : type-theory l1 l2} {B : type-theory l3 l4} (f : hom-dtt A B) → htpy-hom-dtt (comp-hom-dtt f (id-hom-dtt A)) f right-unit-law-comp-hom-dtt f = right-unit-law-comp-hom-system (hom-dtt.sys f) associative-comp-hom-dtt : {l1 l2 l3 l4 l5 l6 l7 l8 : Level} {A : type-theory l1 l2} {B : type-theory l3 l4} {C : type-theory l5 l6} {D : type-theory l7 l8} (h : hom-dtt C D) (g : hom-dtt B C) (f : hom-dtt A B) → htpy-hom-dtt ( comp-hom-dtt (comp-hom-dtt h g) f) ( comp-hom-dtt h (comp-hom-dtt g f)) associative-comp-hom-dtt h g f = associative-comp-hom-system (hom-dtt.sys h) (hom-dtt.sys g) (hom-dtt.sys f)
Simple type theories
record is-simple-type-theory {l1 l2 : Level} (A : type-theory l1 l2) : UU l1 where coinductive field type : (X : system.type (type-theory.sys A)) → is-equiv ( section-system.type ( weakening.type (type-theory.W A) X)) slice : (X : system.type (type-theory.sys A)) → is-simple-type-theory (slice-dtt A X) record simple-type-theory (l1 l2 : Level) : UU (lsuc l1 ⊔ lsuc l2) where field dtt : type-theory l1 l2 is-simple : is-simple-type-theory dtt
The condition that the action on elements of a morphism of dependent type theories is an equivalence
We introduce the condition that the action on elements of a morphism of dependent type theories is an equivalence.
record is-equiv-on-elements-hom-system {l1 l2 l3 l4 : Level} (A : system l1 l2) (B : system l3 l4) (h : hom-system A B) : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) where coinductive field type : (X : system.type A) → is-equiv (section-system.element h {X}) slice : (X : system.type A) → is-equiv-on-elements-hom-system ( system.slice A X) ( system.slice B (section-system.type h X)) ( section-system.slice h X)
Unary type theories
record unary-type-theory {l1 l2 : Level} (A : type-theory l1 l2) : UU (lsuc l1 ⊔ lsuc l2) where field dtt : type-theory l1 l2 is-simple : is-simple-type-theory A is-unary : (X Y : system.type (type-theory.sys A)) → is-equiv-on-elements-hom-system ( system.slice (type-theory.sys A) Y) ( system.slice ( system.slice (type-theory.sys A) X) ( section-system.type ( weakening.type (type-theory.W A) X) Y)) ( section-system.slice ( weakening.type (type-theory.W A) X) ( Y))
Proof irrelevant type theories
record is-proof-irrelevant-type-theory {l1 l2 : Level} (A : type-theory l1 l2) : UU (l1 ⊔ l2) where coinductive field type : (X : system.type (type-theory.sys A)) → is-prop (system.element (type-theory.sys A) X) slice : (X : system.type (type-theory.sys A)) → is-proof-irrelevant-type-theory (slice-dtt A X)
system-Slice : {l : Level} (X : UU l) → system (lsuc l) l system.type (system-Slice {l} X) = X → UU l system.element (system-Slice X) Y = (x : X) → Y x system.slice (system-Slice X) Y = system-Slice (Σ X Y) {- hom-system-weakening-system-Slice : {l : Level} (X : UU l) (Y : X → UU l) → hom-system (system-Slice X) (system-Slice (Σ X Y)) section-system.type (hom-system-weakening-system-Slice X Y) Z (pair x y) = Z x section-system.element (hom-system-weakening-system-Slice X Y) Z g (pair x y) = g x section-system.type (section-system.slice (hom-system-weakening-system-Slice X Y) Z) W (pair (pair x y) z) = W (pair x z) section-system.element (section-system.slice (hom-system-weakening-system-Slice X Y) Z) W h (pair (pair x y) z) = h (pair x z) section-system.slice (section-system.slice (hom-system-weakening-system-Slice X Y) Z) W = {!section-system.slice (hom-system-weakening-system-Slice X Y) ?!} weakening-system-Slice : {l : Level} (X : UU l) → weakening (system-Slice X) weakening.type (weakening-system-Slice X) Y = hom-system-weakening-system-Slice X Y weakening.slice (weakening-system-Slice X) = {!!} system-UU : (l : Level) → system (lsuc l) l system.type (system-UU l) = UU l system.element (system-UU l) X = X system.slice (system-UU l) X = system-Slice X weakening-type-UU : {l : Level} (X : UU l) → hom-system (system-UU l) (system.slice (system-UU l) X) section-system.type (weakening-type-UU X) Y x = Y section-system.element (weakening-type-UU X) Y y x = y section-system.slice (weakening-type-UU X) Y = {!!} weakening-UU : (l : Level) → weakening (system-UU l) section-system.type (weakening.type (weakening-UU l) X) Y x = Y section-system.element (weakening.type (weakening-UU l) X) Y y x = y section-system.type (section-system.slice (weakening.type (weakening-UU l) X) Y) Z t = Z (pr2 t) section-system.element ( section-system.slice (weakening.type (weakening-UU l) X) Y) Z f t = f (pr2 t) section-system.slice (section-system.slice (weakening.type (weakening-UU l) X) Y) Z = {!!} section-system.type ( weakening.type (weakening.slice (weakening-UU l) X) Y) Z (pair x y) = Z x section-system.element ( weakening.type (weakening.slice (weakening-UU l) X) Y) Z f (pair x y) = f x section-system.slice (weakening.type (weakening.slice (weakening-UU l) X) Y) Z = {!!} weakening.slice (weakening.slice (weakening-UU l) X) Y = weakening.slice (weakening-UU l) (Σ X Y) -}
Dependent type theories with Π-types
We define what it means for a dependent type theory to have Π-types.
record function-types {l1 l2 : Level} (A : type-theory l1 l2) : UU (l1 ⊔ l2) where coinductive field sys : (X : system.type (type-theory.sys A)) → hom-dtt (slice-dtt A X) A app : (X : system.type (type-theory.sys A)) → is-equiv-on-elements-hom-system ( type-theory.sys (slice-dtt A X)) ( type-theory.sys A) ( hom-dtt.sys (sys X)) slice : (X : system.type (type-theory.sys A)) → function-types (slice-dtt A X) {- record preserves-function-types {l1 l2 l3 l4 : Level} {A : type-theory l1 l2} {B : type-theory l3 l4} (ΠA : function-types A) (ΠB : function-types B) (h : hom-dtt A B) : UU {!!} where coinductive field sys : {!!} slice : {!!} -}
record natural-numbers {l1 l2 : Level} (A : type-theory l1 l2) (Π : function-types A) : UU (l1 ⊔ l2) where field N : closed-type-dtt A zero : global-element-dtt A N succ : global-element-dtt A ( section-system.type ( hom-dtt.sys (function-types.sys Π N)) ( section-system.type ( weakening.type (type-theory.W A) N) ( N))) {- natural-numbers-slice : {l1 l2 : Level} (A : type-theory l1 l2) (Π : function-types A) (N : natural-numbers A Π) (X : closed-type-dtt A) → natural-numbers (slice-dtt A X) (function-types.slice Π X) natural-numbers.N (natural-numbers-slice A Π N X) = section-system.type ( weakening.type (type-theory.W A) X) ( natural-numbers.N N) natural-numbers.zero (natural-numbers-slice A Π N X) = section-system.element ( weakening.type (type-theory.W A) X) ( natural-numbers.N N) ( natural-numbers.zero N) natural-numbers.succ (natural-numbers-slice A Π N X) = tr ( system.element (type-theory.sys (slice-dtt A X))) {! (section-system.type (preserves-weakening.type (hom-dtt.W (function-types.sys Π (natural-numbers.N N))) ?) ?)!} {- Id ( section-system.type ( weakening.type (type-theory.W A) X) ( section-system.type ( hom-dtt.sys (function-types.sys Π (natural-numbers.N N))) ( section-system.type ( weakening.type (type-theory.W A) (natural-numbers.N N)) (natural-numbers.N N)))) ( section-system.type ( hom-dtt.sys ( function-types.sys (function-types.slice Π X) ( natural-numbers.N (natural-numbers-slice A Π N X)))) ( section-system.type ( weakening.type ( type-theory.W (slice-dtt A X)) ( natural-numbers.N (natural-numbers-slice A Π N X))) ( natural-numbers.N (natural-numbers-slice A Π N X)))) -} ( section-system.element ( weakening.type (type-theory.W A) X) ( section-system.type ( hom-dtt.sys (function-types.sys Π (natural-numbers.N N))) ( section-system.type ( weakening.type (type-theory.W A) (natural-numbers.N N)) ( natural-numbers.N N))) ( natural-numbers.succ N)) -}
{- concat-htpy-hom-system' : {l1 l2 l3 l4 : Level} {A : system l1 l2} {B B' B'' : system l3 l4} (p : Id B B') (q : Id B' B'') {f : hom-system A B} {g : hom-system A B'} {h : hom-system A B''} → htpy-hom-system' p f g → htpy-hom-system' q g h → htpy-hom-system' (p ∙ q) f h htpy-hom-system'.type (concat-htpy-hom-system' refl refl H K) = htpy-hom-system'.type H ∙h htpy-hom-system'.type K htpy-hom-system'.element ( concat-htpy-hom-system' {A = A} {B} {.B} refl refl {f} H K) X x = ( ( tr-concat ( section-system.type H X) ( section-system.type K X) ( section-system.element (tr (hom-system A) refl f) X x)) ∙ ( ap ( tr (system.element B) (section-system.type K X)) ( section-system.element H X x))) ∙ ( section-system.element K X x) htpy-hom-system'.slice (concat-htpy-hom-system' p q H K) = {!!} concat-htpy-hom-system : {l1 l2 l3 l4 : Level} {A : system l1 l2} {B : system l3 l4} {f g h : hom-system A B} (H : htpy-hom-system f g) (K : htpy-hom-system g h) → htpy-hom-system f h htpy-hom-system'.type (concat-htpy-hom-system H K) = section-system.type H ∙h section-system.type K htpy-hom-system'.element ( concat-htpy-hom-system {A = A} {B = B} {f} H K) X x = ( ( tr-concat ( section-system.type H X) ( section-system.type K X) ( section-system.element (tr (hom-system A) refl f) X x)) ∙ ( ap ( tr (system.element B) (section-system.type K X)) ( section-system.element H X x))) ∙ ( section-system.element K X x) htpy-hom-system'.slice (concat-htpy-hom-system H K) X = {!!} -}
Contexts in a dependent type theory
We interpret contexts in a dependent type theory.
module c-system where open dependent data context {l1 l2 : Level} (A : type-theory l1 l2) : UU l1 where empty-ctx : context A extension-ctx : (X : system.type (type-theory.sys A)) (Γ : context (slice-dtt A X)) → context A
The action on contexts of a morphism of dependent type theories
context-hom : {l1 l2 l3 l4 : Level} {A : type-theory l1 l2} {B : type-theory l3 l4} (f : hom-dtt A B) → context A → context B context-hom f empty-ctx = empty-ctx context-hom f (extension-ctx X Γ) = extension-ctx ( section-system.type (hom-dtt.sys f) X) ( context-hom (hom-slice-dtt f X) Γ)
Elements of contexts
{- data element-context {l1 l2 : Level} {A : type-theory l1 l2} : (Γ : context A) → UU {!substitution.type (type-theory.S A) !} where element-empty-context : element-context empty-ctx element-extension-ctx : {!(X : system.type (type-theory.sys A)) (Γ : context (slice-dtt A X)) (x : system.element (type-theory.sys A) X) (y : element-context (context-hom (substitution.type (type-theory.S A) x) Γ)) → element-context (extension-ctx X Γ)!} -}
Interpreting types in context in a dependent type theory
type : {l1 l2 : Level} (A : type-theory l1 l2) → context A → UU l1 type A empty-ctx = system.type (type-theory.sys A) type A (extension-ctx X Γ) = type (slice-dtt A X) Γ
Interpreting elements of types in context in a dependent type theory
element : {l1 l2 : Level} (A : type-theory l1 l2) (Γ : context A) (Y : type A Γ) → UU l2 element A empty-ctx = system.element (type-theory.sys A) element A (extension-ctx X Γ) = element (slice-dtt A X) Γ slice : {l1 l2 : Level} (A : type-theory l1 l2) (Γ : context A) → type-theory l1 l2 slice A empty-ctx = A slice A (extension-ctx X Γ) = slice (slice-dtt A X) Γ dependent-context : {l1 l2 : Level} (A : type-theory l1 l2) (Γ : context A) → UU l1 dependent-context A Γ = context (slice A Γ) {- weakening-by-type-context : {l1 l2 : Level} {A : type-theory l1 l2} (X : system.type (type-theory.sys A)) → context A → context (slice-dtt A X) weakening-by-type-context {A = A} X Δ = context-hom {!weakening.type (type-theory.W A) X!} Δ -} weakening-type-context : {l1 l2 : Level} (A : type-theory l1 l2) (Γ : context A) → system.type (type-theory.sys A) → system.type (type-theory.sys (slice A Γ)) weakening-type-context A empty-ctx Y = Y weakening-type-context A (extension-ctx X Γ) Y = weakening-type-context (slice-dtt A X) Γ ( section-system.type ( weakening.type (type-theory.W A) X) Y) {- weakening-context : {l1 l2 : Level} (A : type-theory l1 l2) (Γ : context A) → context A → context (slice A Γ) weakening-context A empty-ctx Δ = Δ weakening-context A (extension-ctx X Γ) empty-ctx = empty-ctx weakening-context A (extension-ctx X Γ) (extension-ctx Y Δ) = extension-ctx ( weakening-type-context A (extension-ctx X Γ) Y) ( weakening-context {!!} {!!} {!!}) -}