# Simple type theories

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

Created on 2022-04-14.

{-# OPTIONS --guardedness --allow-unsolved-metas #-}

module type-theories.simple-type-theories where

Imports
open import foundation.action-on-identifications-functions
open import foundation.function-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.transport-along-identifications
open import foundation.universe-levels


## Idea

Simple type theories are type theories that have no type dependency. The category of simple type theories is equivalent to the category of multisorted algebraic theories.

## Definitions

module simple where

record system
{l1 : Level} (l2 : Level) (T : UU l1) : UU (l1 ⊔ lsuc l2)
where
coinductive
field
element : T → UU l2
slice : (X : T) → system l2 T

record fibered-system
{l1 l2 l3 : Level} (l4 : Level) {T : UU l1} (S : T → UU l2)
(A : system l3 T) : UU (l1 ⊔ l2 ⊔ l3 ⊔ lsuc l4)
where
coinductive
field
element : {X : T} → S X → system.element A X → UU l4
slice : {X : T} → S X → fibered-system l4 S (system.slice A X)

record section-system
{l1 l2 l3 l4 : Level} {T : UU l1} {S : T → UU l2} {A : system l3 T}
(B : fibered-system l4 S A) (f : (X : T) → S X) : UU (l1 ⊔ l3 ⊔ l4)
where
coinductive
field
element :
{X : T} (x : system.element A X) →
fibered-system.element B (f X) x
slice : (X : T) → section-system (fibered-system.slice B (f X)) f

------------------------------------------------------------------------------


We 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.

  Eq-fibered-system' :
{l1 l2 l3 l4 : Level} {T : UU l1} {A : system l2 T} {S : T → UU l3}
{B B' : fibered-system l4 S A} (α : Id B B') {f f' : (X : T) → S X}
(g : section-system B f) (g' : section-system B' f') →
fibered-system l4 (λ t → Id (f t) (f' t)) A
fibered-system.element (Eq-fibered-system' {B = B} refl {f} g g') {X} p x =
Id
( tr
( λ u → fibered-system.element B u x)
( p)
( section-system.element g x))
( section-system.element g' x)
fibered-system.slice (Eq-fibered-system' {B = B} refl g g') {X} p =
Eq-fibered-system'
( ap (fibered-system.slice B) p)
( section-system.slice g X)
( section-system.slice g' X)

htpy-section-system' :
{l1 l2 l3 l4 : Level} {T : UU l1} {A : system l2 T} {S : T → UU l3}
{B B' : fibered-system l4 S A} (α : Id B B') {f f' : (X : T) → S X}
(H : f ~ f') (g : section-system B f) (g' : section-system B' f') →
UU (l1 ⊔ l2 ⊔ l4)
htpy-section-system' α H g g' =
section-system (Eq-fibered-system' α g g') H

concat-htpy-section-system' :
{l1 l2 l3 l4 : Level}
{T : UU l1} {A : system l2 T} {S : T → UU l3}
{B B' B'' : fibered-system l4 S A} {α : Id B B'} {β : Id B' B''}
(γ : Id B B'') (δ : Id (α ∙ β) γ) {f f' f'' : (X : T) → S X}
{H : f ~ f'} {H' : f' ~ f''} {g : section-system B f}
{g' : section-system B' f'} {g'' : section-system B'' f''}
(K : htpy-section-system' α H g g')
(K' : htpy-section-system' β H' g' g'') →
htpy-section-system' γ (H ∙h H') g g''
section-system.element
( concat-htpy-section-system'
{B = B} {α = refl} {refl} .refl refl {H = H} {H'} {g} K K') {X} x =
( tr-concat
{ B = λ t → fibered-system.element B t x}
( H X)
( H' X)
( section-system.element g x)) ∙
( ( ap
( tr
( λ t → fibered-system.element B t x)
( H' X))
( section-system.element K x)) ∙
( section-system.element K' x))
section-system.slice
( concat-htpy-section-system'
{B = B} {α = refl} {refl} .refl refl {H = H} {H'} K K') X =
concat-htpy-section-system'
( ap (fibered-system.slice B) (H X ∙ H' X))
( inv (ap-concat (fibered-system.slice B) (H X) (H' X)))
( section-system.slice K X)
( section-system.slice K' X)

inv-htpy-section-system' :
{l1 l2 l3 l4 : Level}
{T : UU l1} {A : system l2 T} {S : T → UU l3}
{B B' : fibered-system l4 S A}
{α : Id B B'} (β : Id B' B) (γ : Id (inv α) β)
{f f' : (X : T) → S X} {g : section-system B f}
{g' : section-system B' f'} {H : f ~ f'} →
htpy-section-system' α H g g' → htpy-section-system' β (inv-htpy H) g' g
section-system.element
( inv-htpy-section-system' {α = refl} .refl refl {H = H} K) {X} x =
eq-transpose-tr
( H X)
( inv (section-system.element K x))
section-system.slice
( inv-htpy-section-system' {B = B} {α = refl} .refl refl {H = H} K) X =
inv-htpy-section-system'
( ap (fibered-system.slice B) (inv (H X)))
( inv (ap-inv (fibered-system.slice B) (H X)))
( section-system.slice K X)


### Nonhomogenous homotopies

We specialize the above definitions to nonhomogenous homotopies.

  htpy-section-system :
{l1 l2 l3 l4 : Level}
{T : UU l1} {A : system l2 T} {S : T → UU l3}
{B : fibered-system l4 S A} {f f' : (X : T) → S X} →
(f ~ f') → section-system B f → section-system B f' → UU (l1 ⊔ l2 ⊔ l4)
htpy-section-system H g g' = htpy-section-system' refl H g g'

refl-htpy-section-system :
{l1 l2 l3 l4 : Level}
{T : UU l1} {A : system l2 T} {S : T → UU l3}
{B : fibered-system l4 S A} {f : (X : T) → S X}
(g : section-system B f) → htpy-section-system refl-htpy g g
section-system.element (refl-htpy-section-system g) = refl-htpy
section-system.slice (refl-htpy-section-system g) X =
refl-htpy-section-system (section-system.slice g X)

concat-htpy-section-system :
{l1 l2 l3 l4 : Level}
{T : UU l1} {A : system l2 T} {S : T → UU l3}
{B : fibered-system l4 S A} {f f' f'' : (X : T) → S X}
{g : section-system B f} {g' : section-system B f'}
{g'' : section-system B f''} {H : f ~ f'} {H' : f' ~ f''} →
htpy-section-system H g g' → htpy-section-system H' g' g'' →
htpy-section-system (H ∙h H') g g''
concat-htpy-section-system K K' =
concat-htpy-section-system' refl refl K K'

inv-htpy-section-system :
{l1 l2 l3 l4 : Level}
{T : UU l1} {A : system l2 T} {S : T → UU l3}
{B : fibered-system l4 S A} {f f' : (X : T) → S X}
{g : section-system B f} {g' : section-system B f'} {H : f ~ f'} →
htpy-section-system H g g' → htpy-section-system (inv-htpy H) g' g
inv-htpy-section-system K =
inv-htpy-section-system' refl refl K


  constant-fibered-system :
{l1 l2 l3 l4 : Level} {T : UU l1} (A : system l2 T) {S : UU l3}
(B : system l4 S) → fibered-system l4 (λ X → S) A
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} {T : UU l1} {S : UU l2} (f : T → S)
(A : system l3 T) (B : system l4 S) → UU (l1 ⊔ l3 ⊔ l4)
hom-system f A B = section-system (constant-fibered-system A B) f

htpy-hom-system :
{l1 l2 l3 l4 : Level} {T : UU l1} {S : UU l2} {f : T → S}
{A : system l3 T} {B : system l4 S} (g h : hom-system f A B) →
UU (l1 ⊔ l3 ⊔ l4)
htpy-hom-system g h = htpy-section-system {!!} {!!} {!!}

id-hom-system :
{l1 l2 : Level} {T : UU l1} (A : system l2 T) → hom-system id A A
section-system.element (id-hom-system A) {X} = id
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} {T : UU l1} {S : UU l2} {R : UU l3} {g : S → R}
{f : T → S} {A : system l4 T} {B : system l5 S} {C : system l6 R}
(β : hom-system g B C) (α : hom-system f A B) → hom-system (g ∘ f) A C
section-system.element (comp-hom-system {f = f} β α) {X} =
section-system.element β {f X} ∘ section-system.element α {X}
section-system.slice (comp-hom-system {f = f} β α) X =
comp-hom-system (section-system.slice β (f X)) (section-system.slice α X)

record weakening
{l1 l2 : Level} {T : UU l1} (A : system l2 T) : UU (l1 ⊔ l2)
where
coinductive
field
element : (X : T) → hom-system id A (system.slice A X)
slice : (X : T) → weakening (system.slice A X)

record preserves-weakening
{l1 l2 l3 l4 : Level} {T : UU l1} {S : UU l2} {f : T → S}
{A : system l3 T} {B : system l4 S} (WA : weakening A) (WB : weakening B)
(h : hom-system f A B) : UU (l1 ⊔ l3 ⊔ l4)
where
coinductive
field
element :
(X : T) →
htpy-hom-system
( comp-hom-system
( section-system.slice h X)
( weakening.element WA X))
( comp-hom-system
( weakening.element WB (f X))
( h))
slice :
(X : T) →
preserves-weakening
( weakening.slice WA X)
( weakening.slice WB (f X))
( section-system.slice h X)

record substitution
{l1 l2 : Level} {T : UU l1} (A : system l2 T) : UU (l1 ⊔ l2)
where
coinductive
field
element :
{X : T} (x : system.element A X) →
hom-system id (system.slice A X) A
slice :
(X : T) → substitution (system.slice A X)

record preserves-substitution
{l1 l2 l3 l4 : Level}
{T : UU l1} {S : UU l2} {f : T → S} {A : system l3 T}
{B : system l4 S} (SA : substitution A) (SB : substitution B)
(h : hom-system f A B) : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
where
coinductive
field
element :
{X : T} (x : system.element A X) →
htpy-hom-system
( comp-hom-system
( h)
( substitution.element SA x))
( comp-hom-system
( substitution.element SB
( section-system.element h x))
( section-system.slice h X))
slice :
(X : T) →
preserves-substitution
( substitution.slice SA X)
( substitution.slice SB (f X))
( section-system.slice h X)

record generic-element
{l1 l2 : Level} {T : UU l1} (A : system l2 T) : UU (l1 ⊔ l2)
where
coinductive
field
element : (X : T) → system.element (system.slice A X) X
slice : (X : T) → generic-element (system.slice A X)

record preserves-generic-element
{l1 l2 l3 l4 : Level}
{T : UU l1} {S : UU l2} {f : T → S}
{A : system l3 T} {B : system l4 S}
(δA : generic-element A) (δB : generic-element B)
(h : hom-system f A B) : UU (l1 ⊔ l3 ⊔ l4)
where
coinductive
field
element :
(X : T) →
Id
( section-system.element
( section-system.slice h X)
( generic-element.element δA X))
( generic-element.element δB (f X))
slice :
(X : T) →
preserves-generic-element
( generic-element.slice δA X)
( generic-element.slice δB (f X))
( section-system.slice h X)

module _
{l1 l2 : Level} {T : UU l1}
where

record weakening-preserves-weakening
{A : system l2 T} (W : weakening A) : UU (l1 ⊔ l2)
where
coinductive
field
element :
(X : T) →
preserves-weakening
( W)
( weakening.slice W X)
( weakening.element W X)
slice :
(X : T) → weakening-preserves-weakening (weakening.slice W X)

record substitution-preserves-substitution
{A : system l2 T} (S : substitution A) : UU (l1 ⊔ l2)
where
coinductive
field
element :
{X : T} (x : system.element A X) →
preserves-substitution
( substitution.slice S X)
( S)
( substitution.element S x)
slice :
(X : T) →
substitution-preserves-substitution (substitution.slice S X)

record weakening-preserves-substitution
{A : system l2 T} (W : weakening A) (S : substitution A) : UU (l1 ⊔ l2)
where
coinductive
field
element :
(X : T) →
preserves-substitution
( S)
( substitution.slice S X)
( weakening.element W X)
slice :
(X : T) →
weakening-preserves-substitution
( weakening.slice W X)
( substitution.slice S X)

record substitution-preserves-weakening
{A : system l2 T} (W : weakening A) (S : substitution A) : UU (l1 ⊔ l2)
where
coinductive
field
element :
{X : T} (x : system.element A X) →
preserves-weakening
( weakening.slice W X)
( W)
( substitution.element S x)
slice :
(X : T) →
substitution-preserves-weakening
( weakening.slice W X)
( substitution.slice S X)

record weakening-preserves-generic-element
{A : system l2 T} (W : weakening A) (δ : generic-element A) :
UU (l1 ⊔ l2)
where
coinductive
field
element :
(X : T) →
preserves-generic-element
( δ)
( generic-element.slice δ X)
( weakening.element W X)
slice :
(X : T) →
weakening-preserves-generic-element
( weakening.slice W X)
( generic-element.slice δ X)

record substitution-preserves-generic-element
{A : system l2 T} (S : substitution A) (δ : generic-element A) :
UU (l1 ⊔ l2)
where
coinductive
field
element :
{X : T} (x : system.element A X) →
preserves-generic-element
( generic-element.slice δ X)
( δ)
( substitution.element S x)
slice :
(X : T) →
substitution-preserves-generic-element
( substitution.slice S X)
( generic-element.slice δ X)

record substitution-cancels-weakening
{A : system l2 T} (W : weakening A) (S : substitution A) : UU (l1 ⊔ l2)
where
coinductive
field
element :
{X : T} (x : system.element A X) →
htpy-hom-system
( comp-hom-system
( substitution.element S x)
( weakening.element W X))
( id-hom-system A)
slice :
(X : T) →
substitution-cancels-weakening
( weakening.slice W X)
( substitution.slice S X)

record generic-element-is-identity
{A : system l2 T} (S : substitution A) (δ : generic-element A) :
UU (l1 ⊔ l2)
where
coinductive
field
element :
{X : T} (x : system.element A X) →
Id ( section-system.element
( substitution.element S x)
( generic-element.element δ X))
( x)
slice :
(X : T) →
generic-element-is-identity
( substitution.slice S X)
( generic-element.slice δ X)

record substitution-by-generic-element
{A : system l2 T} (W : weakening A) (S : substitution A)
(δ : generic-element A) : UU (l1 ⊔ l2)
where
coinductive
field
element :
(X : T) →
htpy-hom-system
( comp-hom-system
( substitution.element
( substitution.slice S X)
( generic-element.element δ X))
( weakening.element (weakening.slice W X) X))
( id-hom-system (system.slice A X))
slice :
(X : T) →
substitution-by-generic-element
( weakening.slice W X)
( substitution.slice S X)
( generic-element.slice δ X)

record type-theory
(l1 l2 : Level) : UU (lsuc l1 ⊔ lsuc l2)
where
field
typ : UU l1
sys : system l2 typ
W : weakening sys
S : substitution sys
δ : generic-element sys
WW : weakening-preserves-weakening W
SS : substitution-preserves-substitution S
WS : weakening-preserves-substitution W S
SW : substitution-preserves-weakening W S
Wδ : weakening-preserves-generic-element W δ
Sδ : substitution-preserves-generic-element S δ
S!W : substitution-cancels-weakening W S
δid : generic-element-is-identity S δ
Sδ! : substitution-by-generic-element W S δ

slice-type-theory :
{l1 l2 : Level} (T : type-theory l1 l2)
(X : type-theory.typ T) →
type-theory l1 l2
type-theory.typ (slice-type-theory T X) =
type-theory.typ T
type-theory.sys (slice-type-theory T X) =
system.slice (type-theory.sys T) X
type-theory.W (slice-type-theory T X) =
weakening.slice (type-theory.W T) X
type-theory.S (slice-type-theory T X) =
substitution.slice (type-theory.S T) X
type-theory.δ (slice-type-theory T X) =
generic-element.slice (type-theory.δ T) X
type-theory.WW (slice-type-theory T X) =
weakening-preserves-weakening.slice (type-theory.WW T) X
type-theory.SS (slice-type-theory T X) =
substitution-preserves-substitution.slice (type-theory.SS T) X
type-theory.WS (slice-type-theory T X) =
weakening-preserves-substitution.slice (type-theory.WS T) X
type-theory.SW (slice-type-theory T X) =
substitution-preserves-weakening.slice (type-theory.SW T) X
type-theory.Wδ (slice-type-theory T X) =
weakening-preserves-generic-element.slice (type-theory.Wδ T) X
type-theory.Sδ (slice-type-theory T X) =
substitution-preserves-generic-element.slice (type-theory.Sδ T) X
type-theory.S!W (slice-type-theory T X) =
substitution-cancels-weakening.slice (type-theory.S!W T) X
type-theory.δid (slice-type-theory T X) =
generic-element-is-identity.slice (type-theory.δid T) X
type-theory.Sδ! (slice-type-theory T X) =
substitution-by-generic-element.slice (type-theory.Sδ! T) X

module dependent-simple
where

open import type-theories.dependent-type-theories
open import type-theories.fibered-dependent-type-theories

system :
{l1 l2 : Level} {T : UU l1} → simple.system l2 T → dependent.system l1 l2
dependent.system.type (system {T = T} A) = T
dependent.system.element (system A) X =
simple.system.element A X
dependent.system.slice (system A) X =
system (simple.system.slice A X)

fibered-system :
{l1 l2 l3 l4 : Level}
{T : UU l1} {A : simple.system l2 T} {S : T → UU l3} →
simple.fibered-system l4 S A →
dependent.fibered-system l3 l4 (system A)
dependent.fibered-system.type (fibered-system {S = S} B) = S
dependent.fibered-system.element (fibered-system B) Y =
simple.fibered-system.element B Y
dependent.fibered-system.slice (fibered-system B) Y =
fibered-system (simple.fibered-system.slice B Y)

section-system :
{l1 l2 l3 l4 : Level}
{T : UU l1} {A : simple.system l2 T} {S : T → UU l3}
{B : simple.fibered-system l4 S A} {f : (X : T) → S X} →
simple.section-system B f → dependent.section-system (fibered-system B)
dependent.section-system.type (section-system {B = B} {f} g) X = f X
dependent.section-system.element (section-system {B = B} {f} g) x =
simple.section-system.element g x
dependent.section-system.slice (section-system {B = B} {f} g) X =
section-system (simple.section-system.slice g X)

Eq-fibered-system' :
{l1 l2 l3 l4 : Level}
{T : UU l1} {A : simple.system l2 T} {S : T → UU l3}
{B B' : simple.fibered-system l4 S A} (α : Id B B')
{f f' : (X : T) → S X}
(g : simple.section-system B f) (g' : simple.section-system B' f') →
fibered.hom-fibered-system
( dependent.id-hom-system (system A))
( fibered-system (simple.Eq-fibered-system' α g g'))
( dependent.Eq-fibered-system'
( ap fibered-system α)
( section-system g)
( section-system g'))
fibered.section-fibered-system.type (Eq-fibered-system' refl f g) Y = Y
fibered.section-fibered-system.element (Eq-fibered-system' refl f g) y = y
fibered.section-fibered-system.slice (Eq-fibered-system' refl f g) Y =
{!Eq-fibered-system' ? ? ? !}

htpy-section-system' :
{l1 l2 l3 l4 : Level}
{T : UU l1} {A : simple.system l2 T} {S : T → UU l3}
{B B' : simple.fibered-system l4 S A} (α : Id B B') {f f' : (X : T) → S X}
{H : f ~ f'} {g : simple.section-system B f}
{g' : simple.section-system B' f'} → simple.htpy-section-system' α H g g' →
dependent.htpy-section-system'
( ap fibered-system α)
( section-system g)
( section-system g')
dependent.section-system.type (htpy-section-system' refl {H = H} K) = H
dependent.section-system.element (htpy-section-system' refl {H = H} K) =
simple.section-system.element K
dependent.section-system.slice (htpy-section-system' refl {H = H} K) X =
{!htpy-section-system' ? ? !}

htpy-section-system :
{l1 l2 l3 l4 : Level}
{T : UU l1} {A : simple.system l2 T} {S : T → UU l3}
{B : simple.fibered-system l4 S A} {f f' : (X : T) → S X} {H : f ~ f'}
{g : simple.section-system B f} {g' : simple.section-system B f'} →
simple.htpy-section-system H g g' →
dependent.htpy-section-system (section-system g) (section-system g')
dependent.section-system.type (htpy-section-system {H = H} K) = H
dependent.section-system.element (htpy-section-system {H = H} K) =
simple.section-system.element K
dependent.section-system.slice (htpy-section-system {H = H} K) X =
{!htpy-section-system ? !}

hom-system :
{l1 l2 l3 l4 : Level} {T : UU l1} {S : UU l3} {f : T → S}
{A : simple.system l2 T} {B : simple.system l4 S} →
simple.hom-system f A B →
dependent.hom-system (system A) (system B)
dependent.section-system.type (hom-system {f = f} h) = f
dependent.section-system.element (hom-system h) =
simple.section-system.element h
dependent.section-system.slice (hom-system h) X =
hom-system (simple.section-system.slice h X)

comp-hom-system :
{l1 l2 l3 l4 l5 l6 : Level}
{T : UU l1} {S : UU l2} {R : UU l3}
{g : S → R} {f : T → S} {A : simple.system l4 T} {B : simple.system l5 S}
{C : simple.system l6 R} (k : simple.hom-system g B C)
(h : simple.hom-system f A B) →
dependent.htpy-hom-system
( hom-system
( simple.comp-hom-system k h))
( dependent.comp-hom-system
( hom-system k)
( hom-system h))
dependent.section-system.type (comp-hom-system k h) X = refl
dependent.section-system.element (comp-hom-system k h) x = refl
dependent.section-system.slice (comp-hom-system {f = f} k h) X =
comp-hom-system
( simple.section-system.slice k (f X))
( simple.section-system.slice h X)

htpy-hom-system :
{l1 l2 l3 l4 : Level}
{T : UU l1} {S : UU l2} {f : T → S}
{A : simple.system l3 T} {B : simple.system l4 S}
{g h : simple.hom-system f A B} →
simple.htpy-hom-system g h →
dependent.htpy-hom-system (hom-system g) (hom-system h)
dependent.section-system.type (htpy-hom-system H) = refl-htpy
dependent.section-system.element (htpy-hom-system {f = f} H) {X} x =
simple.section-system.element {f = {!!}} H x
--simple.section-system.element H {X} x
dependent.section-system.slice (htpy-hom-system H) X =
{!!} --htpy-hom-system (simple.section-system.slice H X)

weakening :
{l1 l2 : Level} {T : UU l1} {A : simple.system l2 T} →
simple.weakening A → dependent.weakening (system A)
dependent.weakening.type (weakening W) X =
hom-system (simple.weakening.element W X)
dependent.weakening.slice (weakening W) X =
weakening (simple.weakening.slice W X)

preserves-weakening :
{l1 l2 l3 l4 : Level}
{T : UU l1} {S : UU l2} {f : T → S}
{A : simple.system l3 T} {B : simple.system l4 S}
{WA : simple.weakening A} {WB : simple.weakening B}
{g : simple.hom-system f A B} →
simple.preserves-weakening WA WB g →
dependent.preserves-weakening
( weakening WA)
( weakening WB)
( hom-system g)
dependent.preserves-weakening.type
( preserves-weakening {f = f} {WA = WA} {WB} {g = g} Wg) X =
dependent.concat-htpy-hom-system
( dependent.inv-htpy-hom-system
( comp-hom-system
( simple.section-system.slice g X)
( simple.weakening.element WA X)))
( dependent.concat-htpy-hom-system
( htpy-hom-system (simple.preserves-weakening.element Wg X))
( comp-hom-system
( simple.weakening.element WB (f X))
( g)))
dependent.preserves-weakening.slice (preserves-weakening Wg) X =
preserves-weakening (simple.preserves-weakening.slice Wg X)

substitution :
{l1 l2 : Level} {T : UU l1} {A : simple.system l2 T} →
simple.substitution A →
dependent.substitution (system A)
dependent.substitution.type
( substitution S) x =
hom-system (simple.substitution.element S x)
dependent.substitution.slice
( substitution S) X =
substitution (simple.substitution.slice S X)

generic-element :
{l1 l2 : Level} {T : UU l1} {A : simple.system l2 T} →
(W : simple.weakening A) → simple.generic-element A →
dependent.generic-element (weakening W)
dependent.generic-element.type
( generic-element W δ) X =
simple.generic-element.element δ X
dependent.generic-element.slice
( generic-element W δ) X =
generic-element
( simple.weakening.slice W X)
( simple.generic-element.slice δ X)

weakening-preserves-weakening :
{l1 l2 : Level} {T : UU l1} {A : simple.system l2 T}
{W : simple.weakening A} →
simple.weakening-preserves-weakening W →
dependent.weakening-preserves-weakening (weakening W)
dependent.weakening-preserves-weakening.type
( weakening-preserves-weakening WW) X =
preserves-weakening (simple.weakening-preserves-weakening.element WW X)
dependent.weakening-preserves-weakening.slice
( weakening-preserves-weakening WW) X =
weakening-preserves-weakening
( simple.weakening-preserves-weakening.slice WW X)