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

module strictifyPMPMorphism where

open import lib
open import model
open import morphism
import strictifyCat
open import strictifyPMP

-- Morphism from the strictified CwF to the original one

module strictifyPMP→ (C : CwF {lzero}{lzero}{lzero}{lzero}) (M : Model C) where
  open str C M

  private module Cₛ = CwF (strictifyCat.Cₛ C M)
  private module Ctₛ = CwF-tools (strictifyCat.Cₛ C M)
  private module Mₛ = Model (strictifyCat.Mₛ C M)
  private module Cₛₛ = CwF Cₛₛ
  private module Mₛₛ = Model Mₛₛ

  mutual
    Con→ : Cₛₛ.Con → Cₛ.Con
    Con→ ◇ₜ = Cₛ.◇
    Con→ (Γ ▹ₜ A) = (Con→ Γ) Cₛ.▹ (∣ A ∣ (φinv Γ Cₛ.id))

    -- (Con→ Γ) represents (El Γ)
    φfun : (Γ : Cₛₛ.Con) {Δ : Cₛ.Con} → Yᶜ (El Γ) Δ → Cₛ.Sub Δ (Con→ Γ)
    φfun ◇ₜ γ = Cₛ.ε
    φfun (Γ ▹ₜ A) γ =
      let
        e₀ : φinv Γ Cₛ.id |ᶜ φfun Γ (Yˢ Ĉ.p γ) ~ Yˢ Ĉ.p γ
        e₀ = (φinv→ Γ Cₛ.id (φfun Γ (Yˢ Ĉ.p γ)) ⁻¹ ◼ φret Γ (Yˢ Ĉ.p γ))

        e₁ : ∣ A ∣ (φinv Γ Cₛ.id) Cₛ.[ φfun Γ (Yˢ Ĉ.p γ) ]T ~ ∣ A ∣ (Yˢ Ĉ.p γ)
        e₁ = A .rel (φinv Γ Cₛ.id) (φfun Γ (Yˢ Ĉ.p γ)) ◼ cong ∣ A ∣ e₀
      in φfun Γ (Yˢ Ĉ.p γ) Cₛ.,[ e₁ ] ∣ Ĉ.Yᵗ Ĉ.q γ ∣ Cₛ.id

    φfun→ : (Γ : Cₛₛ.Con) {Δ Θ : Cₛ.Con} (γ : Yᶜ (El Γ) Δ) (δ : Cₛ.Sub Θ Δ) → φfun Γ (γ |ᶜ δ) ~ (φfun Γ γ) Cₛ.∘ δ
    φfun→ ◇ₜ {Δ} {Θ} γ δ = Cₛ.◇η ⁻¹
    φfun→ (Γ ▹ₜ A) {Δ} {Θ} γ δ =
      let
        e₀ : ∀ {Θ} (γ : Yᶜ (El Γ) Θ) → φinv Γ Cₛ.id |ᶜ φfun Γ γ ~ γ
        e₀ γ = (φinv→ Γ Cₛ.id (φfun Γ γ) ⁻¹ ◼ φret Γ γ)

        e₁ : ∀ {Θ} (γ : Yᶜ (El Γ) Θ) → ∣ A ∣ (φinv Γ Cₛ.id) Cₛ.[ φfun Γ γ ]T ~ ∣ A ∣ γ
        e₁ γ = A .rel (φinv Γ Cₛ.id) (φfun Γ γ) ◼ cong ∣ A ∣ (e₀ γ)

        e₂ : ∣ A ∣ (φinv Γ Cₛ.id) Cₛ.[ φfun Γ (Yˢ Ĉ.p γ) Cₛ.∘ δ ]T ~ ∣ A ∣ (Yˢ Ĉ.p γ) Cₛ.[ δ ]T
        e₂ = cong (λ f → ∣ A ∣ (φinv Γ Cₛ.id) Cₛ.[ f ]T) (φfun→ Γ (Yˢ Ĉ.p γ) δ ⁻¹) ◼ e₁ (Yˢ Ĉ.p γ |ᶜ δ) ◼ A .rel (Yˢ Ĉ.p γ) δ ⁻¹
      in CwF-tools.cong-subExt Cₛ (φfun→ Γ (Yˢ Ĉ.p γ) δ) (A .rel (Yˢ Ĉ.p γ) δ ⁻¹) (e₁ (Yˢ Ĉ.p γ |ᶜ δ)) e₂ (γ .rel Cₛ.id .Ĉ.ty δ ⁻¹)
         ◼ CwF-tools.subExt∘ Cₛ (φfun Γ (Yˢ Ĉ.p γ)) (e₁ (Yˢ Ĉ.p γ)) (∣ Ĉ.Yᵗ Ĉ.q γ ∣ Cₛ.id) δ ⁻¹

    φinv : (Γ : Cₛₛ.Con) {Δ : Cₛ.Con} → Cₛ.Sub Δ (Con→ Γ) → Yᶜ (El Γ) Δ
    φinv ◇ₜ γ = mkY (λ _ → tt) (λ _ → ttₚ)
    φinv (Γ ▹ₜ A) {Δ} γ = C↑ A (φinv Γ Cₛ.id) |ᶜ γ

    φinv→ : (Γ : Cₛₛ.Con) {Δ Θ : Cₛ.Con} (γ : Cₛ.Sub Δ (Con→ Γ)) (δ : Cₛ.Sub Θ Δ) → φinv Γ (γ Cₛ.∘ δ) ~ (φinv Γ γ) |ᶜ δ
    φinv→ ◇ₜ γ δ = ~refl
    φinv→ (Γ ▹ₜ A) {Δ} {Θ} γ δ = ~refl

    φsec : (Γ : Cₛₛ.Con) {Δ : Cₛ.Con} (γ : Cₛ.Sub Δ (Con→ Γ)) → φfun Γ {Δ} (φinv Γ {Δ} γ) ~ γ
    φsec ◇ₜ γ = Cₛ.◇η ⁻¹
    φsec (Γ ▹ₜ A) {Δ} γ =
      let
        e₀ : ∀ {Θ} (γ : Yᶜ (El Γ) Θ) → φinv Γ Cₛ.id |ᶜ φfun Γ γ ~ γ
        e₀ γ = (φinv→ Γ Cₛ.id (φfun Γ γ) ⁻¹ ◼ φret Γ γ)

        e₁ : ∀ {Θ} (γ : Yᶜ (El Γ) Θ) → ∣ A ∣ (φinv Γ Cₛ.id) Cₛ.[ φfun Γ γ ]T ~ ∣ A ∣ γ
        e₁ γ = A .rel (φinv Γ Cₛ.id) (φfun Γ γ) ◼ cong ∣ A ∣ (e₀ γ)

        e₂ : φfun Γ (Yˢ Ĉ.p (C↑ A (φinv Γ Cₛ.id) |ᶜ γ)) ~ Cₛ.p Cₛ.∘ γ
        e₂ = φfun→ Γ (φinv Γ Cₛ.id) (Cₛ.p Cₛ.∘ γ) ◼ cong (λ x → x Cₛ.∘ (Cₛ.p Cₛ.∘ γ)) (φsec Γ Cₛ.id)

        e₃ : ∣ C↑ A (φinv Γ Cₛ.id) ∣ γ .Ĉ.ty ~ Cₛ.q Cₛ.[ γ ]t
        e₃ = coe≡-eq _ (Cₛ.q Cₛ.[ γ ]t) ⁻¹
      in Ctₛ.cong-subExt e₂ (A .rel (φinv Γ Cₛ.id) (Cₛ.p Cₛ.∘ γ) ⁻¹ ◼ Cₛ.[∘]T {γ = Cₛ.p} {δ = γ})
                        (e₁ (Yˢ Ĉ.p (C↑ A (φinv Γ Cₛ.id) |ᶜ γ))) (Cₛ.[∘]T {γ = Cₛ.p} {δ = γ}) e₃
         ◼ Cₛ.▹η {γa = γ}

    φret : (Γ : Cₛₛ.Con) {Δ : Cₛ.Con} (γ : Yᶜ (El Γ) Δ) → φinv Γ {Δ} (φfun Γ {Δ} γ) ~ γ
    φret ◇ₜ γ = ~refl
    φret (Γ ▹ₜ A) {Δ} γ =
      let
        e₀ : ∀ {Θ} (γ : Yᶜ (El Γ) Θ) → φinv Γ Cₛ.id |ᶜ φfun Γ γ ~ γ
        e₀ γ = (φinv→ Γ Cₛ.id (φfun Γ γ) ⁻¹ ◼ φret Γ γ)

        e₁ : ∀ {Θ} (γ : Yᶜ (El Γ) Θ) → ∣ A ∣ (φinv Γ Cₛ.id) Cₛ.[ φfun Γ γ ]T ~ ∣ A ∣ γ
        e₁ γ = A .rel (φinv Γ Cₛ.id) (φfun Γ γ) ◼ cong ∣ A ∣ (e₀ γ)

        f : Cₛ.Sub Δ (Con→ (Γ ▹ₜ A))
        f = φfun Γ (Yˢ Ĉ.p γ) Cₛ.,[ e₁ (Yˢ Ĉ.p γ) ] ∣ Ĉ.Yᵗ Ĉ.q γ ∣ Cₛ.id

        e₂ : Cp A (φinv Γ Cₛ.id) |ᶜ f ~ Yˢ Ĉ.p γ
        e₂ = cong (λ f → (φinv Γ Cₛ.id) |ᶜ f) {Cₛ.p Cₛ.∘ f} {φfun Γ (Yˢ Ĉ.p γ)} (Ctₛ.▹β₁-EX {e = e₁ (Yˢ Ĉ.p γ)})
             ◼ (φinv→ Γ Cₛ.id (φfun Γ (Yˢ Ĉ.p γ)) ⁻¹) ◼ φret Γ (Yˢ Ĉ.p γ)

        e₃ : Cₛ.q Cₛ.[ f ]t ~ ∣ Ĉ.Yᵗ Ĉ.q γ ∣ Cₛ.id
        e₃ = Ctₛ.▹β₂-EX {γ = φfun Γ (Yˢ Ĉ.p γ)} {e = e₁ (Yˢ Ĉ.p γ)}

        e₄ : ∀ {Θ} (δ : Hom Θ Δ) →  Cₛ.q Cₛ.[ f ]t Cₛ.[ δ ]t ~ ∣ Ĉ.Yᵗ Ĉ.q γ ∣ δ
        e₄ δ = cong₂ (λ X (x : Cₛ.Tm Δ X) → x Cₛ.[ δ ]t)
                     (Cₛ.[∘]T {γ = Cₛ.p}{δ = f} ⁻¹ ◼ A .rel (φinv Γ Cₛ.id) (Cₛ.p Cₛ.∘ f) ◼ cong ∣ A ∣ e₂)
                     e₃
               ◼ (Ĉ.Yᵗ Ĉ.q γ .rel Cₛ.id δ)

        e₅ : Ĉ.⟨ CTm Ĉ.[ A ]T , Cp A (φinv Γ Cₛ.id) ⟩ (Cq A (φinv Γ Cₛ.id)) |ᵀ f ~ Ĉ.Yᵗ (Ĉ.q {A = CTm Ĉ.[ A ]T}) γ
        e₅ = Ĉ.Yᵀ≡ (CTm Ĉ.[ A ]T) {Δ}{Δ} ~refl {Cp A (φinv Γ Cₛ.id) |ᶜ f}{Yˢ Ĉ.p γ} e₂
                   (funexthᵢᵣ λ {Θ} δ → coe≡-eq _ (Cₛ.q Cₛ.[ f Cₛ.∘ δ ]t) ⁻¹ ◼ (Cₛ.[∘]t {γ = f}{δ = δ} ◼ e₄ δ))
      in cong₂ Ĉ.Y▹ e₂ e₅ ◼ cong (λ x → Yˢ x γ) (Ĉ.▹η {A = CTm Ĉ.[ A ]T})

  Sub→ : {Γ Δ : Cₛₛ.Con} → Cₛₛ.Sub Δ Γ → Cₛ.Sub (Con→ Δ) (Con→ Γ)
  Sub→ {Γ} {Δ} γ = φfun Γ (Yˢ γ (φinv Δ Cₛ.id))

  Ty→ : (Γ : Cₛₛ.Con) → Cₛₛ.Ty Γ → Cₛ.Ty (Con→ Γ)
  Ty→ Γ A = ∣ A ∣ (φinv Γ Cₛ.id)

  -- Inverse to Ty→
  -- Ty← : (Γ : Cₛₛ.Con) → Cₛ.Ty (Con→ Γ) → Cₛₛ.Ty Γ
  -- Ty← Γ A = mkSub (λ γ → A Cₛ.[ φfun Γ γ ]T)
  --                 (λ γ δ → Cₛ.[∘]T {γ = φfun Γ γ} {δ = δ} ⁻¹ ◼ cong (Cₛ._[_]T A) (φfun→ Γ γ δ ⁻¹))

  -- Ty-sec : (Γ : Cₛₛ.Con) (A : Cₛₛ.Ty Γ) → Ty← Γ (Ty→ Γ A) ~ A
  -- Ty-sec Γ A = Sub≡ (funextHᵢᵣ λ {Δ} γ → A .rel (φinv Γ Cₛ.id) (φfun Γ γ) ◼ cong ∣ A ∣ (φinv→ Γ Cₛ.id (φfun Γ γ) ⁻¹ ◼ φret Γ γ))

  Tm→ : (Γ : Cₛₛ.Con) → (A : Cₛₛ.Ty Γ) → Cₛₛ.Tm Γ A → Cₛ.Tm (Con→ Γ) (Ty→ Γ A)
  Tm→ Γ A a = Ĉ.∣ a ∣ (φinv Γ Cₛ.id)

  -- Now that we have Con→, Sub→, Ty→, Tm→, we can prove that they provide a CwF morphism from Cₛₛ to Cₛ

  ∘→ : ∀ {Γ Δ} (γ : Cₛₛ.Sub Δ Γ) {Θ} (δ : Cₛₛ.Sub Θ Δ) → Sub→ {Γ}{Θ} (Cₛₛ._∘_ {Γ}{Δ} γ {Θ} δ) ~ (Sub→ {Γ}{Δ} γ) Cₛ.∘ (Sub→ {Δ}{Θ} δ)
  ∘→ {Γ}{Δ} γ {Θ} δ =
    cong (φfun Γ) (cong (Yˢ γ) ((φret Δ (Yˢ δ (φinv Θ Cₛ.id))) ⁻¹ ◼ (φinv→ Δ Cₛ.id (Sub→ {Δ}{Θ} δ))))
    ◼ φfun→ Γ (Yˢ γ (φinv Δ Cₛ.id)) (Sub→ {Δ}{Θ} δ)

  id→ : ∀ {Γ} → Sub→ {Γ}{Γ} (Cₛₛ.id {Γ = Γ}) ~ Cₛ.id {Γ = Con→ Γ}
  id→ {Γ} = φsec Γ (Cₛ.id {Γ = Con→ Γ})

  ◇→ : Con→ (Cₛₛ.◇) ~ Cₛ.◇
  ◇→ = ~refl

  ε→ : ∀ {Γ} → Sub→ {Cₛₛ.◇}{Γ} (Cₛₛ.ε {Γ = Γ}) ~ Cₛ.ε {Γ = Con→ Γ}
  ε→ {Γ} = ~refl

  [→]T : ∀ {Γ} (A : Cₛₛ.Ty Γ) {Δ} (γ : Cₛₛ.Sub Δ Γ) → Ty→ Δ (Cₛₛ._[_]T {Γ} A {Δ} γ) ~ (Ty→ Γ A) Cₛ.[ Sub→ {Γ}{Δ} γ ]T
  [→]T {Γ} A {Δ} γ =
    cong ∣ A ∣ (φret Γ (Yˢ γ (φinv Δ Cₛ.id)) ⁻¹ ◼ φinv→ Γ Cₛ.id (Sub→ {Γ}{Δ} γ))
    ◼ (A .rel (φinv Γ Cₛ.id) (Sub→ {Γ}{Δ} γ) ⁻¹)

  [→]t : ∀ {Γ} (A : Cₛₛ.Ty Γ) (a : Cₛₛ.Tm Γ A) {Δ} (γ : Cₛₛ.Sub Δ Γ)
       → Tm→ Δ (Cₛₛ._[_]T {Γ} A {Δ} γ) (Cₛₛ._[_]t {Γ} {A} a {Δ} γ) ~ (Tm→ Γ A a) Cₛ.[ Sub→ {Γ}{Δ} γ ]t
  [→]t {Γ} A a {Δ} γ =
    cong Ĉ.∣ a ∣ (φret Γ (Yˢ γ (φinv Δ Cₛ.id)) ⁻¹ ◼ φinv→ Γ Cₛ.id (Sub→ {Γ}{Δ} γ))
    ◼ a .Ĉ.rel (φinv Γ Cₛ.id) (Sub→ {Γ}{Δ} γ) ⁻¹

  ▹→ : ∀ {Γ} (A : Cₛₛ.Ty Γ) → Con→ (Γ Cₛₛ.▹ A) ~ (Con→ Γ) Cₛ.▹ (Ty→ Γ A)
  ▹→ {Γ} A = ~refl

  ,→ : ∀ {Γ Δ} (γ : Cₛₛ.Sub Δ Γ) {A : Cₛₛ.Ty Γ} {A' : Cₛₛ.Ty Δ} (e : Cₛₛ._[_]T {Γ} A {Δ} γ ~ A') (a : Cₛₛ.Tm Δ A')
       → Sub→ {Γ Cₛₛ.▹ A}{Δ} (Cₛₛ._,[_]_ {Γ}{Δ} γ {A}{A'} e a)
         ~ Cₛ._,[_]_ (Sub→ {Γ}{Δ} γ) {Ty→ Γ A} ([→]T {Γ} A {Δ} γ ⁻¹ ◼ cong (Ty→ Δ) e) (Tm→ Δ A' a)
  ,→ {Γ}{Δ} γ {A}{A'} e a =
    let
      e₀ : ∀ {Θ} (γ : Yᶜ (El Γ) Θ) → φinv Γ Cₛ.id |ᶜ φfun Γ γ ~ γ
      e₀ γ = (φinv→ Γ Cₛ.id (φfun Γ γ) ⁻¹ ◼ φret Γ γ)

      e₁ : ∀ {Θ} (γ : Yᶜ (El Γ) Θ) → ∣ A ∣ (φinv Γ Cₛ.id) Cₛ.[ φfun Γ γ ]T ~ ∣ A ∣ γ
      e₁ γ = A .rel (φinv Γ Cₛ.id) (φfun Γ γ) ◼ cong ∣ A ∣ (e₀ γ)
    in Ctₛ.cong-subExt {Con→ Γ}{Con→ Δ}{Sub→ {Γ}{Δ} γ}{Sub→ {Γ}{Δ} γ} ~refl
                      (cong (λ X → ∣ X ∣ (φinv Δ Cₛ.id)) e) (e₁ (Yˢ γ (φinv Δ Cₛ.id)))
                      ([→]T {Γ} A {Δ} γ ⁻¹ ◼ cong (Ty→ Δ) e) (coe≡-eq _ (Tm→ Δ A' a) ⁻¹)

  p→ : ∀ {Γ} (A : Cₛₛ.Ty Γ) → Sub→ {Γ}{Γ Cₛₛ.▹ A} (Cₛₛ.p {Γ} {A}) ~ Cₛ.p {A = Ty→ Γ A}
  p→ {Γ} A = cong (φfun Γ) (φinv→ Γ Cₛ.id Cₛ.p ⁻¹) ◼ φsec Γ Cₛ.p

  q→ : ∀ {Γ} (A : Cₛₛ.Ty Γ) → Tm→ (Γ Cₛₛ.▹ A) (Cₛₛ._[_]T {Γ} A {Γ Cₛₛ.▹ A} (Cₛₛ.p {Γ} {A})) (Cₛₛ.q {Γ} {A}) ~ Cₛ.q {A = Ty→ Γ A}
  q→ {Γ} A = coe≡-eq _ (Cₛ.q Cₛ.[ Cₛ.id ]t) ⁻¹ ◼ Cₛ.[id]t {a = Cₛ.q}

  Cₛₛ→Cₛ : CwF→ Cₛₛ Cₛ
  Cₛₛ→Cₛ = record
           { Con→ = Con→
           ; Sub→ = λ {Γ}{Δ} γ → Sub→ {Γ}{Δ} γ
           ; ∘→ = λ {Γ}{Δ} → ∘→ {Γ}{Δ}
           ; id→ = λ {Γ} → id→ {Γ}
           ; ◇→ = ~refl
           ; ε→ = ~refl
           ; Ty→ = λ {Γ} → Ty→ Γ
           ; [→]T = λ {Γ} A {Δ} γ → [→]T {Γ} A {Δ} γ
           ; Tm→ = λ {Γ}{A} → Tm→ Γ A
           ; [→]t = λ {Γ} A a {Δ} γ → [→]t {Γ} A a {Δ} γ
           ; ▹→ = ~refl
           ; ,→ = λ {Γ}{Δ} γ {A}{A'} e a → ,→ {Γ}{Δ} γ {A}{A'} e a
           ; p→ = λ {Γ} A → p→ {Γ} A
           ; q→ = λ {Γ} A → q→ {Γ} A
           }

  Π→ : ∀{Γ}{A : Cₛₛ.Ty Γ}{B : Cₛₛ.Ty (Γ Cₛₛ.▹ A)} → Ty→ Γ (Mₛₛ.Π {Γ} A B) ~ Mₛ.Π (Ty→ Γ A) (Ty→ (Γ Cₛₛ.▹ A) B)
  Π→ = ~refl

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

  app→ : ∀{Γ}{A : Cₛₛ.Ty Γ}{B : Cₛₛ.Ty (Γ Cₛₛ.▹ A)}(t : Cₛₛ.Tm Γ (Mₛₛ.Π {Γ} A B))(u : Cₛₛ.Tm Γ A)
         → Tm→ Γ (Cₛₛ._[_]T {Γ Cₛₛ.▹ A} B {Γ} (CwF-tools.sg Cₛₛ {Γ}{A} u)) (Mₛₛ.app {Γ}{A}{B} t u) ~ Mₛ.app (Tm→ Γ (Mₛₛ.Π {Γ} A B) t) (Tm→ Γ A u)
  app→ {Γ}{A}{B} t u = coe≡-eq _ (Mₛ.app (Tm→ Γ (Mₛₛ.Π {Γ} A B) t) (Tm→ Γ A u)) ⁻¹

  𝔹→ : Ty→ Cₛₛ.◇ Mₛₛ.𝔹 ~ Mₛ.𝔹
  𝔹→ = cong (Cₛ._[_]T Mₛ.𝔹) {Cₛ.ε} {Cₛ.id} (Cₛ.◇η ⁻¹) ◼ Cₛ.[id]T

  𝕥→ : Tm→ Cₛₛ.◇ Mₛₛ.𝔹 Mₛₛ.𝕥 ~ Mₛ.𝕥
  𝕥→ = cong (Cₛ._[_]t Mₛ.𝕥) {Cₛ.ε} {Cₛ.id} (Cₛ.◇η ⁻¹) ◼ Cₛ.[id]t

  𝕗→ : Tm→ Cₛₛ.◇ Mₛₛ.𝔹 Mₛₛ.𝕗 ~ Mₛ.𝕗
  𝕗→ = cong (Cₛ._[_]t Mₛ.𝕗) {Cₛ.ε} {Cₛ.id} (Cₛ.◇η ⁻¹) ◼ Cₛ.[id]t

  ifᵀ→ : ∀ {Γ} (b : Cₛₛ.Tm Γ (Cₛₛ._[_]T {Cₛₛ.◇} Mₛₛ.𝔹 {Γ} (Cₛₛ.ε {Γ}))) (A B : Cₛₛ.Ty Γ)
         → Ty→ Γ (Mₛₛ.ifᵀ {Γ} b A B) ~ Mₛ.ifᵀ ((Tm→ Γ (Cₛₛ._[_]T {Cₛₛ.◇} Mₛₛ.𝔹 {Γ} (Cₛₛ.ε {Γ})) b)) (Ty→ Γ A) (Ty→ Γ B)
  ifᵀ→ {Γ} b A B = ~refl

  ifᵗ→ : ∀{Γ} →
    let
      𝔹[ε] = Cₛₛ._[_]T {Cₛₛ.◇} Mₛₛ.𝔹 {Γ} (Cₛₛ.ε {Γ})
      𝕥[ε] = Cₛₛ._[_]t {Cₛₛ.◇} {Mₛₛ.𝔹} Mₛₛ.𝕥 {Γ} (Cₛₛ.ε {Γ})
      𝕗[ε] = Cₛₛ._[_]t {Cₛₛ.◇} {Mₛₛ.𝔹} Mₛₛ.𝕗 {Γ} (Cₛₛ.ε {Γ})
    in (P : Cₛₛ.Ty (Γ Cₛₛ.▹ 𝔹[ε]))
       (P𝕥 : Cₛₛ.Tm Γ (Cₛₛ._[_]T {Γ Cₛₛ.▹ 𝔹[ε]} P {Γ} (CwF-tools.sg Cₛₛ {Γ}{𝔹[ε]} 𝕥[ε])))
       (P𝕗 : Cₛₛ.Tm Γ (Cₛₛ._[_]T {Γ Cₛₛ.▹ 𝔹[ε]} P {Γ} (CwF-tools.sg Cₛₛ {Γ}{𝔹[ε]} 𝕗[ε])))
       (b : Cₛₛ.Tm Γ 𝔹[ε])
       → Tm→ Γ (Cₛₛ._[_]T {Γ Cₛₛ.▹ 𝔹[ε]} P {Γ} (CwF-tools.sg Cₛₛ {Γ}{𝔹[ε]} b)) (Mₛₛ.ifᵗ {Γ} P P𝕥 P𝕗 b)
         ~ Mₛ.ifᵗ (Ty→ (Γ Cₛₛ.▹ 𝔹[ε]) P)
                 (coe (cong (Cₛ.Tm (Con→ Γ)) (Tools→.[sgε]T→ Cₛₛ→Cₛ {Γ}{Mₛₛ.𝔹}{Mₛₛ.𝕥} P 𝔹→ 𝕥→))
                      (Tm→ Γ (Cₛₛ._[_]T {Γ Cₛₛ.▹ 𝔹[ε]} P {Γ} (CwF-tools.sg Cₛₛ {Γ}{𝔹[ε]} 𝕥[ε])) P𝕥))
                 (coe (cong (Cₛ.Tm (Con→ Γ)) (Tools→.[sgε]T→ Cₛₛ→Cₛ {Γ}{Mₛₛ.𝔹}{Mₛₛ.𝕗} P 𝔹→ 𝕗→))
                      (Tm→ Γ (Cₛₛ._[_]T {Γ Cₛₛ.▹ 𝔹[ε]} P {Γ} (CwF-tools.sg Cₛₛ {Γ}{𝔹[ε]} 𝕗[ε])) P𝕗))
                 (Tm→ Γ 𝔹[ε] b)
  ifᵗ→ {Γ} P P𝕥 P𝕗 b =
    let
      𝔹[ε] = Cₛₛ._[_]T {Cₛₛ.◇} Mₛₛ.𝔹 {Γ} (Cₛₛ.ε {Γ})
      𝕥[ε] = Cₛₛ._[_]t {Cₛₛ.◇} {Mₛₛ.𝔹} Mₛₛ.𝕥 {Γ} (Cₛₛ.ε {Γ})
      𝕗[ε] = Cₛₛ._[_]t {Cₛₛ.◇} {Mₛₛ.𝔹} Mₛₛ.𝕗 {Γ} (Cₛₛ.ε {Γ})
    in coe≡-eq _ (Mₛ.ifᵗ (Ty→ (Γ Cₛₛ.▹ 𝔹[ε]) P)
                        (coe (cong (Cₛ.Tm (Con→ Γ)) (Tools→.[sgε]T→ Cₛₛ→Cₛ {Γ}{Mₛₛ.𝔹}{Mₛₛ.𝕥} P 𝔹→ 𝕥→))
                             (Tm→ Γ (Cₛₛ._[_]T {Γ Cₛₛ.▹ 𝔹[ε]} P {Γ} (CwF-tools.sg Cₛₛ {Γ}{𝔹[ε]} 𝕥[ε])) P𝕥))
                        (coe (cong (Cₛ.Tm (Con→ Γ)) (Tools→.[sgε]T→ Cₛₛ→Cₛ {Γ}{Mₛₛ.𝔹}{Mₛₛ.𝕗} P 𝔹→ 𝕗→))
                             (Tm→ Γ (Cₛₛ._[_]T {Γ Cₛₛ.▹ 𝔹[ε]} P {Γ} (CwF-tools.sg Cₛₛ {Γ}{𝔹[ε]} 𝕗[ε])) P𝕗))
                        (Tm→ Γ 𝔹[ε] b)) ⁻¹

  Mₛₛ→Mₛ : Model→ Cₛₛ→Cₛ Mₛₛ Mₛ
  Mₛₛ→Mₛ = record
            { Π→ = λ {Γ}{A}{B} → Π→ {Γ}{A}{B}
            ; lam→ = λ {Γ}{A}{B}{t} → lam→ {Γ}{A}{B}{t}
            ; app→ = λ {Γ}{A}{B} t u → app→ {Γ}{A}{B} t u
            ; 𝔹→ = 𝔹→
            ; 𝕥→ = 𝕥→
            ; 𝕗→ = 𝕗→
            ; ifᵀ→ = λ {Γ} b A B → ifᵀ→ {Γ} b A B
            ; ifᵗ→ = λ {Γ} P P𝕥 P𝕗 b → ifᵗ→ {Γ} P P𝕥 P𝕗 b
            }