{-# OPTIONS --without-K --exact-split --allow-unsolved-metas #-}

module type-theories.simple-type-theories where

open import book public

{- We introduce the category of simple type theories. Those are type theories
   that have no type dependency. The category of simple type theories is 
   equivalent to the category of multisorted algebraic theories. -}

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

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