{-# OPTIONS --prop --rewriting #-}

module initialObs where

open import lib
open import model
open import depModel
open import morphism

-- Initial Model
-- This is a QIIT (quotient inductive-inductive type). Since Agda does not natively support
-- QIITs, we postulate the constructors and the eliminators, along with their computation rules.

-- Sorts
postulate
  Con : Set
  Sub : Con → Con → Set
  Ty  : Con → Set
  Tm  : (Γ : Con) → Ty Γ → Set

-- Forded constructors
postulate
  _∘_       : ∀{Γ Δ Θ} → Sub Δ Γ → Sub Θ Δ → Sub Θ Γ
  id        : ∀{Γ Δ} → (Γ ~ Δ) → Sub Δ Γ
  ◇         : Con
  ε         : ∀{Γ Δ} → (Γ ~ ◇) → Sub Δ Γ
  _[_]T     : ∀{Γ Δ} → Ty Γ → Sub Δ Γ → Ty Δ
  _[_][_]t  : ∀{Γ Δ}{A : Ty Γ}{B : Ty Δ} → Tm Γ A → (σ : Sub Δ Γ) → (B ~ A [ σ ]T) → Tm Δ B
  _▹_       : (Γ : Con) → Ty Γ → Con
  _,[_][_]_ : ∀{Γ Δ Θ}(γ : Sub Δ Γ) → ∀ {A B} → A [ γ ]T ~ B → (Θ ~ Γ ▹ A) → Tm Δ B → Sub Δ Θ
  p         : ∀{Γ Δ}{A : Ty Γ} → (Δ ~ Γ ▹ A) → Sub Δ Γ
  q         : ∀{Γ Δ}{A : Ty Γ}{B : Ty Δ}(h₁ : Δ ~ Γ ▹ A)(h₂ : B ~ A [ p {A = A} ~refl ]T) → Tm Δ B

-- Equalities of the QIIT
postulate
  ass   : ∀{Γ Δ}{γ : Sub Δ Γ}{Θ}{δ : Sub Θ Δ}{Ξ}{θ : Sub Ξ Θ} → ((γ ∘ δ) ∘ θ) ~ (γ ∘ (δ ∘ θ))
  idl   : ∀{Γ Δ}{γ : Sub Δ Γ} → (id ~refl ∘ γ) ~ γ
  idr   : ∀{Γ Δ}{γ : Sub Δ Γ} → (γ ∘ id ~refl) ~ γ
  ◇η    : ∀{Γ}{σ : Sub Γ ◇} → σ ~ (ε {◇}{Γ} ~refl)
  [∘]T  : ∀{Γ}{A : Ty Γ}{Δ}{γ : Sub Δ Γ}{Θ}{δ : Sub Θ Δ} → A [ γ ∘ δ ]T ~ A [ γ ]T [ δ ]T
  [id]T : ∀{Γ}{A : Ty Γ} → A [ id ~refl ]T ~ A
  [∘]t  : ∀{Γ}{A : Ty Γ}{a : Tm Γ A}{Δ}{γ : Sub Δ Γ}{Θ}{δ : Sub Θ Δ} → a [ γ ∘ δ ][ ~refl ]t ~ a [ γ ][ ~refl ]t [ δ ][ ~refl ]t
  [id]t : ∀{Γ}{A : Ty Γ}{a : Tm Γ A} → a [ id ~refl ][ ~refl ]t ~ a
  ▹β₁   : ∀{Γ Δ}{γ : Sub Δ Γ}{A}{a : Tm Δ (A [ γ ]T)} → p ~refl ∘ (γ ,[ ~refl ][ ~refl ] a) ~ γ
  ▹β₂   : ∀{Γ Δ}{γ : Sub Δ Γ}{A}{a : Tm Δ (A [ γ ]T)} → (q ~refl ~refl) [ γ ,[ ~refl ][ ~refl ] a ][ ~refl ]t ~ a
  ▹η    : ∀{Γ Δ A}{γa : Sub Δ (Γ ▹ A)} → ((p ~refl ∘ γa) ,[ [∘]T ][ ~refl ] ((q ~refl ~refl) [ γa ][ ~refl ]t)) ~ γa

-- Observational equalities
postulate
  eq∘₁   : ∀{Γ Γ' Δ Θ Θ'}(γ : Sub Δ Γ)(δ : Sub Θ Δ) → Sub Θ Γ ≡ Sub Θ' Γ'
         → Sub Δ Γ ≡ Sub Δ Γ'
  eq∘₂   : ∀{Γ Γ' Δ Θ Θ'}(γ : Sub Δ Γ)(δ : Sub Θ Δ) → Sub Θ Γ ≡ Sub Θ' Γ'
         → Sub Θ Δ ≡ Sub Θ' Δ
  eq-id  : ∀{Γ Γ' Δ Δ'}(h : Γ ~ Δ)(e : Sub Δ Γ ≡ Sub Δ' Γ')
         → (Γ ~ Δ) ~ (Γ' ~ Δ')
  eqε    : ∀{Γ Γ' Δ Δ'}(h : Γ ~ ◇)(e : Sub Δ Γ ≡ Sub Δ' Γ')
         → (Γ ~ ◇) ~ (Γ' ~ ◇)
  eq[T]  : ∀{Γ Δ Δ'}(A : Ty Γ)(σ : Sub Δ Γ)(e : Ty Δ ≡ Ty Δ')
         → (Sub Δ Γ) ≡ (Sub Δ' Γ)
  eq[t]₁ : ∀{Γ Δ Δ'}{A : Ty Γ}{B : Ty Δ}{B' : Ty Δ'}(a : Tm Γ A)(σ : Sub Δ Γ)(h : B ~ A [ σ ]T)(e : Tm Δ B ≡ Tm Δ' B')
         → (Sub Δ Γ) ≡ (Sub Δ' Γ)
  eq[t]₂ : ∀{Γ Δ Δ'}{A : Ty Γ}{B : Ty Δ}{B' : Ty Δ'}(a : Tm Γ A)(σ : Sub Δ Γ)(h : B ~ A [ σ ]T)(e : Tm Δ B ≡ Tm Δ' B')
         → (B ~ A [ σ ]T) ~ (B' ~ A [ (coe≡ {_}{Sub Δ Γ}{Sub Δ' Γ} (eq[t]₁ a σ h e) σ) ]T)
  eq,₁   : ∀{Γ Δ Δ' Θ Θ'}(σ : Sub Δ Γ){A : Ty Γ}{B : Ty Δ}(h₁ : A [ σ ]T ~ B)(h₂ : Θ ~ Γ ▹ A)(a : Tm Δ B)(e : Sub Δ Θ ≡ Sub Δ' Θ')
         → Sub Δ Γ ≡ Sub Δ' Γ
  eq,₂   : ∀{Γ Δ Δ' Θ Θ'}(σ : Sub Δ Γ){A : Ty Γ}{B : Ty Δ}(h₁ : A [ σ ]T ~ B)(h₂ : Θ ~ Γ ▹ A)(a : Tm Δ B)(e : Sub Δ Θ ≡ Sub Δ' Θ')
         → Ty Δ ≡ Ty Δ'
  eq,₃   : ∀{Γ Δ Δ' Θ Θ'}(σ : Sub Δ Γ){A : Ty Γ}{B : Ty Δ}(h₁ : A [ σ ]T ~ B)(h₂ : Θ ~ Γ ▹ A)(a : Tm Δ B)(e : Sub Δ Θ ≡ Sub Δ' Θ')
         → (A [ σ ]T ~ B) ~ (A [ coe≡ (eq,₁ σ h₁ h₂ a e) σ ]T ~ coe≡ (eq,₂ σ h₁ h₂ a e) B)
  eq,₄   : ∀{Γ Δ Δ' Θ Θ'}(σ : Sub Δ Γ){A : Ty Γ}{B : Ty Δ}(h₁ : A [ σ ]T ~ B)(h₂ : Θ ~ Γ ▹ A)(a : Tm Δ B)(e : Sub Δ Θ ≡ Sub Δ' Θ')
         → (Θ ~ Γ ▹ A) ~ (Θ' ~ Γ ▹ A)
  eq,₅   : ∀{Γ Δ Δ' Θ Θ'}(σ : Sub Δ Γ){A : Ty Γ}{B : Ty Δ}(h₁ : A [ σ ]T ~ B)(h₂ : Θ ~ Γ ▹ A)(a : Tm Δ B)(e : Sub Δ Θ ≡ Sub Δ' Θ')
         → Tm Δ B ≡ Tm Δ' (coe≡ {_}{Ty Δ}{Ty Δ'} (eq,₂ σ h₁ h₂ a e) B)
  eq-p₁  : ∀{Γ Γ' Δ Δ'}{A : Ty Γ}(h : Δ ~ Γ ▹ A)(e : Sub Δ Γ ≡ Sub Δ' Γ')
         → Ty Γ ≡ Ty Γ'
  eq-p₂  : ∀{Γ Γ' Δ Δ'}{A : Ty Γ}(h : Δ ~ Γ ▹ A)(e : Sub Δ Γ ≡ Sub Δ' Γ')
         → (Δ ~ Γ ▹ A) ~ (Δ' ~ Γ' ▹ (coe≡ {_}{Ty Γ}{Ty Γ'} (eq-p₁ h e) A))
  eq-q₁  : ∀{Γ Δ Δ'}{A : Ty Γ}{B : Ty Δ}{B' : Ty Δ'}(h₁ : Δ ~ Γ ▹ A)(h₂ : B ~ A [ p {A = A} ~refl ]T)(e : Tm Δ B ≡ Tm Δ' B')
         → (Δ ~ Γ ▹ A) ~ (Δ' ~ Γ ▹ A)
  eq-q₂  : ∀{Γ Δ Δ'}{A : Ty Γ}{B : Ty Δ}{B' : Ty Δ'}(h₁ : Δ ~ Γ ▹ A)(h₂ : B ~ A [ p {A = A} ~refl ]T)(e : Tm Δ B ≡ Tm Δ' B')
         → (B ~ A [ p {A = A} ~refl ]T) ~ (B' ~ A [ p {A = A} ~refl ]T)

-- Coercion rules
postulate
  coe∘   : ∀{Γ Γ' Δ Θ Θ'} → (γ : Sub Δ Γ) → (δ : Sub Θ Δ) (e : Sub Θ Γ ≡ Sub Θ' Γ')
         → coe≡ {_}{Sub Θ Γ}{Sub Θ' Γ'} e (_∘_ {Γ}{Δ}{Θ} γ δ) ≡ (coe≡ (eq∘₁ γ δ e) γ) ∘ (coe≡ (eq∘₂ γ δ e) δ)
  coe-id : ∀ {Γ Γ' Δ Δ'} → (h : Γ ~ Δ) (e : Sub Δ Γ ≡ Sub Δ' Γ')
         → coe≡ {_}{Sub Δ Γ}{Sub Δ' Γ'} e (id {Γ}{Δ} h) ≡ id (coeₚ (eq-id h e) h)
  -- coe◇   : coe≡ {_}{Con}{Con} e ◇ ≡ ◇
  coeε   : ∀ {Γ Γ' Δ Δ'} → (h : Γ ~ ◇) (e : Sub Δ Γ ≡ Sub Δ' Γ')
         → coe≡ {_}{Sub Δ Γ}{Sub Δ' Γ'} e (ε {Γ}{Δ} h) ≡ ε {Γ'}{Δ'} (coeₚ (eqε h e) h)
  coe[T] : ∀ {Γ Δ Δ'}(A : Ty Γ)(σ : Sub Δ Γ)(e : Ty Δ ≡ Ty Δ')
         → coe≡ {_}{Ty Δ}{Ty Δ'} e (_[_]T {Γ}{Δ} A σ) ≡ _[_]T {Γ}{Δ'} A (coe≡ (eq[T] A σ e) σ)
  coe[t] : ∀ {Γ Δ Δ'}{A : Ty Γ}{B : Ty Δ}{B' : Ty Δ'}(a : Tm Γ A)(σ : Sub Δ Γ)(h : B ~ A [ σ ]T)(e : Tm Δ B ≡ Tm Δ' B')
         → coe≡ {_}{Tm Δ B}{Tm Δ' B'} e (_[_][_]t {Γ}{Δ}{A}{B} a σ h)
           ≡ _[_][_]t {Γ}{Δ'}{A}{B'} a (coe≡ (eq[t]₁ a σ h e) σ) (coeₚ (eq[t]₂ a σ h e) h)
  -- coe▹   : coe≡ {_}{Con}{Con} e (σ ▹ a) ≡ σ ▹ a
  coe,   : ∀{Γ Δ Δ' Θ Θ'}(σ : Sub Δ Γ){A : Ty Γ}{B : Ty Δ}(h₁ : A [ σ ]T ~ B)(h₂ : Θ ~ Γ ▹ A)(a : Tm Δ B)(e : Sub Δ Θ ≡ Sub Δ' Θ')
         → coe≡ {_}{Sub Δ Θ}{Sub Δ' Θ'} e (_,[_][_]_ {Γ}{Δ}{Θ} σ {A}{B} h₁ h₂ a)
           ≡ _,[_][_]_ {Γ}{Δ'}{Θ'}(coe≡ (eq,₁ σ h₁ h₂ a e) σ){A}{coe≡ (eq,₂ σ h₁ h₂ a e) B}(coeₚ (eq,₃ σ h₁ h₂ a e) h₁)
                       (coeₚ (eq,₄ σ h₁ h₂ a e) h₂)(coe≡ (eq,₅ σ h₁ h₂ a e) a)
  coe-p  : ∀{Γ Γ' Δ Δ'}{A : Ty Γ}(h : Δ ~ Γ ▹ A)(e : Sub Δ Γ ≡ Sub Δ' Γ')
         → coe≡ {_}{Sub Δ Γ}{Sub Δ' Γ'} e (p {Γ}{Δ}{A} h) ≡ p (coeₚ (eq-p₂ h e) h)
  coe-q  : ∀{Γ Δ Δ'}{A : Ty Γ}{B : Ty Δ}{B' : Ty Δ'}(h₁ : Δ ~ Γ ▹ A)(h₂ : B ~ A [ p ~refl ]T)(e : Tm Δ B ≡ Tm Δ' B')
         → coe≡ {_}{Tm Δ B}{Tm Δ' B'} e (q {Γ}{Δ}{A}{B} h₁ h₂) ≡ q (coeₚ (eq-q₁ h₁ h₂ e) h₁) (coeₚ (eq-q₂ h₁ h₂ e) h₂)

{-# REWRITE coe∘ coe-id coeε coe[T] coe[t] coe, coe-p coe-q #-}

Ci : CwF {lzero}{lzero}{lzero}{lzero}
Ci = record
      { Con = Con
      ; Sub = Sub
      ; _∘_ = λ γ δ → γ ∘ δ
      ; ass = ass
      ; id = id ~refl
      ; idl = idl
      ; idr = idr
      ; ◇ = ◇
      ; ε = ε ~refl
      ; ◇η = ◇η
      ; Ty = Ty
      ; _[_]T = λ A σ → A [ σ ]T
      ; [∘]T = [∘]T
      ; [id]T = [id]T
      ; Tm = Tm
      ; _[_]t = λ a σ → a [ σ ][ ~refl ]t
      ; [∘]t = [∘]t
      ; [id]t = [id]t
      ; _▹_ = _▹_
      ; _,[_]_ = λ γ {A}{A'} e a → _,[_][_]_ γ e ~refl a
      ; p = λ {Γ}{A} → p ~refl
      ; q = λ {Γ}{A} → q ~refl ~refl
      ; ▹β₁ = ▹β₁
      ; ▹β₂ = ▹β₂
      ; ▹η = ▹η
      }

open CwF-tools Ci

-- Forded constructors, part 2
postulate
  Π   : ∀{Γ}(A : Ty Γ) → Ty (Γ ▹ A) → Ty Γ
  lam : ∀{Γ}{X : Ty Γ}{A : Ty Γ}{B : Ty (Γ ▹ A)}(t : Tm (Γ ▹ A) B)(h : X ~ Π A B) → Tm Γ X
  app : ∀{Γ}{X : Ty Γ}{A : Ty Γ}{B : Ty (Γ ▹ A)}(t : Tm Γ (Π A B))(u : Tm Γ A)(h : X ~ (B [ sg u ]T)) → Tm Γ X
  𝔹   : ∀{Γ : Con}(h : Γ ~ ◇) → Ty Γ
  𝕥   : ∀{Γ : Con}{A : Ty Γ}(h₁ : Γ ~ ◇)(h₂ : A ~ 𝔹 ~refl) → Tm Γ A
  𝕗   : ∀{Γ : Con}{A : Ty Γ}(h₁ : Γ ~ ◇)(h₂ : A ~ 𝔹 ~refl) → Tm Γ A
  ifᵀ : ∀{Γ} → Tm Γ ((𝔹 ~refl) [ ε ~refl ]T) → Ty Γ → Ty Γ → Ty Γ
  ifᵗ : ∀{Γ}{X : Ty Γ}(P : Ty (Γ ▹ (𝔹 ~refl [ ε ~refl ]T)))(P𝕥 : Tm Γ (P [ sg (𝕥 ~refl ~refl [ ε ~refl ][ ~refl ]t) ]T))
         (P𝕗 : Tm Γ (P [ sg (𝕗 ~refl ~refl [ ε ~refl ][ ~refl ]t) ]T))(b : Tm Γ (𝔹 ~refl [ ε ~refl ]T))(h : X ~ (P [ sg b ]T)) → Tm Γ X

-- Equalities of the QIIT, part 2
postulate
  Π[]   : ∀{Γ}{A : Ty Γ}{B : Ty (Γ ▹ A)}{Δ}{γ : Sub Δ Γ} → (Π A B) [ γ ]T ~ Π (A [ γ ]T) (B [ ↑ γ ]T)
  lam[] : ∀{Γ}{A : Ty Γ}{B : Ty (Γ ▹ A)}{t : Tm (Γ ▹ A) B}{Δ}{γ : Sub Δ Γ} → (lam t ~refl) [ γ ][ ~refl ]t ~ lam (t [ ↑ γ ][ ~refl ]t) ~refl
  app[] : ∀{Γ}{A : Ty Γ}{B : Ty (Γ ▹ A)}{t : Tm Γ (Π A B)}{u : Tm Γ A}{Δ}{γ : Sub Δ Γ}
           → (app t u ~refl) [ γ ][ ~refl ]t ~ app (coe (cong (Tm Δ) Π[]) (t [ γ ][ ~refl ]t)) (u [ γ ][ ~refl ]t) ~refl
  Πβ    : ∀{Γ}{A : Ty Γ}{B : Ty (Γ ▹ A)}{t : Tm (Γ ▹ A) B}{a : Tm Γ A} → app (lam t ~refl) a ~refl ~ t [ sg a ][ ~refl ]t
  Πη    : ∀{Γ}{A : Ty Γ}{B : Ty (Γ ▹ A)}{t : Tm Γ (Π A B)}
           → t ~ lam {A = A} {B = B [ ↑ (p ~refl) ]T [ sg (q ~refl ~refl) ]T}
                     (app (coe (cong (Tm (Γ ▹ A)) Π[]) (t [ p ~refl ][ ~refl ]t)) (q ~refl ~refl) ~refl) ~refl
  ifᵀ[] : ∀{Γ}{b : Tm Γ (𝔹 ~refl [ ε ~refl ]T)}{A B : Ty Γ}{Δ}{γ : Sub Δ Γ}
           → (ifᵀ b A B) [ γ ]T ~ ifᵀ (coe (cong (Tm Δ) ε[]T) (b [ γ ][ ~refl ]t)) (A [ γ ]T) (B [ γ ]T)
  ifᵀβ₁ : ∀{Γ}{A B : Ty Γ} → ifᵀ (𝕥 ~refl ~refl [ ε ~refl ][ ~refl ]t) A B ~ A
  ifᵀβ₂ : ∀{Γ}{A B : Ty Γ} → ifᵀ (𝕗 ~refl ~refl [ ε ~refl ][ ~refl ]t) A B ~ B
  ifᵗ[] : ∀{Γ} {P : Ty (Γ ▹ (𝔹 ~refl [ ε ~refl ]T))}{P𝕥 : Tm Γ (P [ sg (𝕥 ~refl ~refl [ ε ~refl ][ ~refl ]t) ]T)}
           {P𝕗 : Tm Γ (P [ sg (𝕗 ~refl ~refl [ ε ~refl ][ ~refl ]t) ]T)}{b : Tm Γ (𝔹 ~refl [ ε ~refl ]T)}{Δ}{γ : Sub Δ Γ}
          → (ifᵗ P P𝕥 P𝕗 b ~refl) [ γ ][ ~refl ]t
            ~ ifᵗ (P [ ↑ε γ ]T)
                  (coe (cong (Tm Δ) (Ty-↑ε-sg (𝕥 ~refl ~refl) P γ)) (P𝕥 [ γ ][ ~refl ]t))
                  (coe (cong (Tm Δ) (Ty-↑ε-sg (𝕗 ~refl ~refl) P γ)) (P𝕗 [ γ ][ ~refl ]t))
                  (coe (cong (Tm Δ) ε[]T) (b [ γ ][ ~refl ]t)) ~refl
  ifᵗβ₁ : ∀{Γ}{P : Ty (Γ ▹ (𝔹 ~refl [ ε ~refl ]T))} {P𝕥 : Tm Γ (P [ sg (𝕥 ~refl ~refl [ ε ~refl ][ ~refl ]t) ]T)}
           {P𝕗 : Tm Γ (P [ sg (𝕗 ~refl ~refl [ ε ~refl ][ ~refl ]t) ]T)}
          → ifᵗ P P𝕥 P𝕗 (𝕥 ~refl ~refl [ ε ~refl ][ ~refl ]t) ~refl ~ P𝕥
  ifᵗβ₂ : ∀{Γ}{P : Ty (Γ ▹ (𝔹 ~refl [ ε ~refl ]T))} {P𝕥 : Tm Γ (P [ sg (𝕥 ~refl ~refl [ ε ~refl ][ ~refl ]t) ]T)}
           {P𝕗 : Tm Γ (P [ sg (𝕗 ~refl ~refl [ ε ~refl ][ ~refl ]t) ]T)}
          → ifᵗ P P𝕥 P𝕗 (𝕗 ~refl ~refl [ ε ~refl ][ ~refl ]t) ~refl ~ P𝕗

-- Observational equalities, part 2
  eqΠ     : ∀{Γ Γ'}(A : Ty Γ)(B : Ty (Γ ▹ A))(e : Ty Γ ≡ Ty Γ')
          → Ty (Γ ▹ A) ≡ Ty (Γ' ▹ (coe≡ e A))
  eq-lam₁ : ∀{Γ Γ'}{X : Ty Γ}{X' : Ty Γ'}{A : Ty Γ}{B : Ty (Γ ▹ A)}(t : Tm (Γ ▹ A) B)(h : X ~ Π A B)(e : Tm Γ X ≡ Tm Γ' X')
          → Ty Γ ≡ Ty Γ'
  eq-lam₂ : ∀{Γ Γ'}{X : Ty Γ}{X' : Ty Γ'}{A : Ty Γ}{B : Ty (Γ ▹ A)}(t : Tm (Γ ▹ A) B)(h : X ~ Π A B)(e : Tm Γ X ≡ Tm Γ' X')
          → Ty (Γ ▹ A) ≡ Ty (Γ' ▹ (coe≡ (eq-lam₁ t h e) A))
  eq-lam₃ : ∀{Γ Γ'}{X : Ty Γ}{X' : Ty Γ'}{A : Ty Γ}{B : Ty (Γ ▹ A)}(t : Tm (Γ ▹ A) B)(h : X ~ Π A B)(e : Tm Γ X ≡ Tm Γ' X')
          → Tm (Γ ▹ A) B ≡ Tm (Γ' ▹ (coe≡ (eq-lam₁ t h e) A)) (coe≡ (eq-lam₂ t h e) B)
  eq-lam₄ : ∀{Γ Γ'}{X : Ty Γ}{X' : Ty Γ'}{A : Ty Γ}{B : Ty (Γ ▹ A)}(t : Tm (Γ ▹ A) B)(h : X ~ Π A B)(e : Tm Γ X ≡ Tm Γ' X')
          → (X ~ Π A B) ~ (X' ~ Π (coe≡ (eq-lam₁ t h e) A) (coe≡ (eq-lam₂ t h e) B))
  eq-app₁ : ∀{Γ Γ'}{X : Ty Γ}{X' : Ty Γ'}{A : Ty Γ}{B : Ty (Γ ▹ A)}(t : Tm Γ (Π A B))(u : Tm Γ A)(h : X ~ (B [ sg u ]T))(e : Tm Γ X ≡ Tm Γ' X')
          → Ty Γ ≡ Ty Γ'
  eq-app₂ : ∀{Γ Γ'}{X : Ty Γ}{X' : Ty Γ'}{A : Ty Γ}{B : Ty (Γ ▹ A)}(t : Tm Γ (Π A B))(u : Tm Γ A)(h : X ~ (B [ sg u ]T))(e : Tm Γ X ≡ Tm Γ' X')
          → Ty (Γ ▹ A) ≡ Ty (Γ' ▹ (coe≡ (eq-app₁ t u h e) A))
  eq-app₃ : ∀{Γ Γ'}{X : Ty Γ}{X' : Ty Γ'}{A : Ty Γ}{B : Ty (Γ ▹ A)}(t : Tm Γ (Π A B))(u : Tm Γ A)(h : X ~ (B [ sg u ]T))(e : Tm Γ X ≡ Tm Γ' X')
          → Tm Γ (Π A B) ≡ Tm Γ' (Π (coe≡ (eq-app₁ t u h e) A) (coe≡ (eq-app₂ t u h e) B))
  eq-app₄ : ∀{Γ Γ'}{X : Ty Γ}{X' : Ty Γ'}{A : Ty Γ}{B : Ty (Γ ▹ A)}(t : Tm Γ (Π A B))(u : Tm Γ A)(h : X ~ (B [ sg u ]T))(e : Tm Γ X ≡ Tm Γ' X')
          → Tm Γ A ≡ Tm Γ' (coe≡ (eq-app₁ t u h e) A)
  eq-app₅ : ∀{Γ Γ'}{X : Ty Γ}{X' : Ty Γ'}{A : Ty Γ}{B : Ty (Γ ▹ A)}(t : Tm Γ (Π A B))(u : Tm Γ A)(h : X ~ (B [ sg u ]T))(e : Tm Γ X ≡ Tm Γ' X')
          → (X ~ (B [ sg u ]T)) ~ (X' ~ ((coe≡ (eq-app₂ t u h e) B) [ sg (coe≡ (eq-app₄ t u h e) u) ]T))
  eq𝔹     : ∀{Γ Γ'}(h : Γ ~ ◇)(e : Ty Γ ≡ Ty Γ')
          → (Γ ~ ◇) ~ (Γ' ~ ◇)
  eq𝕓₁    : ∀{Γ Γ'}{A : Ty Γ}{A' : Ty Γ'}(h₁ : Γ ~ ◇)(h₂ : A ~ 𝔹 ~refl)(e : Tm Γ A ≡ Tm Γ' A')
          → (Γ ~ ◇) ~ (Γ' ~ ◇)
  eq𝕓₂    : ∀{Γ Γ'}{A : Ty Γ}{A' : Ty Γ'}(h₁ : Γ ~ ◇)(h₂ : A ~ 𝔹 ~refl)(e : Tm Γ A ≡ Tm Γ' A')
          → (A ~ 𝔹 ~refl) ~ (A' ~ 𝔹 ~refl)
  eq-ifᵀ  : ∀{Γ Γ'}(b : Tm Γ ((𝔹 ~refl) [ ε ~refl ]T))(A : Ty Γ)(B : Ty Γ)(e : Ty Γ ≡ Ty Γ')
          → Tm Γ ((𝔹 ~refl) [ ε ~refl ]T) ≡ Tm Γ' ((𝔹 ~refl) [ ε ~refl ]T)
  eq-ifᵗ₁ : ∀{Γ Γ'}{X : Ty Γ}{X' : Ty Γ'}(P : Ty (Γ ▹ (𝔹 ~refl [ ε ~refl ]T)))(P𝕥 : Tm Γ (P [ sg (𝕥 ~refl ~refl [ ε ~refl ][ ~refl ]t) ]T))
            (P𝕗 : Tm Γ (P [ sg (𝕗 ~refl ~refl [ ε ~refl ][ ~refl ]t) ]T))(b : Tm Γ (𝔹 ~refl [ ε ~refl ]T))(h : X ~ (P [ sg b ]T))
            (e : Tm Γ X ≡ Tm Γ' X')
          → Ty (Γ ▹ (𝔹 ~refl [ ε ~refl ]T)) ≡ Ty (Γ' ▹ (𝔹 ~refl [ ε ~refl ]T))
  eq-ifᵗ₂ : ∀{Γ Γ'}{X : Ty Γ}{X' : Ty Γ'}(P : Ty (Γ ▹ (𝔹 ~refl [ ε ~refl ]T)))(P𝕥 : Tm Γ (P [ sg (𝕥 ~refl ~refl [ ε ~refl ][ ~refl ]t) ]T))
            (P𝕗 : Tm Γ (P [ sg (𝕗 ~refl ~refl [ ε ~refl ][ ~refl ]t) ]T))(b : Tm Γ (𝔹 ~refl [ ε ~refl ]T))(h : X ~ (P [ sg b ]T))
            (e : Tm Γ X ≡ Tm Γ' X')
          → Tm Γ (P [ sg (𝕥 ~refl ~refl [ ε ~refl ][ ~refl ]t) ]T)
            ≡ Tm Γ' ((coe≡ (eq-ifᵗ₁ P P𝕥 P𝕗 b h e) P) [ sg (𝕥 ~refl ~refl [ ε ~refl ][ ~refl ]t) ]T)
  eq-ifᵗ₃ : ∀{Γ Γ'}{X : Ty Γ}{X' : Ty Γ'}(P : Ty (Γ ▹ (𝔹 ~refl [ ε ~refl ]T)))(P𝕥 : Tm Γ (P [ sg (𝕥 ~refl ~refl [ ε ~refl ][ ~refl ]t) ]T))
            (P𝕗 : Tm Γ (P [ sg (𝕗 ~refl ~refl [ ε ~refl ][ ~refl ]t) ]T))(b : Tm Γ (𝔹 ~refl [ ε ~refl ]T))(h : X ~ (P [ sg b ]T))
            (e : Tm Γ X ≡ Tm Γ' X')
          → Tm Γ (P [ sg (𝕗 ~refl ~refl [ ε ~refl ][ ~refl ]t) ]T)
            ≡ Tm Γ' ((coe≡ (eq-ifᵗ₁ P P𝕥 P𝕗 b h e) P) [ sg (𝕗 ~refl ~refl [ ε ~refl ][ ~refl ]t) ]T)
  eq-ifᵗ₄ : ∀{Γ Γ'}{X : Ty Γ}{X' : Ty Γ'}(P : Ty (Γ ▹ (𝔹 ~refl [ ε ~refl ]T)))(P𝕥 : Tm Γ (P [ sg (𝕥 ~refl ~refl [ ε ~refl ][ ~refl ]t) ]T))
            (P𝕗 : Tm Γ (P [ sg (𝕗 ~refl ~refl [ ε ~refl ][ ~refl ]t) ]T))(b : Tm Γ (𝔹 ~refl [ ε ~refl ]T))(h : X ~ (P [ sg b ]T))
            (e : Tm Γ X ≡ Tm Γ' X')
          → Tm Γ (𝔹 ~refl [ ε ~refl ]T) ≡ Tm Γ' (𝔹 ~refl [ ε ~refl ]T)
  eq-ifᵗ₅ : ∀{Γ Γ'}{X : Ty Γ}{X' : Ty Γ'}(P : Ty (Γ ▹ (𝔹 ~refl [ ε ~refl ]T)))(P𝕥 : Tm Γ (P [ sg (𝕥 ~refl ~refl [ ε ~refl ][ ~refl ]t) ]T))
            (P𝕗 : Tm Γ (P [ sg (𝕗 ~refl ~refl [ ε ~refl ][ ~refl ]t) ]T))(b : Tm Γ (𝔹 ~refl [ ε ~refl ]T))(h : X ~ (P [ sg b ]T))
            (e : Tm Γ X ≡ Tm Γ' X')
          → (X ~ (P [ sg b ]T)) ~ (X' ~ ((coe≡ (eq-ifᵗ₁ P P𝕥 P𝕗 b h e) P) [ sg (coe≡ (eq-ifᵗ₄ P P𝕥 P𝕗 b h e) b) ]T))

-- Coercion rules, part 2
  coeΠ    : ∀{Γ Γ'}(A : Ty Γ)(B : Ty (Γ ▹ A))(e : Ty Γ ≡ Ty Γ')
          → coe≡ {_}{Ty Γ}{Ty Γ'} e (Π {Γ} A B) ≡ Π (coe≡ e A) (coe≡ {_}{Ty (Γ ▹ A)}{Ty (Γ' ▹ (coe≡ e A))} (eqΠ A B e) B)
  coe-lam : ∀{Γ Γ'}{X : Ty Γ}(X' : Ty Γ'){A : Ty Γ}{B : Ty (Γ ▹ A)}(t : Tm (Γ ▹ A) B)(h : X ~ Π A B)(e : Tm Γ X ≡ Tm Γ' X')
          → coe≡ {_}{Tm Γ X}{Tm Γ' X'} e (lam {Γ}{X}{A}{B} t h)
            ≡ lam {A = coe≡ (eq-lam₁ t h e) A}{coe≡ (eq-lam₂ t h e) B}(coe≡ (eq-lam₃ t h e) t)(coeₚ (eq-lam₄ t h e) h)
  coe𝔹    : ∀{Γ Γ'}(h : Γ ~ ◇)(e : Ty Γ ≡ Ty Γ')
          → coe≡ {_}{Ty Γ}{Ty Γ'} e (𝔹 {Γ} h) ≡ 𝔹 (coeₚ (eq𝔹 h e) h)
  coe𝕥    : ∀{Γ Γ'}{A : Ty Γ}{A' : Ty Γ'}(h₁ : Γ ~ ◇)(h₂ : A ~ 𝔹 ~refl)(e : Tm Γ A ≡ Tm Γ' A')
          → coe≡ {_}{Tm Γ A}{Tm Γ' A'} e (𝕥 {Γ}{A} h₁ h₂) ≡ 𝕥 (coeₚ (eq𝕓₁ h₁ h₂ e) h₁) (coeₚ (eq𝕓₂ h₁ h₂ e) h₂)
  coe𝕗    : ∀{Γ Γ'}{A : Ty Γ}{A' : Ty Γ'}(h₁ : Γ ~ ◇)(h₂ : A ~ 𝔹 ~refl)(e : Tm Γ A ≡ Tm Γ' A')
          → coe≡ {_}{Tm Γ A}{Tm Γ' A'} e (𝕗 {Γ}{A} h₁ h₂) ≡ 𝕗 (coeₚ (eq𝕓₁ h₁ h₂ e) h₁) (coeₚ (eq𝕓₂ h₁ h₂ e) h₂)
  coe-app : ∀{Γ Γ'}{X : Ty Γ}{X' : Ty Γ'}{A : Ty Γ}{B : Ty (Γ ▹ A)}(t : Tm Γ (Π A B))(u : Tm Γ A)(h : X ~ (B [ sg u ]T))(e : Tm Γ X ≡ Tm Γ' X')
          → coe≡ {_}{Tm Γ X}{Tm Γ' X'} e (app {Γ}{X}{A}{B} t u h)
            ≡ app {Γ'}{X'}{coe≡ (eq-app₁ t u h e) A}{coe≡ (eq-app₂ t u h e) B}(coe≡ (eq-app₃ t u h e) t)
                  (coe≡ (eq-app₄ t u h e) u)(coeₚ (eq-app₅ t u h e) h)
  coe-ifᵀ : ∀{Γ Γ'}(b : Tm Γ ((𝔹 ~refl) [ ε ~refl ]T))(A : Ty Γ)(B : Ty Γ)(e : Ty Γ ≡ Ty Γ')
          → coe≡ {_}{Ty Γ}{Ty Γ'} e (ifᵀ {Γ} b A B) ≡ ifᵀ (coe≡ (eq-ifᵀ b A B e) b) (coe≡ e A) (coe≡ e B)
  coe-ifᵗ : ∀{Γ Γ'}{X : Ty Γ}{X' : Ty Γ'}(P : Ty (Γ ▹ (𝔹 ~refl [ ε ~refl ]T)))(P𝕥 : Tm Γ (P [ sg (𝕥 ~refl ~refl [ ε ~refl ][ ~refl ]t) ]T))
            (P𝕗 : Tm Γ (P [ sg (𝕗 ~refl ~refl [ ε ~refl ][ ~refl ]t) ]T))(b : Tm Γ (𝔹 ~refl [ ε ~refl ]T))(h : X ~ (P [ sg b ]T))
            (e : Tm Γ X ≡ Tm Γ' X')
          → coe≡ {_}{Tm Γ X}{Tm Γ' X'} e (ifᵗ {Γ}{X} P P𝕥 P𝕗 b h)
            ≡ ifᵗ (coe≡ (eq-ifᵗ₁ P P𝕥 P𝕗 b h e) P) (coe≡ (eq-ifᵗ₂ P P𝕥 P𝕗 b h e) P𝕥) (coe≡ (eq-ifᵗ₃ P P𝕥 P𝕗 b h e) P𝕗)
                  (coe≡ (eq-ifᵗ₄ P P𝕥 P𝕗 b h e) b) (coeₚ (eq-ifᵗ₅ P P𝕥 P𝕗 b h e) h)

{-# REWRITE coeΠ coe-lam coe𝔹 coe𝕥 coe𝕗 coe-app coe-ifᵀ coe-ifᵗ #-}

Mi : Model Ci
Mi = record
      { Π = Π
      ; Π[] = Π[]
      ; lam = λ A t → lam t ~refl
      ; lam[] = lam[]
      ; app = λ t u → app t u ~refl
      ; app[] = app[]
      ; Πβ = Πβ
      ; Πη = Πη
      ; 𝔹 = 𝔹 ~refl
      ; 𝕥 = 𝕥 ~refl ~refl
      ; 𝕗 = 𝕗 ~refl ~refl
      ; ifᵀ = ifᵀ
      ; ifᵀ[] = ifᵀ[]
      ; ifᵀβ₁ = ifᵀβ₁
      ; ifᵀβ₂ = ifᵀβ₂
      ; ifᵗ = λ P P𝕥 P𝕗 b → ifᵗ P P𝕥 P𝕗 b ~refl
      ; ifᵗ[] = ifᵗ[]
      ; ifᵗβ₁ = ifᵗβ₁
      ; ifᵗβ₂ = ifᵗβ₂
      }

-- Dependent eliminator with its rewrite rules
module initElim {i j k l : Level} (C : DepCwF {lzero}{i}{lzero}{j}{lzero}{k}{lzero}{l} Ci)
                                  (M : DepModel {lzero}{i}{lzero}{j}{lzero}{k}{lzero}{l} Ci C Mi) where
  open DepCwF C
  open DepCwF-tools Ci C
  open DepModel M

  postulate
    elimCon : (Γ : Con) → Con∙ Γ
    elimSub : ∀{Δ Γ}(γ : Sub Δ Γ) → Sub∙ (elimCon Δ) (elimCon Γ) γ
    elimTy  : ∀{Γ}(A : Ty Γ) → Ty∙ (elimCon Γ) A
    elimTm  : ∀{Γ A}(a : Tm Γ A) → Tm∙ (elimCon Γ) (elimTy A) a

    elim◇   : elimCon ◇ ≡ ◇∙
    elim▹   : ∀{Γ A}
            → elimCon (Γ ▹ A) ≡ elimCon Γ ▹∙ elimTy A
    elim∘   : ∀{Γ Δ Θ}{f : Sub Δ Γ}{g : Sub Θ Δ}
            → elimSub {Θ}{Γ}(_∘_ {Γ}{Δ}{Θ} f g) ≡ (elimSub f) ∘∙ (elimSub g)
    elim-id : ∀{Γ Δ}{h : Γ ~ Δ}
            → elimSub {Δ}{Γ}(id {Γ}{Δ} h) ≡ coe (~Jeq (λ Δ e → Sub∙ (elimCon Δ) (elimCon Γ) (id e)) Δ h) (id∙ {Γ}{elimCon Γ})
    elim[]T : ∀{Γ Δ}{f : Sub Δ Γ}{A : Ty Γ}
            → elimTy {Δ}(A [ f ]T) ≡ (elimTy A) [ elimSub f ]T∙

  {-# REWRITE elim◇ elim▹ elim∘ elim-id elim[]T #-}

  postulate
    elimε   : ∀ {Γ}{Δ}(h : Γ ~ ◇)
            → elimSub {Δ}{Γ}(ε {Γ}{Δ} h) ≡ coe (~Jeq' {a = ◇} (λ Γ e → Sub∙ (elimCon Δ) (elimCon Γ) (ε e)) Γ h) (ε∙ {Δ}{elimCon Δ})
    elim[]t : ∀{Γ Δ}{A : Ty Γ}{B : Ty Δ}{a : Tm Γ A}(σ : Sub Δ Γ)(h : B ~ A [ σ ]T)
            → elimTm {Δ}{B}(_[_][_]t {Γ}{Δ}{A}{B} a σ h)
              ≡ coe (~Jeq' {a = A [ σ ]T} (λ B e → Tm∙ (elimCon Δ) (elimTy B) (a [ σ ][ e ]t)) B h) ((elimTm a) [ elimSub σ ]t∙)
    elim,[] : ∀{Γ Δ Θ}(γ : Sub Δ Γ){A : Ty Γ}{B : Ty Δ}(h₁ : A [ γ ]T ~ B)(h₂ : Θ ~ Γ ▹ A)(a : Tm Δ B)
            → elimSub {Δ}{Θ}(_,[_][_]_ {Γ}{Δ}{Θ} γ {A}{B} h₁ h₂ a)
              ≡ coe (~Jeq' {a = Γ ▹ A} (λ Θ e → Sub∙ (elimCon Δ)(elimCon Θ) (γ ,[ h₁ ][ e ] a)) Θ h₂)
                    ((elimSub γ) ,[ h₁ ][ cong (elimTy {Δ}) h₁ ]∙ (elimTm a))
    elim-p  : ∀{Γ Δ}{A : Ty Γ}(h : Δ ~ Γ ▹ A)
            → elimSub {Δ}{Γ}(p {Γ}{Δ}{A} h)
              ≡ coe (~Jeq' {a = Γ ▹ A} (λ Δ e → Sub∙ (elimCon Δ) (elimCon Γ) (p e)) Δ h) (p∙ {Γ}{elimCon Γ}{A}{elimTy A})
    elimΠ   : ∀{Γ}{A : Ty Γ}{B : Ty (Γ ▹ A)}
            → elimTy {Γ}(Π A B) ≡ Π∙ (elimTy A) (elimTy B)
    elim𝔹   : ∀ {Γ}(h : Γ ~ ◇)
            → elimTy {Γ}(𝔹 {Γ} h) ≡ coe (~Jeq' {a = ◇} (λ Γ e → Ty∙ (elimCon Γ) (𝔹 e)) Γ h) 𝔹∙

  {-# REWRITE elimε elim[]t elim,[] elim-p elimΠ elim𝔹 #-}

  postulate
    elim-q  : ∀{Γ Δ}{A : Ty Γ}{B : Ty Δ}(h₁ : Δ ~ Γ ▹ A)(h₂ : B ~ A [ p ~refl ]T)
            → elimTm {Δ}{B}(q {Γ}{Δ}{A}{B} h₁ h₂)
              ≡ coe (~Jeq₂' {A = Con}{Ty}{Γ ▹ A}{A [ p ~refl ]T} (λ Δ e₁ B e₂ → Tm∙ (elimCon Δ)(elimTy B) (q e₁ e₂)) Δ h₁ B h₂)
                    (q∙ {Γ}{elimCon Γ}{A}{elimTy A})
    elim-lam : ∀{Γ}{X : Ty Γ}{A : Ty Γ}{B : Ty (Γ ▹ A)}(t : Tm (Γ ▹ A) B)(h : X ~ Π A B)
             → elimTm {Γ}{X}(lam {Γ}{X}{A}{B} t h)
               ≡ coe (~Jeq' {a = Π A B} (λ X e → Tm∙ (elimCon Γ) (elimTy X) (lam t e)) X h) (lam∙ (elimTy A) (elimTm t))
    elim-app : ∀{Γ}{X : Ty Γ}{A : Ty Γ}{B : Ty (Γ ▹ A)}(t : Tm Γ (Π A B))(u : Tm Γ A)(h : X ~ (B [ sg u ]T))
             → elimTm {Γ}{X}(app {Γ}{X}{A}{B} t u h)
               ≡ coe (~Jeq' {a = B [ sg u ]T} (λ X e → Tm∙ (elimCon Γ) (elimTy X) (app t u e)) X h) (app∙ (elimTm t) (elimTm u))
    elim-𝕥   : ∀{Γ : Con}{A : Ty Γ}(h₁ : Γ ~ ◇)(h₂ : A ~ 𝔹 ~refl)
             → elimTm {Γ}{A}(𝕥 {Γ}{A} h₁ h₂)
               ≡ coe (~Jeq₂' {A = Con}{Ty}{◇}{𝔹 ~refl} (λ Γ e₁ A e₂ → Tm∙ (elimCon Γ) (elimTy A) (𝕥 e₁ e₂)) Γ h₁ A h₂) 𝕥∙
    elim-𝕗   : ∀{Γ : Con}{A : Ty Γ}(h₁ : Γ ~ ◇)(h₂ : A ~ 𝔹 ~refl)
             → elimTm {Γ}{A}(𝕗 {Γ}{A} h₁ h₂)
               ≡ coe (~Jeq₂' {A = Con}{Ty}{◇}{𝔹 ~refl} (λ Γ e₁ A e₂ → Tm∙ (elimCon Γ) (elimTy A) (𝕗 e₁ e₂)) Γ h₁ A h₂) 𝕗∙
    elim-ifᵀ : ∀{Γ}{b : Tm Γ (𝔹 ~refl [ ε ~refl ]T)}{A B : Ty Γ}
             → elimTy {Γ}(ifᵀ {Γ} b A B) ≡ ifᵀ∙ (elimTm b) (elimTy A) (elimTy B)

  {-# REWRITE elim-q elim-lam elim-app elim-𝕥 elim-𝕗 elim-ifᵀ #-}

  postulate
    elim-ifᵗ : ∀{Γ}{X : Ty Γ}(P : Ty (Γ ▹ (𝔹 ~refl [ ε ~refl ]T)))(P𝕥 : Tm Γ (P [ sg (𝕥 ~refl ~refl [ ε ~refl ][ ~refl ]t) ]T))
                (P𝕗 : Tm Γ (P [ sg (𝕗 ~refl ~refl [ ε ~refl ][ ~refl ]t) ]T))(b : Tm Γ (𝔹 ~refl [ ε ~refl ]T))(h : X ~ (P [ sg b ]T))
             → elimTm {Γ}{X}(ifᵗ {Γ}{X} P P𝕥 P𝕗 b h)
               ≡ coe (~Jeq' {a = P [ sg b ]T} (λ X e → Tm∙ (elimCon Γ) (elimTy X) (ifᵗ P P𝕥 P𝕗 b e)) X h)
                     (ifᵗ∙ (elimTy P) (elimTm P𝕥) (elimTm P𝕗) (elimTm b))

  {-# REWRITE elim-ifᵗ #-}


-- proof-irrelevant eliminator
module initInd {i j k l : Level} (C : CwFPred {lzero}{i}{lzero}{j}{lzero}{k}{lzero}{l} Ci)
                                 (M : ModelPred {lzero}{i}{lzero}{j}{lzero}{k}{lzero}{l} Ci C Mi) where
  open CwFPred C
  open ModelPred M

  postulate
    indCon : (Γ : Con) → Con∙ Γ
    indSub : ∀{Δ Γ}(γ : Sub Δ Γ) → Sub∙ (indCon Δ) (indCon Γ) γ
    indTy  : ∀{Γ}(A : Ty Γ) → Ty∙ (indCon Γ) A
    indTm  : ∀{Γ A}(a : Tm Γ A) → Tm∙ (indCon Γ) (indTy A) a


-- nondependent eliminator (also called iterator)
module initIte {i j k l : Level} (C : CwF {i}{j}{k}{l})(M : Model C) where
  private module C = CwF C
  private module M = Model M

  toDepCwF : DepCwF Ci
  toDepCwF = record
       { Con∙ = λ _ → C.Con
       ; Sub∙ = λ Δ Γ _ → C.Sub Δ Γ
       ; _∘∙_ = λ γ δ → γ C.∘ δ
       ; ass∙ = C.ass
       ; id∙ = C.id
       ; idl∙ = C.idl
       ; idr∙ = C.idr
       ; ◇∙ = C.◇
       ; ε∙ = C.ε
       ; ◇η∙ = C.◇η
       ; Ty∙ = λ Γ _ → C.Ty Γ
       ; _[_]T∙ = λ A γ → A C.[ γ ]T
       ; [∘]T∙ = C.[∘]T
       ; [id]T∙ = C.[id]T
       ; Tm∙ = λ Γ A _ → C.Tm Γ A
       ; _[_]t∙ = λ a γ → a C.[ γ ]t
       ; [∘]t∙ = C.[∘]t
       ; [id]t∙ = C.[id]t
       ; _▹∙_ = λ Γ A → Γ C.▹ A
       ; _,[_][_]∙_ = λ γ _ e a → γ C.,[ e ] a
       ; p∙ = C.p
       ; q∙ = C.q
       ; ▹β₁∙ = C.▹β₁
       ; ▹β₂∙ = C.▹β₂
       ; ▹η∙ = C.▹η
       }

  toDepModel : DepModel Ci toDepCwF Mi
  toDepModel = record
          { Π∙ = λ A B → M.Π A B
          ; Π[]∙ = M.Π[]
          ; lam∙ = λ A t → M.lam A t
          ; lam[]∙ = M.lam[]
          ; app∙ = λ t u → M.app t u
          ; app[]∙ = M.app[]
          ; Πβ∙ = M.Πβ
          ; Πη∙ = M.Πη
          ; 𝔹∙ = M.𝔹
          ; 𝕥∙ = M.𝕥
          ; 𝕗∙ = M.𝕗
          ; ifᵀ∙ = λ b A B → M.ifᵀ b A B
          ; ifᵀ[]∙ = M.ifᵀ[]
          ; ifᵀβ₁∙ = M.ifᵀβ₁
          ; ifᵀβ₂∙ = M.ifᵀβ₂
          ; ifᵗ∙ = λ P P𝕥 P𝕗 b → M.ifᵗ P P𝕥 P𝕗 b
          ; ifᵗ[]∙ = M.ifᵗ[]
          ; ifᵗβ₁∙ = M.ifᵗβ₁
          ; ifᵗβ₂∙ = M.ifᵗβ₂
          }

  private module toDepCwF = DepCwF toDepCwF
  private module toDepModel = DepModel toDepModel
  private module Ci = CwF Ci
  private module Mi = Model Mi
  open initElim

  iteCon : (Γ : Con) → C.Con
  iteCon = elimCon toDepCwF toDepModel
  iteSub : ∀{Δ Γ}(γ : Sub Δ Γ) → C.Sub (iteCon Δ) (iteCon Γ)
  iteSub = elimSub toDepCwF toDepModel
  iteTy  : ∀{Γ}(A : Ty Γ) → C.Ty (iteCon Γ)
  iteTy = elimTy toDepCwF toDepModel
  iteTm  : ∀{Γ A}(a : Tm Γ A) → C.Tm (iteCon Γ) (iteTy A)
  iteTm = elimTm toDepCwF toDepModel

  iteCwF : CwF→ Ci C
  iteCwF = record
            { Con→ = iteCon
            ; Sub→ = iteSub
            ; ∘→ = λ γ δ → ~refl
            ; id→ = ~refl
            ; ◇→ = ~refl
            ; ε→ = ~refl
            ; Ty→ = iteTy
            ; [→]T = λ A γ → ~refl
            ; Tm→ = iteTm
            ; [→]t = λ A a γ → ~refl
            ; ▹→ = ~refl
            ; ,→ = λ γ e a → ~refl
            ; p→ = λ A → ~refl
            ; q→ = λ A → ~refl
            }

  iteModel : Model→ iteCwF Mi M
  iteModel = record
              { Π→ = ~refl
              ; lam→ = ~refl
              ; app→ = λ t u → ~refl
              ; 𝔹→ = ~refl
              ; 𝕥→ = ~refl
              ; 𝕗→ = ~refl
              ; ifᵀ→ = λ b A B → ~refl
              ; ifᵗ→ = λ P P𝕥 P𝕗 b → ~refl
              }


-- The morphism given by the iterator is unique
module initUnique {i j k l : Level} (C : CwF {i}{j}{k}{l})(M : Model C)(C→ : CwF→ Ci C)(M→ : Model→ C→ Mi M) where
  open initIte C M
  private module C = CwF C
  private module C→ = CwF→ C→
  private module M = Model M
  private module M→ = Model→ M→

  unicityCwF : CwFPred Ci
  unicityCwF = record
                { Con∙ = λ Γ → C→.Con→ Γ ~ iteCon Γ
                ; Sub∙ = λ Δ∙ Γ∙ σ → C→.Sub→ σ ~ iteSub σ
                ; _∘∙_ =  λ {Γ Γ∙ Δ Δ∙ γ} γ∙ {Θ Θ∙ δ} δ∙ → C→.∘→ γ δ ◼ cong₅ (λ Γ Δ Θ (γ : C.Sub Δ Γ) (δ : C.Sub Θ Δ) → γ C.∘ δ) Γ∙ Δ∙ Θ∙ γ∙ δ∙
                ; id∙ = λ {Γ Γ∙} → C→.id→ ◼ cong (λ Γ → C.id {Γ}) Γ∙
                ; ◇∙ = C→.◇→
                ; ε∙ = λ {Γ Γ∙} → C→.ε→ ◼ cong (λ Γ → C.ε {Γ}) Γ∙
                ; Ty∙ = λ Γ∙ A → C→.Ty→ A ~ iteTy A
                ; _[_]T∙ = λ {Γ Γ∙ A} A∙ {Δ Δ∙ γ} γ∙ → C→.[→]T A γ ◼ cong₄ (λ Γ A Δ γ → C._[_]T {Γ} A {Δ} γ) Γ∙ A∙ Δ∙ γ∙
                ; Tm∙ = λ Γ∙ A∙ a → C→.Tm→ a ~ iteTm a
                ; _[_]t∙ = λ {Γ Γ∙ A A∙ a} a∙ {Δ Δ∙ γ} γ∙ → C→.[→]t A a γ ◼ cong₅ (λ Γ A a Δ γ → C._[_]t {Γ}{A} a {Δ} γ) Γ∙ A∙ a∙ Δ∙ γ∙
                ; _▹∙_ = λ {Γ} Γ∙ {A} A∙ → C→.▹→ ◼ cong₂ C._▹_ Γ∙ A∙
                ; _,[_]∙_ = λ {Γ Γ∙ Δ Δ∙ γ} γ∙ {A A∙ A' A'∙} e {a} a∙ → C→.,→ γ e a
                              ◼ CwF-tools.cong-subExt-EX C Γ∙ Δ∙ γ∙ A∙ A'∙ (C→.[→]T A γ ⁻¹ ◼ cong C→.Ty→ e) (cong iteTy e) a∙
                ; p∙ = λ {Γ Γ∙ A A∙} → C→.p→ A ◼ cong₂ (λ Γ A → C.p {Γ} {A}) Γ∙ A∙
                ; q∙ = λ {Γ Γ∙ A A∙} → C→.q→ A ◼ cong₂ (λ Γ A → C.q {Γ} {A}) Γ∙ A∙
                }

  unicityModel : ModelPred Ci unicityCwF Mi
  unicityModel = record
                  { Π∙ = λ {Γ Γ∙ A} A∙ {B} B∙ → M→.Π→ ◼ cong₃ (λ Γ A B → M.Π {Γ} A B) Γ∙ A∙ (coe≡-eq _ (C→.Ty→ B) ⁻¹ ◼ B∙)
                  ; lam∙ = λ {Γ Γ∙ A} A∙ {B B∙ t} t∙ → M→.lam→
                           ◼ cong₄ (λ Γ A B t → M.lam {Γ} A {B} t) Γ∙ A∙ (coe≡-eq _ (C→.Ty→ B) ⁻¹ ◼ B∙) (coe≡-eq _ (C→.Tm→ t) ⁻¹ ◼ t∙)
                  ; app∙ = λ {Γ Γ∙ A A∙ B B∙ t} t∙ {u} u∙ → M→.app→ t u
                           ◼ cong₅ (λ Γ A B t u → M.app {Γ} {A} {B} t u) Γ∙ A∙ (coe≡-eq _ (C→.Ty→ B) ⁻¹ ◼ B∙) (coe≡-eq _ (C→.Tm→ t) ⁻¹ ◼ t∙) u∙
                  ; 𝔹∙ = M→.𝔹→
                  ; 𝕥∙ = M→.𝕥→
                  ; 𝕗∙ = M→.𝕗→
                  ; ifᵀ∙ = λ {Γ Γ∙ b} b∙ {A} A∙ {B} B∙ → M→.ifᵀ→ b A B ◼ cong₄ (λ Γ → M.ifᵀ {Γ}) Γ∙ (coe≡-eq _ (C→.Tm→ b) ⁻¹ ◼ b∙) A∙ B∙
                  ; ifᵗ∙ = λ {Γ Γ∙ P} P∙ {P𝕥} P𝕥∙ {P𝕗} P𝕗∙ {b} b∙ → M→.ifᵗ→ P P𝕥 P𝕗 b
                           ◼ cong₅ (λ Γ → M.ifᵗ {Γ}) Γ∙ (coe≡-eq _ (C→.Ty→ P) ⁻¹ ◼ P∙) (coe≡-eq _ (C→.Tm→ P𝕥) ⁻¹ ◼ P𝕥∙)
                                   (coe≡-eq _ (C→.Tm→ P𝕗) ⁻¹ ◼ P𝕗∙) (coe≡-eq _ (C→.Tm→ b) ⁻¹ ◼ b∙)
                  }

  open initInd unicityCwF unicityModel

  unicityCon : (Γ : Con) → C→.Con→ Γ ~ iteCon Γ
  unicityCon Γ = indCon Γ

  unicitySub : {Γ Δ : Con} (γ : Sub Δ Γ) → C→.Sub→ γ ~ iteSub γ
  unicitySub γ = indSub γ

  unicityTy : {Γ : Con} (A : Ty Γ) → C→.Ty→ A ~ iteTy A
  unicityTy A = indTy A

  unicityTm : {Γ : Con} {A : Ty Γ} (a : Tm Γ A) → C→.Tm→ a ~ iteTm a
  unicityTm a = indTm a


-- A special case of the unicity of the iterator
module initUniqueEndo (C→ : CwF→ Ci Ci)(M→ : Model→ C→ Mi Mi) where
  private module C→ = CwF→ C→
  private module M→ = Model→ M→

  open Identity→ Ci Mi
  private module U₁ = initUnique Ci Mi C→ M→
  private module U₂ = initUnique Ci Mi idCwF idModel

  uniqueEndoCon : (Γ : Con) → C→.Con→ Γ ~ Γ
  uniqueEndoCon Γ = U₁.unicityCon Γ ◼ U₂.unicityCon Γ ⁻¹

  uniqueEndoSub : {Γ Δ : Con} (γ : Sub Δ Γ) → C→.Sub→ γ ~ γ
  uniqueEndoSub γ = U₁.unicitySub γ ◼ U₂.unicitySub γ ⁻¹

  uniqueEndoTy : {Γ : Con} (A : Ty Γ) → C→.Ty→ A ~ A
  uniqueEndoTy A = U₁.unicityTy A ◼ U₂.unicityTy A ⁻¹

  uniqueEndoTm : {Γ : Con} {A : Ty Γ} (a : Tm Γ A) → C→.Tm→ a ~ a
  uniqueEndoTm a = U₁.unicityTm a ◼ U₂.unicityTm a ⁻¹