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

open import lib
open import model

-- In this file, we strictify the underlying category of a CwF using the Yoneda embedding
-- i.e., we only replace substitutions with natural transformations

module strictifyCat (C : CwF {lzero}{lzero}{lzero}{lzero}) (M : Model C) where

module C = CwF C
module Ct = CwF-tools C
Con = C.Con
Ty  = C.Ty
Tm  = C.Tm
◇   = C.◇
_▹_ = C._▹_
infixl  _∘_
infixl  _▹_
infixl  _,[_]_

-- Sub Δ Γ := yΔ ̇→ yΓ
record Sub (Δ Γ : Con) : Set where
  inductive
  eta-equality
  constructor mkSub
  field
    γ   : ∀{Θ : Con} → C.Sub Θ Δ → C.Sub Θ Γ
    nat : ∀{Θ}{δ : C.Sub Θ Δ}{Ξ}{θ : C.Sub Ξ Θ} → γ δ C.∘ θ ~ γ (δ C.∘ θ)
open Sub renaming (γ to ∣_∣)

infix  ∣_∣≡
∣_∣≡ : ∀{Γ Δ}{σ₀ σ₁ : Sub Δ Γ} → (λ {Θ} → ∣ σ₀ ∣ {Θ}) ~ (λ {Θ} → ∣ σ₁ ∣ {Θ}) → σ₀ ~ σ₁
∣ e ∣≡ = ~congₚₛ (cong₃ (λ Γ Δ → mkSub {Γ} {Δ}) ~refl ~refl e)

_∘_ : ∀{Γ Δ} → Sub Δ Γ → ∀{Θ} → Sub Θ Δ → Sub Θ Γ
∣ γ ∘ δ ∣ θ = ∣ γ ∣ (∣ δ ∣ θ)
nat (γ ∘ δ) {Θ} {δ₁} {Ξ} {θ} = nat γ {_} {∣ δ ∣ δ₁} ◼ cong ∣ γ ∣ (nat δ)

ass : ∀{Γ Δ}{γ : Sub Δ Γ}{Θ}{δ : Sub Θ Δ}{Ξ}{θ : Sub Ξ Θ} → (γ ∘ δ) ∘ θ ~ γ ∘ (δ ∘ θ)
ass = ~refl

id : ∀{Γ} → Sub Γ Γ
∣ id ∣ γ = γ
nat id = ~refl

idl : ∀{Γ Δ}{γ : Sub Δ Γ} → id {Γ} ∘ γ ~ γ
idl = ~refl

idr : ∀{Γ Δ}{γ : Sub Δ Γ} → γ ∘ id ~ γ
idr = ~refl

ε : ∀{Γ} → Sub Γ ◇
∣ ε ∣ _ = C.ε
nat ε = C.◇η

◇η : ∀{Γ}{σ : Sub Γ ◇} → σ ~ (ε {Γ})
◇η {σ = σ} = ∣ funextᵢ (λ {Δ} {Δ'} eΔ → funext λ {σ₀} {σ₁} eσ → coe-eq (cong₂ C.Sub eΔ ~refl) (∣ σ ∣ σ₀) ◼ C.◇η) ∣≡

_[_]T : ∀{Γ} → Ty Γ → ∀{Δ} → Sub Δ Γ → Ty Δ
A [ γ ]T = A C.[ ∣ γ ∣ C.id ]T

[∘]T : ∀{Γ}{A : Ty Γ}{Δ}{γ : Sub Δ Γ}{Θ}{δ : Sub Θ Δ} → A [ γ ∘ δ ]T ~ A [ γ ]T [ δ ]T
[∘]T {A = A} {_} {γ = γ} {_} {δ} = cong (A C.[_]T) (cong ∣ γ ∣ (C.idl ⁻¹) ◼ (nat γ ⁻¹)) ◼ C.[∘]T

[id]T : ∀{Γ}{A : Ty Γ} → A [ id {Γ} ]T ~ A
[id]T = C.[id]T

_[_]t : ∀{Γ}{A : Ty Γ} → Tm Γ A → ∀{Δ}(γ : Sub Δ Γ) → Tm Δ (A [ γ ]T)
a [ γ ]t = a C.[ ∣ γ ∣ C.id ]t

[∘]t     : ∀{Γ}{A : Ty Γ}{a : Tm Γ A}{Δ}{γ : Sub Δ Γ}{Θ}{δ : Sub Θ Δ}
         → a [ γ ∘ δ ]t ~ a [ γ ]t [ δ ]t
[∘]t {a = a} {_} {γ} {_} {δ} = cong (λ x → a C.[ x ]t) ((γ .nat ◼ cong ∣ γ ∣ C.idl) ⁻¹) ◼ C.[∘]t

[id]t : ∀{Γ}{A : Ty Γ}{a : Tm Γ A} → a [ id ]t ~ a
[id]t = C.[id]t

_,[_]_   : ∀{Γ Δ}(γ : Sub Δ Γ) → ∀{A A'} → A [ γ ]T ~ A' → Tm Δ A' → Sub Δ (Γ ▹ A)
∣ _,[_]_ {Γ} {Δ} γ {A} {A'} e a ∣ δ =
  let e = cong (A C.[_]T) (cong ∣ γ ∣ (C.idl ⁻¹) ◼ nat γ ⁻¹) ◼ C.[∘]T ◼ cong C._[ δ ]T e in
  ∣ γ ∣ δ C.,[ e ] (a C.[ δ ]t)
nat (_,[_]_ {Γ} {Δ} γ {A} {A'} e a) {Θ} {δ = δ} {Ξ} {θ = θ} =
  let
    e₀ : ∀ {Θ} (δ : C.Sub Θ Δ) → A C.[ ∣ γ ∣ δ ]T ~ A' C.[ δ ]T
    e₀ {Θ} δ = cong (C._[_]T A) (cong (∣ γ ∣) (C.idl ⁻¹) ◼ ((γ .nat) ⁻¹)) ◼ C.[∘]T ◼ (cong (λ x → x C.[ δ ]T) e)
    e₁ : C.p C.∘ ((∣ γ ∣ δ C.,[ e₀ δ ] a C.[ δ ]t) C.∘ θ) ~ ∣ γ ∣ (δ C.∘ θ)
    e₁ = C.ass ⁻¹ ◼ cong (λ x → x C.∘ θ) Ct.▹β₁-EX ◼ γ .nat
  in (C.▹η {Γ} {Ξ} {A} {(∣ γ ∣ δ C.,[ _ ] a C.[ δ ]t) C.∘ θ}) ⁻¹
     ◼ congᵣᵣᵣᵢᵣ (λ a b c d e → C._,[_]_ {Γ = Γ} {Δ = Ξ} a {b} {c} d e)
                 e₁ ~refl (C.[∘]T ⁻¹ ◼ cong (C._[_]T A) e₁ ◼ (e₀ (δ C.∘ θ)))
                 (C.[∘]t ◼ cong₂ (λ a b → C._[_]t {Θ} {a} b {Ξ} θ) ((C.[∘]T ⁻¹)
                 ◼ cong (C._[_]T A) Ct.▹β₁-EX ◼ (e₀ δ)) Ct.▹β₂-EX ◼ (C.[∘]t ⁻¹))

p : ∀{Γ A} → Sub (Γ ▹ A) Γ
∣ p ∣ γa = C.p C.∘ γa
nat p = C.ass

q : ∀{Γ A} → Tm (Γ ▹ A) (A [ p ]T)
q {Γ} {A} = coe (cong (λ x → C.Tm (Γ C.▹ A) (A C.[ x ]T)) (C.idr ⁻¹)) C.q

▹β₁ : ∀{Γ Δ}{γ : Sub Δ Γ}{A}{a : Tm Δ (A [ γ ]T)} → p ∘ (γ ,[ ~refl ] a) ~ γ
▹β₁ {Γ} {Δ} {γ} {A} {a} = ∣ funextᵢ (λ {Θ} {Θ'} eΘ → funext λ {δ} {δ'} eδ → Ct.▹β₁-EX ◼ cong₂ (λ a → ∣ γ ∣ {a}) eΘ eδ) ∣≡

▹β₂ : ∀{Γ Δ}{γ : Sub Δ Γ}{A}{a : Tm Δ (A [ γ ]T)} → q [ γ ,[ ~refl ] a ]t ~ a
▹β₂ {Γ} {Δ} {γ} {A} {a} =
  cong₂ (λ x y → C._[_]t {Γ ▹ A} {x} y {Δ} (∣ γ ∣ C.id C.,[ cong (λ x → A C.[ x ]T) (C.idr ⁻¹) ◼ C.[∘]T ] a C.[ C.id ]t))
    (cong (λ x → A C.[ x ]T) C.idr)
    ((coe-eq (cong (λ x → C.Tm (Γ C.▹ A) (A C.[ x ]T)) (C.idr ⁻¹)) C.q) ⁻¹)
  ◼ Ct.▹β₂-EX ◼ C.[id]t

▹η : ∀ {Γ Δ A} {γa : Sub Δ (Γ ▹ A)} → ((p ∘ γa) ,[ [∘]T {γ = p} {δ = γa} ] (q [ γa ]t)) ~ γa
▹η {Γ} {Δ} {A} {γa} =
  ∣ funextᵢ (λ {Θ} {Θ'} eΘ → funext λ {δ} {δ'} eδ →
      congᵣᵣᵣᵢᵣ (λ a b c d e → C._,[_]_ {Γ = Γ} {a} b {A} {c} d e)
        eΘ (cong₂ (λ x y → C.p C.∘ ∣ γa ∣ {x} y) eΘ eδ)
        ((C.[∘]T ⁻¹) ◼ cong₃ (λ x y z → C._[_]T x {y} z) (cong (λ x → A C.[ x ]T) C.idr) eΘ
          (γa .nat ◼ cong₂ (λ x → ∣ γa ∣ {x}) eΘ (C.idl ◼ eδ)))
        (C.[∘]t ⁻¹ ◼ cong₄ (λ x y z → C._[_]t {Γ ▹ A} {x} y {z}) (cong (λ x → A C.[ x ]T) C.idr) (((coe≡-eq _ C.q) ⁻¹))
          eΘ (γa .nat ◼ cong₂ (λ x → ∣ γa ∣ {x}) eΘ (C.idl ◼ eδ)))
      ◼ C.▹η)
  ∣≡

-- strictified CwF
Cₛ : CwF {lzero}{lzero}{lzero}{lzero}
Cₛ = record
      { Con = Con
      ; Sub = Sub
      ; _∘_ = _∘_
      ; ass = ~refl
      ; id = id
      ; idl = ~refl
      ; idr = ~refl
      ; ◇ = ◇
      ; ε = ε
      ; ◇η = ◇η
      ; Ty = Ty
      ; _[_]T = _[_]T
      ; [∘]T = λ {x1}{x2}{x3}{x4}{x5}{x6} → [∘]T {x1}{x2}{x3}{x4}{x5}{x6}
      ; [id]T = [id]T
      ; Tm = Tm
      ; _[_]t = _[_]t
      ; [∘]t = λ {x1}{x2}{x3}{x4}{x5}{x6}{x7} → [∘]t {x1}{x2}{x3}{x4}{x5}{x6}{x7}
      ; [id]t = [id]t
      ; _▹_ = _▹_
      ; _,[_]_ = _,[_]_
      ; p = p
      ; q = q
      ; ▹β₁ = ▹β₁
      ; ▹β₂ = λ {x1}{x2}{x3}{x4} → ▹β₂ {x1}{x2}{x3}{x4}
      ; ▹η = ▹η
      }

-- map from C to Cₛ
toSub : {Δ Γ : Con} → C.Sub Δ Γ → Sub Δ Γ
toSub f = mkSub (λ g → f C.∘ g) C.ass

toSub∘ : {Γ Δ Θ : Con} {f : C.Sub Δ Γ} {g : C.Sub Θ Δ} → toSub (f C.∘ g) ~ (toSub f) ∘ (toSub g)
toSub∘ = ∣ funextHᵢᵣ (λ h → C.ass) ∣≡

toSub-id : {Γ : Con} → toSub (C.id {Γ = Γ}) ~ id {Γ = Γ}
toSub-id = ∣ funextHᵢᵣ (λ h → C.idl) ∣≡

open CwF-tools Cₛ

-- useful lemmas on CwF-tools
subst-p : ∀{Γ} → {A : Ty Γ} (B : Ty Γ)
        → B [ p {A = A} ]T ~ B C.[ C.p {A = A} ]T
subst-p B = cong (C._[_]T B) C.idr

∣↑∣ : ∀ {Γ}{A : Ty Γ}{Δ}(γ : Sub Δ Γ) → ∣ ↑ {A = A} γ ∣ C.id ~ Ct.↑ {A = A} (∣ γ ∣ C.id)
∣↑∣ {Γ}{A}{Δ} γ =
  congᵣᵣᵣᵢᵣ (λ a b c d e → C._,[_]_ {Γ = Γ} {a} b {A} {c} d e) ~refl
            (cong ∣ γ ∣ C.idr ◼ (cong ∣ γ ∣ (C.idl ⁻¹) ◼ γ .nat ⁻¹))
            (C.[id]T ◼ subst-p (A [ γ ]T)) (C.[id]t ◼ coe≡-eq _ C.q ⁻¹)

subst↑T : ∀ {Γ}{A : Ty Γ}{Δ}(γ : Sub Δ Γ)(B : Ty (Γ ▹ A))
        → B [ ↑ γ ]T ~ B C.[ Ct.↑ (∣ γ ∣ C.id) ]T
subst↑T {Γ}{A}{Δ} γ B = cong (C._[_]T B) (∣↑∣ γ)

subst↑t : ∀ {Γ}{A : Ty Γ}{Δ}(γ : Sub Δ Γ){B : Ty (Γ ▹ A)}(t : Tm (Γ ▹ A) B)
        → t [ ↑ γ ]t ~ t C.[ Ct.↑ (∣ γ ∣ C.id) ]t
subst↑t {Γ}{A}{Δ} γ {B} t = cong (C._[_]t t) (∣↑∣ γ)

∣↑ε∣ : ∀ {Γ}{A : Ty ◇}{Δ}(γ : Sub Δ Γ) → ∣ ↑ε {A = A} γ ∣ C.id ~ Ct.↑ε {A = A} (∣ γ ∣ C.id)
∣↑ε∣ {Γ}{A}{Δ} γ =
  congᵣᵣᵣᵢᵣ (λ a b c d e → C._,[_]_ {Γ = Γ} {a} b {A [ ε ]T} {c} d e) ~refl
            (cong ∣ γ ∣ C.idr ◼ (cong ∣ γ ∣ (C.idl ⁻¹) ◼ γ .nat ⁻¹))
            (C.[id]T ◼ subst-p (A C.[ C.ε ]T)) (C.[id]t ◼ coe≡-eq _ C.q ⁻¹)

subst↑εT : ∀ {Γ}{A : Ty ◇}{Δ}(γ : Sub Δ Γ)(B : Ty (Γ ▹ A [ ε ]T))
        → B [ ↑ε γ ]T ~ B C.[ Ct.↑ε (∣ γ ∣ C.id) ]T
subst↑εT {Γ}{A}{Δ} γ B = cong (C._[_]T B) (∣↑ε∣ γ)

∣sg∣ : ∀ {Γ}{A : Ty Γ}(a : Tm Γ A) → ∣ sg a ∣ C.id ~ Ct.sg a
∣sg∣ {Γ}{A} a = congᵣᵣᵣᵢᵣ (λ a b c d e → C._,[_]_ {Γ = Γ} {a} b {A} {c} d e) ~refl ~refl C.[id]T C.[id]t

subst-sg-T : ∀ {Γ}{A : Ty Γ}(a : Tm Γ A)(B : Ty (Γ ▹ A))
           → B [ sg a ]T ~ B C.[ Ct.sg a ]T
subst-sg-T {Γ}{A} a B = cong (C._[_]T B) (∣sg∣ a)

subst-sg-t : ∀ {Γ}{A : Ty Γ}(a : Tm Γ A){B : Ty (Γ ▹ A)}(t : Tm (Γ ▹ A) B)
           → t [ sg a ]t ~ t C.[ Ct.sg a ]t
subst-sg-t {Γ}{A} a {B} t = cong (C._[_]t t) (∣sg∣ a)

subst-↑p : ∀{Γ}{A : Ty Γ}{B : Ty Γ}(B' : Ty (Γ ▹ B))
         → B' [ ↑ (p {A = A}) ]T ~ B' C.[ Ct.↑ (C.p {A = A}) ]T
subst-↑p B' = subst↑T p B' ◼ cong (λ f → B' C.[ Ct.↑ f ]T) C.idr

subst-sgq : ∀{Γ}{A : Ty Γ}{B₁ : Ty (Γ ▹ A ▹ (A [ p ]T))}{B₂ : Ty (Γ ▹ A ▹ (A C.[ C.p ]T))}(eB : B₁ ~ B₂)
          → B₁ [ sg q ]T ~ B₂ C.[ Ct.sg C.q ]T
subst-sgq {Γ}{A}{B₁}{B₂} eB =
  cong₄ (λ Γ A Δ → C._[_]T {Γ} A {Δ}) (cong (C._▹_ (Γ ▹ A)) (subst-p A)) eB ~refl
        (∣sg∣ q ◼ cong₂ (λ A → Ct.sg {A = A}) (subst-p A) (coe≡-eq _ C.q ⁻¹))

-- Now we add dependent products and booleans to the strictified CwF
module M = Model M

Π : ∀{Γ}(A : Ty Γ) → Ty (Γ ▹ A) → Ty Γ
Π = M.Π

Π[] : ∀{Γ}{A : Ty Γ}{B : Ty (Γ ▹ A)}{Δ}{γ : Sub Δ Γ}
    → (Π A B) [ γ ]T ~ Π (A [ γ ]T) (B [ ↑ γ ]T)
Π[] {Γ} {A} {B} {Δ} {γ} =
  M.Π[] ◼ cong₂ M.Π ~refl ((subst↑T γ B) ⁻¹)

lam : ∀{Γ}(A : Ty Γ){B : Ty (Γ ▹ A)}(t : Tm (Γ ▹ A) B) → Tm Γ (Π A B)
lam = M.lam

lam[] : ∀{Γ}{A : Ty Γ}{B : Ty (Γ ▹ A)}{t : Tm (Γ ▹ A) B}{Δ}{γ : Sub Δ Γ}
      → (lam A t) [ γ ]t ~ lam (A [ γ ]T) (t [ ↑ γ ]t)
lam[] {Γ}{A}{B}{t}{Δ}{γ} =
  M.lam[] ◼ cong₂ (λ x → M.lam (A [ γ ]T) {x}) ((subst↑T γ B) ⁻¹) ((subst↑t γ t) ⁻¹)

app : ∀{Γ}{A : Ty Γ}{B : Ty (Γ ▹ A)}(t : Tm Γ (Π A B))(u : Tm Γ A) → Tm Γ (B [ sg u ]T)
app {Γ} {A} {B} t u = coe (cong (C.Tm Γ) ((subst-sg-T u B) ⁻¹)) (M.app t u)

app[] : ∀{Γ}{A : Ty Γ}{B : Ty (Γ ▹ A)}{t : Tm Γ (Π A B)}{u : Tm Γ A}{Δ}{γ : Sub Δ Γ}
      → (app t u) [ γ ]t ~ app (coe (cong (Tm Δ) (Π[] {γ = γ})) (t [ γ ]t)) (u [ γ ]t)
app[] {Γ}{A}{B}{t}{u}{Δ}{γ} =
  Ct.coe[]t ((subst-sg-T u B) ⁻¹) (M.app t u) (∣ γ ∣ C.id)
  ◼ (coe≡-eq _ (M.app t u C.[ ∣ γ ∣ C.id ]t)) ⁻¹
  ◼ M.app[]
  ◼ cong₃ (λ B → M.app {B = B}) ((subst↑T γ B) ⁻¹) (coe≡-eq₂ (t C.[ ∣ γ ∣ C.id ]t)) ~refl
  ◼ coe≡-eq _ (M.app (coe (cong (Tm Δ) (Π[] {γ = γ})) (t [ γ ]t)) (u [ γ ]t))

Πβ : ∀{Γ}{A : Ty Γ}{B : Ty (Γ ▹ A)}{t : Tm (Γ ▹ A) B}{a : Tm Γ A}
   → app (lam A t) a ~ t [ sg a ]t
Πβ {Γ}{A}{B}{t}{a} =
  (coe≡-eq _ (M.app (M.lam A t) a)) ⁻¹
  ◼ M.Πβ
  ◼ (subst-sg-t a t) ⁻¹

Πη : ∀{Γ}{A : Ty Γ}{B : Ty (Γ ▹ A)}{t : Tm Γ (Π A B)}
   → t ~ lam A (app (coe (cong (Tm (Γ ▹ A)) (Π[] {γ = p})) (t [ p ]t)) q)
Πη {Γ}{A}{B}{t} = M.Πη ◼ cong₂ (λ B → M.lam A {B}) eB et
  where
    eB : B C.[ Ct.↑ C.p ]T C.[ Ct.sg C.q ]T ~ B [ ↑ p ]T [ sg q ]T
    eB = subst-sgq (subst-↑p B) ⁻¹
    et : M.app (coe (cong (C.Tm (Γ ▹ A)) (M.Π[] {γ = C.p})) (t C.[ C.p ]t)) C.q
         ~ app (coe (cong (Tm (Γ ▹ A)) (Π[] {γ = p})) (t [ p ]t)) q
    et = cong₄ (λ A B → M.app {_}{A}{B}) (subst-p A ⁻¹) (subst-↑p B ⁻¹)
               (coe≡-eq _ (t C.[ C.p {A = A} ]t) ⁻¹ ◼ cong (C._[_]t t) (C.idr ⁻¹) ◼ coe≡-eq _ (t [ p {A = A} ]t)) (coe≡-eq _ C.q)
         ◼ (coe≡-eq _ (M.app (coe (cong (Tm (Γ ▹ A)) (Π[] {γ = p})) (t [ p ]t)) q))

𝔹 : Ty ◇
𝔹 = M.𝔹

𝕥 : Tm ◇ 𝔹
𝕥 = M.𝕥

𝕗 : Tm ◇ 𝔹
𝕗 = M.𝕗

ifᵀ : ∀{Γ} → Tm Γ (𝔹 [ ε ]T) → Ty Γ → Ty Γ → Ty Γ
ifᵀ = M.ifᵀ

ifᵀ[] : ∀{Γ}{b : Tm Γ (𝔹 [ ε ]T)}{A B : Ty Γ}{Δ}{γ : Sub Δ Γ}
      → (ifᵀ b A B) [ γ ]T ~ ifᵀ (coe (cong (Tm Δ) (ε[]T {γ = γ})) (b [ γ ]t)) (A [ γ ]T) (B [ γ ]T)
ifᵀ[] = M.ifᵀ[]

ifᵀβ₁ : ∀{Γ}{A B : Ty Γ} → ifᵀ (𝕥 [ ε ]t) A B ~ A
ifᵀβ₁ = M.ifᵀβ₁

ifᵀβ₂ : ∀{Γ}{A B : Ty Γ} → ifᵀ (𝕗 [ ε ]t) A B ~ B
ifᵀβ₂ = M.ifᵀβ₂

ifᵗ : ∀{Γ} (P : Ty (Γ ▹ 𝔹 [ ε ]T)) (P𝕥 : Tm Γ (P [ sg (𝕥 [ ε ]t) ]T)) (P𝕗 : Tm Γ (P [ sg (𝕗 [ ε ]t) ]T)) (b : Tm Γ (𝔹 [ ε ]T))
    → Tm Γ (P [ sg b ]T)
ifᵗ {Γ} P P𝕥 P𝕗 b = coe (cong (C.Tm Γ) ((subst-sg-T b P) ⁻¹))
                        (M.ifᵗ P (coe (cong (C.Tm Γ) (subst-sg-T (𝕥 [ ε ]t) P)) P𝕥)
                                 (coe (cong (C.Tm Γ) (subst-sg-T (𝕗 [ ε ]t) P)) P𝕗) b)

ifᵗ[] : ∀{Γ}{P : Ty (Γ ▹ 𝔹 [ ε ]T)}{P𝕥 : Tm Γ (P [ sg (𝕥 [ ε ]t) ]T)}{P𝕗 : Tm Γ (P [ sg (𝕗 [ ε ]t) ]T)}{b : Tm Γ (𝔹 [ ε ]T)}{Δ}{γ : Sub Δ Γ}
      → (ifᵗ P P𝕥 P𝕗 b) [ γ ]t ~ ifᵗ (P [ ↑ε γ ]T) (coe (cong (Tm Δ) (Ty-↑ε-sg 𝕥 P γ)) (P𝕥 [ γ ]t))
                                     (coe (cong (Tm Δ) (Ty-↑ε-sg 𝕗 P γ)) (P𝕗 [ γ ]t)) (coe (cong (Tm Δ) (ε[]T {γ = γ})) (b [ γ ]t))
ifᵗ[] {Γ}{P}{P𝕥}{P𝕗}{b}{Δ}{γ} =
  Ct.coe[]t ((subst-sg-T b P) ⁻¹) (M.ifᵗ P (coe≡ _ P𝕥) (coe≡ _ P𝕗) b) (∣ γ ∣ C.id)
  ◼ coe≡-eq _ (M.ifᵗ P (coe≡ _ P𝕥) (coe≡ _ P𝕗) b C.[ ∣ γ ∣ C.id ]t) ⁻¹
  ◼ M.ifᵗ[]
  ◼ cong₄ M.ifᵗ (subst↑εT γ P ⁻¹)
                (coe≡-eq _ (coe≡ _ P𝕥 C.[ ∣ γ ∣ C.id ]t) ⁻¹
                  ◼ cong₂ (λ A a → C._[_]t {A = A} a (∣ γ ∣ C.id)) (subst-sg-T (𝕥 [ ε ]t) P ⁻¹) (coe≡-eq _ P𝕥 ⁻¹)
                  ◼ coe≡-eq _ (P𝕥 [ γ ]t) ◼ coe≡-eq _ (coe (cong (Tm Δ) (Ty-↑ε-sg 𝕥 P γ)) (P𝕥 [ γ ]t)))
                (coe≡-eq _ (coe≡ _ P𝕗 C.[ ∣ γ ∣ C.id ]t) ⁻¹
                  ◼ cong₂ (λ A a → C._[_]t {A = A} a (∣ γ ∣ C.id)) (subst-sg-T (𝕗 [ ε ]t) P ⁻¹) (coe≡-eq _ P𝕗 ⁻¹)
                  ◼ coe≡-eq _ (P𝕗 [ γ ]t) ◼ coe≡-eq _ (coe (cong (Tm Δ) (Ty-↑ε-sg 𝕗 P γ)) (P𝕗 [ γ ]t)))
                ~refl
  ◼ coe≡-eq _ (M.ifᵗ (P [ ↑ε γ ]T)
                     (coe≡ _ (coe (cong (Tm Δ) (Ty-↑ε-sg 𝕥 P γ)) (P𝕥 [ γ ]t)))
                     (coe≡ _ (coe (cong (Tm Δ) (Ty-↑ε-sg 𝕗 P γ)) (P𝕗 [ γ ]t)))
                     (coe≡ _ (b [ γ ]t)))

ifᵗβ₁ : ∀{Γ} {P : Ty (Γ ▹ 𝔹 [ ε ]T)} {P𝕥 : Tm Γ (P [ sg (𝕥 [ ε ]t) ]T)} {P𝕗 : Tm Γ (P [ sg (𝕗 [ ε ]t) ]T)}
      → ifᵗ P P𝕥 P𝕗 (𝕥 [ ε ]t) ~ P𝕥
ifᵗβ₁ {Γ} {P} {P𝕥} {P𝕗} =
  coe≡-eq _ (M.ifᵗ P (coe≡ _ P𝕥) (coe≡ _ P𝕗) (M.𝕥 C.[ C.ε ]t)) ⁻¹
  ◼ M.ifᵗβ₁
  ◼ coe≡-eq _ P𝕥 ⁻¹

ifᵗβ₂ : ∀{Γ} {P : Ty (Γ ▹ 𝔹 [ ε ]T)} {P𝕥 : Tm Γ (P [ sg (𝕥 [ ε ]t) ]T)} {P𝕗 : Tm Γ (P [ sg (𝕗 [ ε ]t) ]T)}
      → ifᵗ P P𝕥 P𝕗 (𝕗 [ ε ]t) ~ P𝕗
ifᵗβ₂ {Γ} {P} {P𝕥} {P𝕗} =
  coe≡-eq _ (M.ifᵗ P (coe≡ _ P𝕥) (coe≡ _ P𝕗) (M.𝕗 C.[ C.ε ]t)) ⁻¹
  ◼ M.ifᵗβ₂
  ◼ coe≡-eq _ P𝕗 ⁻¹

Mₛ : Model Cₛ
Mₛ = record
      { Π = Π
      ; Π[] = λ {Γ} {A} {B} {Δ} {γ} → Π[] {Γ} {A} {B} {Δ} {γ}
      ; lam = lam
      ; lam[] = λ {Γ}{A}{B}{t}{Δ}{γ} → lam[] {Γ}{A}{B}{t}{Δ}{γ}
      ; app = app
      ; app[] = λ {Γ}{A}{B}{t}{u}{Δ}{γ} → app[] {Γ}{A}{B}{t}{u}{Δ}{γ}
      ; Πβ = Πβ
      ; Πη = Πη
      ; 𝔹 = 𝔹
      ; 𝕥 = 𝕥
      ; 𝕗 = 𝕗
      ; ifᵀ = ifᵀ
      ; ifᵀ[] = λ {Γ}{b}{A}{B}{Δ}{γ} → ifᵀ[] {Γ}{b}{A}{B}{Δ}{γ}
      ; ifᵀβ₁ = ifᵀβ₁
      ; ifᵀβ₂ = ifᵀβ₂
      ; ifᵗ = ifᵗ
      ; ifᵗ[] = λ {Γ}{P}{P𝕥}{P𝕗}{b}{Δ}{γ} → ifᵗ[] {Γ}{P}{P𝕥}{P𝕗}{b}{Δ}{γ}
      ; ifᵗβ₁ = ifᵗβ₁
      ; ifᵗβ₂ = ifᵗβ₂
      }