# Dependent type theories

Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.

Created on 2022-04-14.

{-# OPTIONS --guardedness #-}

module type-theories.dependent-type-theories where

Imports
open import foundation.action-on-identifications-binary-functions
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.propositions
open import foundation.transport-along-identifications
open import foundation.universe-levels
open import foundation.whiskering-identifications-concatenation


## Idea

We introduce the category 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.

    Ã₀       Ã₁       Ã₂
|        |        |
|        |        |
∨        ∨        ∨
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-comp-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-comp-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-comp-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-comp-hom-system'
{A = A} {B = B} {C = C} {g = g} refl refl refl refl refl H) X =
left-whisker-comp-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-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 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-comp-hom-system g H =
left-whisker-comp-hom-system' refl refl refl refl refl H

right-whisker-comp-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-comp-hom-system' refl refl refl H f) X =
section-system.type H (section-system.type f X)
section-system.element
( right-whisker-comp-hom-system' refl refl refl H f) x =
section-system.element H (section-system.element f x)
section-system.slice
( right-whisker-comp-hom-system'
{A = A} {B = B} {C = C} refl refl refl H f) X =
right-whisker-comp-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-comp-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-comp-hom-system H f =
right-whisker-comp-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-comp-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-comp-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-comp-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-comp-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)))
( left-whisker-concat α 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 {!!} {!!} {!!})
-}