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

module strictifyPMP where

open import lib
open import model

-- In this file, we define a strictified model using Pédrot's strict presheaves

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

  import strictifyCat C M as strictifyCat

  Cₛ = strictifyCat.Cₛ
  Mₛ = strictifyCat.Mₛ

  private module Cₛ = CwF Cₛ
  private module Ct = CwF-tools Cₛ
  private module Mₛ = Model Mₛ

  variable i j k l : Level

  Ob  = Cₛ.Con -- named x,y,z
  Hom = Cₛ.Sub -- named f,g,h

  -- sections of a strict presheaf on C/x
  record Y
    (x : Ob)
    (A : ∀ {y} → Hom y x → Set i)
    (A-rel : ∀ {y} (f : Hom y x) → (∀ {z} (g : Hom z y) → A (f Cₛ.∘ g)) → Prop i)
    : Set i
    where
    constructor mkY
    field
      a   : ∀ {y} → (f : Hom y x) → A f
      rel : ∀ {y} → (f : Hom y x) → A-rel f (λ g → a (f Cₛ.∘ g))
  open Y public renaming (a to ∣_∣)

  record Con (i : Level) : Set (lsuc i) where
    constructor mkCon
    field
      Γ   : Ob → Set i
      rel : ∀ {x} → (∀ {y : Ob} → Hom y x → Γ y) → Prop i
  open Con public renaming (Γ to ∣_∣)

  -- converting Γ to ordinary presheaf
  Yᶜ : Con i → Ob → Set i
  Yᶜ Γ x = Y x (λ {y} _ → ∣ Γ ∣ y) (λ _ → Γ .rel)

  Yᶜ~ : ∀ {Γ : Con i} {x₀ x₁} (xₑ : x₀ ~ x₁) {γ₀ : Yᶜ Γ x₀} {γ₁ : Yᶜ Γ x₁} → (λ {x} → ∣ γ₀ ∣ {x}) ~ (λ {x} → ∣ γ₁ ∣ {x}) → γ₀ ~ γ₁
  Yᶜ~ xₑ γₑ = ~congₚₛ (cong₂ (λ x → mkY {x = x}) xₑ γₑ)

  Yᶜ≡ : ∀ {Γ : Con i} {x} → {γ₀ γ₁ : Yᶜ Γ x} → (λ {x} → ∣ γ₀ ∣ {x}) ~ (λ {x} → ∣ γ₁ ∣ {x}) → γ₀ ~ γ₁
  Yᶜ≡ e = ~congₚₛ (cong mkY e)

  infixl  _|ᶜ_
  _|ᶜ_ : ∀ {Γ : Con i} {x} → Yᶜ Γ x → ∀ {y} → Hom y x → Yᶜ Γ y
  ∣ γ |ᶜ f ∣ g = ∣ γ ∣ (f Cₛ.∘ g)
  (γ |ᶜ f) .rel g = γ .rel (f Cₛ.∘ g)

  record Sub (Δ : Con i) (Γ : Con j) : Set (i ⊔ j) where
    constructor mkSub
    field
      γ   : ∀ {x} → (δ : Yᶜ Δ x) → ∣ Γ ∣ x
      rel : ∀ {x} → (δ : Yᶜ Δ x) → Γ .rel (λ f → γ (δ |ᶜ f))
  open Sub public renaming (γ to ∣_∣)

  Sub≡ : ∀ {Γ : Con i} {Δ : Con j}
    {γ₀ γ₁ : Sub Δ Γ} → (λ {x} → ∣ γ₀ ∣ {x}) ~ (λ {x} → ∣ γ₁ ∣ {x}) → γ₀ ~ γ₁
  Sub≡ e = ~congₚₛ (cong mkSub e)

  -- converting a Sub into a natural transformation
  Yˢ : ∀ {Γ : Con i} {Δ : Con j} (σ : Sub Δ Γ) → ∀ {x} → Yᶜ Δ x → Yᶜ Γ x
  ∣ Yˢ σ δ ∣ f =  ∣ σ ∣ (δ |ᶜ f)
  Yˢ σ δ .rel f =  σ .rel (δ |ᶜ f)

  infixl  _∘_
  _∘_ : ∀ {Γ : Con i} {Δ : Con j} {Θ : Con k} → Sub Δ Γ → Sub Θ Δ → Sub Θ Γ
  ∣ σ ∘ τ ∣ θ = ∣ σ ∣ (Yˢ τ θ)
  (σ ∘ τ) .rel θ = σ .rel (Yˢ τ θ)

  comp : ∀ (Γ : Con i) {Δ : Con i} → Sub Δ Γ → ∀{Θ : Con i} → Sub Θ Δ → Sub Θ Γ
  comp Γ σ τ = _∘_ {Γ = Γ} σ τ
  syntax comp Γ σ τ = σ ∘[ Γ ] τ

  assoc : ∀ {Γ : Con i} {Δ : Con j} {Θ : Con k} {Ξ : Con l} (σ : Sub Δ Γ) (τ : Sub Θ Δ) (υ : Sub Ξ Θ) → σ ∘ (τ ∘ υ) ~ (σ ∘ τ) ∘ υ
  assoc σ τ υ = ~refl

  id : ∀ {Γ : Con i} → Sub Γ Γ
  ∣ id ∣ γ = ∣ γ ∣ Cₛ.id
  id .rel γ = γ .rel Cₛ.id

  idr : ∀ {Γ : Con i} {Δ : Con j} (σ : Sub Δ Γ) → σ ∘ id ~ σ
  idr σ = ~refl

  idl : ∀ {Γ : Con i} {Δ : Con j} (σ : Sub Δ Γ) → id ∘ σ ~ σ
  idl σ = ~refl

  -- CwF structure on strict presheaves
  module Ĉ where
    record Ty (Γ : Con i) (j : Level) : Set (i ⊔ lsuc j) where
      field
        A   : ∀ {x} → (γ : Yᶜ Γ x) → Set j
        rel : ∀ {x} → (γ : Yᶜ Γ x) → (∀ {y} (f : Hom y x) → A (γ |ᶜ f)) → Prop j
    open Ty public renaming (A to ∣_∣)

    Yᵀ : ∀ {Γ : Con i} → Ty Γ j → ∀ {x} → Yᶜ Γ x → Set j
    Yᵀ A {x = x} γ = Y x (λ f → ∣ A ∣ (γ |ᶜ f)) (λ f → A .rel (γ |ᶜ f))

    Yᵀ≡ : ∀ {Γ : Con i} (A : Ty Γ j) {x₀ x₁} (xₑ : x₀ ~ x₁) {γ₀ : Yᶜ Γ x₀} {γ₁ : Yᶜ Γ x₁} (γₑ : γ₀ ~ γ₁)
            {a₀ : Yᵀ A {x₀} γ₀} {a₁ : Yᵀ A {x₁} γ₁} → (λ {x} → ∣ a₀ ∣ {x}) ~ (λ {x} → ∣ a₁ ∣ {x}) → a₀ ~ a₁
    Yᵀ≡ A xₑ γₑ aₑ = ~congₚₛ (cong₃ (λ x γ → mkY {x = x} {A = λ f → ∣ A ∣ (γ |ᶜ f)} {A-rel = λ f → A .rel (γ |ᶜ f)}) xₑ γₑ aₑ)

    infixl  ⟨_,_⟩_|ᵀ_
    ⟨_,_⟩_|ᵀ_ : ∀ {Γ : Con i} (A : Ty Γ j) {x} (γ : Yᶜ Γ x) → Yᵀ A γ → ∀ {y} (f : Hom y x) → Yᵀ A (γ |ᶜ f)
    ∣ ⟨ A , γ ⟩ a |ᵀ f ∣ g = ∣ a ∣ (f Cₛ.∘ g)
    (⟨ A , γ ⟩ a |ᵀ f) .rel g = a .rel (f Cₛ.∘ g)

    infixl  _[_]T
    _[_]T : ∀ {Γ : Con i} {Δ : Con j} → Ty Γ k → Sub Δ Γ → Ty Δ k
    ∣ A [ σ ]T ∣ δ = ∣ A ∣ (Yˢ σ δ)
    (A [ σ ]T) .rel δ = A .rel (Yˢ σ δ)

    [∘]T : ∀ {Γ : Con i} {Δ : Con j} {Θ : Con k}
             (A : Ty Γ l) (σ : Sub Δ Γ) (τ : Sub Θ Δ) → A [ σ ∘ τ ]T ~ A [ σ ]T [ τ ]T
    [∘]T A γ δ = ~refl

    [id]T : ∀ {Γ : Con i} (A : Ty Γ j) → A [ id ]T ~ A
    [id]T A = ~refl

    record Tm (Γ : Con i) (A : Ty Γ j) : Set (i ⊔ j) where
      constructor mkTm
      field
        a   : ∀ {x} (γ : Yᶜ Γ x) → ∣ A ∣ γ
        rel : ∀ {x} (γ : Yᶜ Γ x) → A .rel γ (λ f → a (γ |ᶜ f))
    open Tm public renaming (a to ∣_∣)

    Tm≡ : ∀ {Γ : Con i} {A : Ty Γ j} {a₀ a₁ : Tm Γ A} → (λ {x} → ∣ a₀ ∣ {x}) ~ (λ {x} → ∣ a₁ ∣ {x}) → a₀ ~ a₁
    Tm≡ e = ~congₚₛ (cong mkTm e)

    Yᵗ : ∀ {Γ : Con i} {A : Ty Γ j} → Tm Γ A → ∀ {x} (γ : Yᶜ Γ x) → Yᵀ A γ
    ∣ Yᵗ a γ ∣ f = ∣ a ∣ (γ |ᶜ f)
    Yᵗ a γ .rel f = a .rel (γ |ᶜ f)

    infixl  _[_]t
    _[_]t : ∀ {Γ : Con i} {Δ : Con j} {A : Ty Γ k} → Tm Γ A → (σ : Sub Δ Γ) → Tm Δ (A [ σ ]T)
    ∣ a [ σ ]t ∣ δ = ∣ a ∣ (Yˢ σ δ)
    (a [ σ ]t) .rel δ = a .rel (Yˢ σ δ)

    [∘]t : ∀ {Γ : Con i} {Δ : Con j} {Θ : Con k} {A : Ty Γ l}
      (a : Tm Γ A) (σ : Sub Δ Γ) (τ : Sub Θ Δ) → a [ σ ∘ τ ]t ~ a [ σ ]t [ τ ]t
    [∘]t a σ τ = ~refl

    [id]t : ∀ {Γ : Con i} {A : Ty Γ j} (a : Tm Γ A) → a [ id ]t ~ a
    [id]t a = ~refl

    record ∣▹∣ (Γ : Con i) (A : Ty Γ j) (x : Ob) : Set (i ⊔ j) where
      constructor mk▹
      field
        con : Yᶜ Γ x
        ty : ∣ A ∣ con
    open ∣▹∣ public

    record ▹-rel
      {Γ : Con i} {A : Ty Γ j} {x : Ob} (γa : ∀ {y} → Hom y x → ∣▹∣ Γ A y) : Prop (i ⊔ j)
      where
      constructor mk▹rel
      field
        con : ∀ {y} (f : Hom y x) {z} (g : Hom z y) → ∣ γa f .con ∣ g ~ ∣ γa (f Cₛ.∘ g) .con ∣ Cₛ.id
        ty :
          A .rel
            record
              { a = λ f → ∣ γa f .∣▹∣.con ∣ Cₛ.id
              ; rel = λ f → coeₚ (cong (Γ .rel) (funextHᵢᵣ λ g → con f g)) (γa f .∣▹∣.con .rel Cₛ.id) }
            (λ f → coe (cong ∣ A ∣ (Yᶜ≡ (funextHᵢᵣ λ g → con f g))) (γa f .ty))
    open ▹-rel public

    infixl  _▹_
    _▹_ : (Γ : Con i) → Ty Γ j → Con (i ⊔ j)
    ∣ Γ ▹ A ∣ = ∣▹∣ Γ A
    (Γ ▹ A) .rel = ▹-rel

    Y▹ : {Γ : Con i} {A : Ty Γ j} {x : Ob} (γ : Yᶜ Γ x) → Yᵀ A γ → Yᶜ (Γ ▹ A) x
    ∣ Y▹ γ a ∣ f .con = γ |ᶜ f
    ∣ Y▹ γ a ∣ f .ty = ∣ a ∣ f
    Y▹ γ a .rel f .con = λ _ _ → ~refl
    Y▹ γ a .rel f .ty = a .rel f

    p : {Γ : Con i} {A : Ty Γ j} → Sub (Γ ▹ A) Γ
    ∣ p ∣ γa = ∣ ∣ γa ∣ Cₛ.id .con ∣ Cₛ.id
    p {Γ = Γ} .rel γa =
      let e = funextHᵢᵣ λ f → γa .rel Cₛ.id .con Cₛ.id f in
      coeₚ (cong (Γ .rel) e) (∣ γa ∣ Cₛ.id .con .rel Cₛ.id)

    q : {Γ : Con i} {A : Ty Γ j} → Tm (Γ ▹ A) (A [ p ]T)
    ∣ q {A = A} ∣ γa =
      let e = Yᶜ≡ (funextHᵢᵣ λ f → γa .rel Cₛ.id .con Cₛ.id f) in
      coe (cong ∣ A ∣ e) (∣ γa ∣ Cₛ.id .ty)
    q .rel γa = γa .rel Cₛ.id .ty

    infixl  _,_
    _,_ : {Γ : Con i} {Δ : Con j} {A : Ty Γ k} (σ : Sub Δ Γ) → Tm Δ (A [ σ ]T) → Sub Δ (Γ ▹ A)
    ∣ σ , a ∣ δ .con = Yˢ σ δ
    ∣ σ , a ∣ δ .ty = ∣ a ∣ δ
    (σ , a) .rel δ .con = λ _ _ → ~refl
    (_,_ {A = A} σ a) .rel δ .ty = a .rel δ

    infixl  _,⟨_⟩_
    _,⟨_⟩_ : {Γ : Con i} {Δ : Con j} (γ : Sub Δ Γ) (A : Ty Γ k) → Tm Δ (A [ γ ]T) → Sub Δ (Γ ▹ A)
    γ ,⟨ A ⟩ a = γ , a

    _,[_]_ : ∀{Γ : Con i}{Δ : Con j}(γ : Sub Δ Γ) {A : Ty Γ k} {A' : Ty Δ k} → A [ γ ]T ~ A' → Tm Δ A' → Sub Δ (Γ ▹ A)
    ∣ _,[_]_ {Γ}{Δ = Δ} γ {A}{A'} e a ∣ δ .con = Yˢ γ δ
    ∣ _,[_]_ {Γ}{Δ = Δ} γ {A}{A'} e a ∣ δ .ty = coe ((cong (λ (A : Ty Δ _) → ∣ A ∣ δ) e) ⁻¹) (∣ a ∣ δ)
    _,[_]_ {Γ = Γ}{Δ = Δ} γ {A}{A'} e a .rel δ .con = λ _ _ → ~refl
    _,[_]_ {Γ = Γ}{Δ = Δ} γ {A}{A'} e a .rel {x = x} δ .ty =
      let e = ~cong (cong (λ (A : Ty Δ _) → A .rel δ) (e ⁻¹))
                    (funextᵢ λ xₑ →
                      funext λ {γ₀} {γ₁} γₑ →
                        cong₂ (λ y (γ : Hom y x) → ∣ a ∣ (δ |ᶜ γ)) xₑ γₑ ◼ coe≡-eq _ (∣ a ∣ (δ |ᶜ γ₁)))
      in coeₚ e (a .rel δ)

    ,∘ : {Γ : Con i} {Δ : Con j} {Θ : Con k} {A : Ty Γ l}
      (σ : Sub Δ Γ) (a : Tm Δ (A [ σ ]T)) (τ : Sub Θ Δ) →
      (σ ,⟨ A ⟩ a) ∘ τ ~ (σ ∘ τ , a [ τ ]t)
    ,∘ σ a τ = ~refl

    ▹β₁ : {Γ : Con i} {Δ : Con j} {A : Ty Γ k} (σ : Sub Δ Γ) (a : Tm Δ (A [ σ ]T)) → p ∘ (σ ,⟨ A ⟩ a) ~ σ
    ▹β₁ σ a = ~refl

    ▹β₂ : {Γ : Con i} {Δ : Con j} {A : Ty Γ k} (σ : Sub Δ Γ) (a : Tm Δ (A [ σ ]T)) → q [ σ ,⟨ A ⟩ a ]t ~ a
    ▹β₂ γ a = ~refl

    ▹η : {Γ : Con i} {A : Ty Γ j} → (p {A = A} ,⟨ A ⟩ q) ~ id {Γ = Γ ▹ A}
    ▹η {Γ = Γ} {A = A} =
      Sub≡ (funextᵢ λ {x} {x'} ex →
            funext λ {γa} {γa'} eγa →
              cong₃ (λ x → mk▹ {Γ = Γ} {A = A} {x}) ex
                ((cong₂ (λ z → Yˢ p {z}) ex eγa) ◼ (Yᶜ≡ (funextHᵢᵣ (λ f → γa' .rel Cₛ.id .con Cₛ.id f) ⁻¹)))
                ((coe≡-eq _ (∣ γa ∣ Cₛ.id .ty)) ⁻¹ ◼ (cong₂ (λ x (γ : Yᶜ (Γ ▹ A) x) → ∣ γ ∣ Cₛ.id .ty) ex eγa)))

    ↑ : {Γ : Con i} {Δ : Con j} {A : Ty Γ k} (σ : Sub Δ Γ) → Sub (Δ ▹ A [ σ ]T) (Γ ▹ A)
    ↑ σ = σ ∘ p , q

    sg : {Γ : Con i} {A : Ty Γ j} (a : Tm Γ A) → Sub Γ (Γ ▹ A)
    sg a = id , a

    ◇ : Con lzero
    ∣ ◇ ∣ x = ⊤
    ◇ .rel γ = ⊤ₚ

    ε : {Γ : Con i} → Sub Γ ◇
    ∣ ε ∣ γ = _
    ε .rel γ = ttₚ

    ε∘ : {Γ : Con i} {Δ : Con j} (σ : Sub Δ Γ) → ε ∘ σ ~ ε
    ε∘ γ = ~refl

    ◇η : (ε {Γ = ◇}) ~ (id {Γ = ◇})
    ◇η = ~refl

    -- Now we build a universe hierarchy for the CwF of strict presheaves
    -- These universes come from the external universes Set i, not from the CwF structure on M
    {-
    record ∣U∣ (i : Level) (x : Ob) : Set (lsuc i) where
      field
        t : ∀ {y} → Hom y x → Set i   -- this is simpler than just Ty (yoneda x)
        rel : (∀ {y} (f : Hom y x) → t f) → Prop i
    open ∣U∣ public renaming (t to ∣_∣)

    U : (i : Level) → {Γ : Con j} → Ty Γ (lsuc i)
    ∣ U i ∣ {x} γ = ∣U∣ i x
    U i .rel {x} γ A =
      (λ {y} (f : Hom y x) {z} (g : Hom z y) → ∣ A f ∣ g) ~
      (λ {y} (f : Hom y x) {z} (g : Hom z y) → ∣ A (f Cₛ.∘ g) ∣ Cₛ.id)

    U-[] : (i : Level) {Γ : Con j} {Δ : Con k} (γ : Sub Δ Γ) → U i [ γ ]ᵀ ~ U i
    U-[] i γ = ~refl

    El : {Γ : Con j} → Tm Γ (U i) → Ty Γ i
    ∣ El A ∣ γ = ∣ ∣ A ∣ γ ∣ Cₛ.id
    El A .rel γ a =
      ∣ A ∣ γ .rel λ f → let e = (~congᵢᵣ (~congᵢᵣ ((A .rel γ) ⁻¹) ~refl (~refl {a = Cₛ.id})) ~refl (~refl {a = f})) in
                             coe (~to≡ e) (a f)

    El-[] : {Γ : Con j} {Δ : Con k} (A : Tm Γ (U i)) (γ : Sub Δ Γ) → El A [ γ ]ᵀ ~ El (A [ γ ]ᵗ)
    El-[] A γ = ~refl

    c : {Γ : Con j} → Ty Γ i → Tm Γ (U i)
    ∣ ∣ c A ∣ γ ∣ f = ∣ A ∣ (γ |ᶜ f)
    ∣ c A ∣ γ .rel a = A .rel γ a
    c A .rel γ = ~refl

    c-[] : {Γ : Con j} {Δ : Con k} (A : Ty Γ i) (γ : Sub Δ Γ) → c A [ γ ]ᵗ ~ c (A [ γ ]ᵀ)
    c-[] A γ = ~refl

    U-β : {Γ : Con j} (A : Ty Γ i) → El (c A) ~ A
    U-β A = ~refl

    {-
    U-η : (A : Tm Γ (U i)) → c (El A) ≡ A
    U-η A = Tm-≡ (funextᵢ (funext λ γ → sym (∣U∣-≡ (ap (λ a → a Cₛ.id) (A .rel γ)) {!refl!})))
    -}

    -- Then we equip the CwF of strict presheaves with dependent products

    Π : {Γ : Con i} (A : Ty Γ j) → Ty (Γ ▹ A) k → Ty Γ (j ⊔ k)
    ∣ Π A B ∣ γ = (a : Yᵀ A γ) → ∣ B ∣ (Y▹ γ a)
    Π A B .rel γ t = (a : Yᵀ A γ) → B .rel (Y▹ γ a) λ f → t f (⟨ A , γ ⟩ a |ᵀ f)

    Π-[] : {Γ : Con i} {Δ : Con j}
      (A : Ty Γ k) (B : Ty (Γ ▹ A) l) (γ : Sub Δ Γ) →
      Π A B [ γ ]ᵀ ~ Π (A [ γ ]ᵀ) (B [ γ ↑ ]ᵀ)
    Π-[] A B γ = ~refl

    app : {Γ : Con i}
      {A : Ty Γ j} (B : Ty (Γ ▹ A) k) →
      Tm Γ (Π A B) → (a : Tm Γ A) → Tm Γ (B [ id , a ]ᵀ)
    ∣ app B t a ∣ γ = ∣ t ∣ γ (Yᵗ a γ)
    app B t a .rel γ = t .rel γ (Yᵗ a γ)

    app-[] : {Γ : Con i} {Δ : Con j}
      {A : Ty Γ k} (B : Ty (Γ ▹ A) l) →
      (t : Tm Γ (Π A B)) (a : Tm Γ A) (γ : Sub Δ Γ) →
      app B t a [ γ ]ᵗ ~
      app (B [ γ ↑ ]ᵀ) (t [ γ ]ᵗ) (a [ γ ]ᵗ)
    app-[] B t a γ = ~refl

    lam : {Γ : Con i} {A : Ty Γ j} {B : Ty (Γ ▹ A) k} → Tm (Γ ▹ A) B → Tm Γ (Π A B)
    ∣ lam b ∣ γ a = ∣ b ∣ (Y▹ γ a)
    lam b .rel γ a = b .rel (Y▹ γ a)

    lam-[] : {Γ : Con i} {Δ : Con j} {A : Ty Γ k} {B : Ty (Γ ▹ A) l}
             (b : Tm (Γ ▹ A) B) (γ : Sub Δ Γ) → lam b [ γ ]ᵗ ~ lam (b [ γ ↑ ]ᵗ)
    lam-[] b γ = ~refl

    Π-β : {Γ : Con i}
      {A : Ty Γ j} (B : Ty (Γ ▹ A) k) (b : Tm (Γ ▹ A) B) (a : Tm Γ A) →
      app B (lam b) a ~ b [ id , a ]ᵗ
    Π-β B b a = ~refl

    Π-η :
      {Γ : Con i} {A : Ty Γ j} (B : Ty (Γ ▹ A) k) (t : Tm Γ (Π A B)) →
      lam (app (B [ p ↑ ]ᵀ) (t [ p ]ᵗ) (q {A = A})) ~ t
    Π-η B t = ~refl

    -- This concludes the definition of the CwF of strict presheaves on Cₛ.
    -- Now we define the higher-order model in the CwF of strict presheaves by internalising the CwF structure on Cₛ.
    -}

  -- reorganising Cₛ.Ty as a strict presheaf
  CTy : Con lzero
  CTy =
    record {
      Γ = Cₛ.Ty ;
      rel = λ {x} γ → ∀{y}(f : Hom y x) → (γ Cₛ.id Cₛ.[ f ]T) ~ γ f
    }

  -- reorganising Cₛ.Tm as a dependent strict presheaf
  CTm : Ĉ.Ty CTy lzero
  CTm = record { A = λ {x} γ → Cₛ.Tm x (∣ γ ∣ Cₛ.id)
               ; rel = λ {x} γ α → ∀{y}(f : Hom y x) → (α Cₛ.id Cₛ.[ f ]t) ~ α f }

  -- the new sort of types in our final model
  Ty : Con i → Set i
  Ty Γ = Sub Γ CTy

  _[_]T : ∀{Γ : Con i} → Ty Γ → ∀{Δ : Con i} → Sub Δ Γ → Ty Δ
  A [ σ ]T = A ∘ σ

  [∘]T : ∀{Γ : Con i}{A : Ty Γ}{Δ : Con i}{σ : Sub Δ Γ}{Θ : Con i}{τ : Sub Θ Δ}
        → A [ σ ∘ τ ]T ~ A [ σ ]T [ τ ]T
  [∘]T = ~refl

  [id]T : ∀{Γ : Con i}{A : Ty Γ} → A [ id ]T ~ A
  [id]T = ~refl

  -- the new sort of terms in our final model
  Tm : (Γ : Con i) → Ty Γ → Set i
  Tm Γ A = Ĉ.Tm Γ (CTm Ĉ.[ A ]T)

  _[_]t : ∀{Γ : Con i}{A : Ty Γ} → Tm Γ A → ∀{Δ : Con i}(γ : Sub Δ Γ) → Tm Δ (A [ γ ]T)
  a [ γ ]t = a Ĉ.[ γ ]t

  [∘]t : ∀{Γ : Con i}{A : Ty Γ}{a : Tm Γ A}{Δ : Con i}{σ : Sub Δ Γ}{Θ : Con i}{τ : Sub Θ Δ}
        → _[_]t {A = A} a (σ ∘[ Γ ] τ) ~ _[_]t {A = A [ σ ]T} (_[_]t {A = A} a σ) τ
  [∘]t = ~refl

  [id]t : ∀{Γ : Con i}{A : Ty Γ}{a : Tm Γ A}
         → _[_]t {A = A} a id ~ a
  [id]t = ~refl

  _▹_ : (Γ : Con i)(A : Ty Γ) → Con i
  Γ ▹ A = Γ Ĉ.▹ (CTm Ĉ.[ A ]T)

  infixl  _,_
  _,_ : ∀{Γ Δ : Con i}(σ : Sub Δ Γ){A : Ty Γ} → Tm Δ (A [ σ ]T) → Sub Δ (Γ ▹ A)
  _,_ σ {A} a = Ĉ._,_ {A = CTm Ĉ.[ A ]T} σ a

  p : ∀{Γ : Con i}{A : Ty Γ} → Sub (Γ ▹ A) Γ
  p {A = A} = Ĉ.p {A = CTm Ĉ.[ A ]T}

  q : ∀{Γ : Con i}{A : Ty Γ} → Tm (Γ ▹ A) (A [ p {A = A} ]T)
  q {A = A} = Ĉ.q {A = CTm Ĉ.[ A ]T}

  ▹β₁ : ∀{Γ Δ : Con i}{γ : Sub Δ Γ}{A : Ty Γ}{a : Tm Δ (A [ γ ]T)}
       → p {A = A} ∘[ Γ ] (_,_ γ {A = A} a) ~ γ
  ▹β₁ = ~refl

  ▹β₂ : ∀{Γ Δ : Con i}{γ : Sub Δ Γ}{A : Ty Γ}{a : Tm Δ (A [ γ ]T)}
       → _[_]t {A = A [ p {A = A} ]T} (q {A = A}) (_,_ γ {A = A} a) ~ a
  ▹β₂ = ~refl

  ▹η : ∀{Γ : Con i}{Δ : Con i}{A : Ty Γ}{γa : Sub Δ (Γ ▹ A)}
        → (Ĉ._,[_]_ (p {A = A} ∘ γa) {A = CTm Ĉ.[ A ]T} {A' = CTm Ĉ.[ A ∘ (p {A = A}) ∘ γa ]T} ~refl
                  (_[_]t {A = A [ p {A = A} ]T} (q {A = A}) γa))
          ~ γa
  ▹η {Γ = Γ}{Δ = Δ}{A = A}{γa = γa} = cong (λ (x : Sub (Γ ▹ A) (Γ ▹ A)) → x ∘ γa) Ĉ.▹η

  mutual
    data Tel : Set where
      ◇ₜ : Tel
      _▹ₜ_ : (Γ : Tel) → Ty (El Γ) → Tel

    El : Tel → Con lzero
    El ◇ₜ = Ĉ.◇
    El (Γ ▹ₜ A) = (El Γ) ▹ A

  Cₛₛ : CwF {lzero}{lzero}{lzero}{lzero}
  Cₛₛ = record
         { Con = Tel
         ; Sub = λ Γ Δ → Sub (El Γ) (El Δ)
         ; _∘_ = λ {_} {_} γ {_} δ → γ ∘ δ
         ; ass = ~refl
         ; id = id
         ; idl = ~refl
         ; idr = ~refl
         ; ◇ = ◇ₜ
         ; ε = Ĉ.ε
         ; ◇η = ~refl
         ; Ty = λ Γ → Ty (El Γ)
         ; _[_]T = λ {_} A {_} γ → A [ γ ]T
         ; [∘]T = ~refl
         ; [id]T = ~refl
         ; Tm = λ Γ A → Tm (El Γ) A
         ; _[_]t = λ {_}{A} a {_} γ → _[_]t {A = A} a γ
         ; [∘]t = ~refl
         ; [id]t = ~refl
         ; _▹_ = λ Γ A → Γ ▹ₜ A
         ; _,[_]_ = λ {_}{Δ} γ {A}{A'} e a → γ Ĉ.,[ cong (λ (γ : Ty (El Δ)) → CTm Ĉ.[ γ ]T) e ] a
         ; p = λ {_}{A} → p {A = A}
         ; q = λ {_}{A} → q {A = A}
         ; ▹β₁ = ~refl
         ; ▹β₂ = ~refl
         ; ▹η = λ {_}{_}{A}{_} → ▹η {A = A} -- not reflexivity!
         }

  open CwF-tools Cₛₛ

  -- Counterparts of p, q, ↑ in the language of presheaves
  Cp : {Γ : Con i}(A : Ty Γ){x : Ob}(γ : Yᶜ Γ x) → Yᶜ Γ (x Cₛ.▹ ∣ A ∣ γ)
  Cp A γ = γ |ᶜ Cₛ.p

  Cq : {Γ : Con i}(A : Ty Γ){x : Ob}(γ : Yᶜ Γ x) → Ĉ.Yᵀ (CTm Ĉ.[ A ]T) (Cp A γ)
  Cq {Γ} A {x} γ =
    mkY
      (λ {y} f → coe (cong (Cₛ.Tm y) (Cₛ.[∘]T {γ = Cₛ.p} {δ = f} ⁻¹ ◼ A .rel γ (Cₛ.p Cₛ.∘ f))) (Cₛ.q Cₛ.[ f ]t))
      (λ {y} f {z} g → cong₂ (λ A a → Cₛ._[_]t {A = A} a g) (A .rel γ (Cₛ.p Cₛ.∘ f) ⁻¹ ◼ Cₛ.[∘]T {γ = Cₛ.p} {δ = f}) (coe≡-eq _ (Cₛ.q Cₛ.[ f ]t) ⁻¹)
                       ◼ Cₛ.[∘]t {γ = f} {δ = g} ⁻¹ ◼ coe≡-eq _ (Cₛ.q Cₛ.[ f Cₛ.∘ g ]t))

  C↑ : {Γ : Con i}(A : Ty Γ){x : Ob}(γ : Yᶜ Γ x) → Yᶜ (Γ ▹ A) (x Cₛ.▹ ∣ A ∣ γ)
  C↑ {Γ} A {x} γ = Ĉ.Y▹ (γ |ᶜ Cₛ.p) (Cq A γ)

  -- Some equations for Cp, Cq, C↑
  Cp-↑ : {Γ : Con i}(A : Ty Γ){x : Ob}(γ : Yᶜ Γ x){y : Ob}(f : Hom y x)
       → (Cp A γ) |ᶜ (Ct.↑ f) ~ Cp A (γ |ᶜ f)
  Cp-↑ {Γ} A {x} γ {y} f = cong₂ (λ y (f : Hom y x) → γ |ᶜ f) (cong (Cₛ._▹_ y) (A .rel γ f))
                                 (Ct.▹β₁-EX {e = Cₛ.[∘]T {γ = f} {δ = Cₛ.p}} ◼ cong (λ A → f Cₛ.∘ Cₛ.p {A = A}) (A .rel γ f))

  Cq-↑ : {Γ : Con i}(A : Ty Γ){x : Ob}(γ : Yᶜ Γ x){y : Ob}(f : Hom y x)
       → Ĉ.⟨ CTm Ĉ.[ A ]T , Cp A γ ⟩ (Cq A γ) |ᵀ (Ct.↑ f) ~ Cq A (γ |ᶜ f)
  Cq-↑ {Γ} A {x} γ {y} f =
    Ĉ.Yᵀ≡ (CTm Ĉ.[ A ]T) (cong (Cₛ._▹_ y) (A .rel γ f)) (Cp-↑ A γ f)
          (funexthᵢ λ {z} → funext λ {g₀} {g₁} gₑ →
            coe≡-eq _ (Cₛ.q Cₛ.[ Ct.↑ f Cₛ.∘ g₀ ]t) ⁻¹ ◼ Cₛ.[∘]t {γ = Ct.↑ f} {δ = g₀}
            ◼ cong₄ (λ x A a f → Cₛ._[_]t {x} {A} a f) (cong (Cₛ._▹_ y) (A .rel γ f)) e₂ e₁ gₑ ◼ coe≡-eq _ (Cₛ.q Cₛ.[ g₁ ]t))
    where
      e₁ : Cₛ.q {A = ∣ A ∣ γ} Cₛ.[ Ct.↑ f ]t ~ Cₛ.q {A = ∣ A ∣ (γ |ᶜ f)}
      e₁ = Ct.▹β₂-EX {γ = f Cₛ.∘ Cₛ.p} {e = Cₛ.[∘]T {γ = f} {δ = Cₛ.p}} ◼ cong (λ A → Cₛ.q {A = A}) (A .rel γ f)

      e₂ : ∣ A ∣ γ Cₛ.[ Cₛ.p ]T Cₛ.[ Ct.↑ f ]T ~ ∣ A ∣ (γ |ᶜ f) Cₛ.[ Cₛ.p ]T
      e₂ = Cₛ.[∘]T {γ = Cₛ.p} {δ = Ct.↑ f} ⁻¹ ◼ A .rel γ (Cₛ.p Cₛ.∘ (Ct.↑ f))
           ◼ cong₂ (λ x → ∣ A ∣ {x}) (cong (Cₛ._▹_ y) (A .rel γ f)) (Cp-↑ A γ f) ◼ A .rel (γ |ᶜ f) Cₛ.p ⁻¹

  C↑-↑ : {Γ : Con i}(A : Ty Γ){x : Ob}(γ : Yᶜ Γ x){y : Ob}(f : Hom y x)
       → (C↑ A γ) |ᶜ (Ct.↑ f) ~ C↑ A (γ |ᶜ f)
  C↑-↑ {Γ} A {x} γ {y} f = cong₃ (λ x → Ĉ.Y▹ {A = CTm Ĉ.[ A ]T} {x = x}) (cong (Cₛ._▹_ y) (A .rel γ f)) (Cp-↑ A γ f) (Cq-↑ A γ f)

  Cp-sg : {Γ : Con i}(A : Ty Γ)(a : Tm Γ A){x : Ob}(γ : Yᶜ Γ x)
       → (Cp A γ) |ᶜ (Ct.sg (Ĉ.∣ a ∣ γ)) ~ γ
  Cp-sg {Γ = Γ} A a {x} γ = cong (λ (f : Hom x x) → γ |ᶜ f) (Ct.▹β₁-EX {γ = Cₛ.id} {e = Cₛ.[id]T})

  Cq-sg : {Γ : Con i}(A : Ty Γ)(a : Tm Γ A){x : Ob}(γ : Yᶜ Γ x)
        → Ĉ.⟨ CTm Ĉ.[ A ]T , Cp A γ ⟩ (Cq A γ) |ᵀ (Ct.sg (Ĉ.∣ a ∣ γ)) ~ Ĉ.Yᵗ a γ
  Cq-sg {Γ = Γ} A a {x} γ =
    Ĉ.Yᵀ≡ (CTm Ĉ.[ A ]T) ~refl (Cp-sg A a γ)
          (funexthᵢᵣ λ {y} f → coe≡-eq _ (Cₛ.q Cₛ.[ Ct.sg (Ĉ.∣ a ∣ γ) Cₛ.∘ f ]t) ⁻¹ ◼ Cₛ.[∘]t {γ = Ct.sg (Ĉ.∣ a ∣ γ)} {δ = f}
                               ◼ cong₂ (λ A a → Cₛ._[_]t {A = A} a f) e (Ct.▹β₂-EX {γ = Cₛ.id} {e = Cₛ.[id]T}) ◼ a .Ĉ.rel γ f)
    where
      e : ∣ A ∣ γ Cₛ.[ Cₛ.p ]T Cₛ.[ Ct.sg (Ĉ.∣ a ∣ γ) ]T ~ ∣ A ∣ γ
      e = Cₛ.[∘]T {γ = Cₛ.p} {δ = Ct.sg (Ĉ.∣ a ∣ γ)} ⁻¹ ◼ A .rel γ (Cₛ.p Cₛ.∘ Ct.sg (Ĉ.∣ a ∣ γ)) ◼ cong ∣ A ∣ (Cp-sg A a γ)

  C↑-sg : {Γ : Con i}(A : Ty Γ)(a : Tm Γ A){x : Ob}(γ : Yᶜ Γ x)
         → (C↑ A γ) |ᶜ (Ct.sg (Ĉ.∣ a ∣ γ)) ~ Ĉ.Y▹ {A = CTm Ĉ.[ A ]T} γ (Ĉ.Yᵗ a γ)
  C↑-sg {Γ = Γ} A a {x} γ = cong₂ (Ĉ.Y▹ {A = CTm Ĉ.[ A ]T}) (Cp-sg A a γ) (Cq-sg A a γ)

  Cp-subExt : {Γ : Con i}(A : Ty Γ)(a : Tm Γ A){x : Ob}(γ : Yᶜ Γ x){y : Ob}(f : Hom y x)
            → (Cp A γ) |ᶜ (f Cₛ.,[ ~refl ] (Ĉ.∣ a ∣ γ Cₛ.[ f ]t)) ~ γ |ᶜ f
  Cp-subExt {Γ} A a {x} γ {y} f = cong (λ f → γ |ᶜ f) (Cₛ.▹β₁ {γ = f} {a = Ĉ.∣ a ∣ γ Cₛ.[ f ]t})

  -- Substituting equations in types and terms
  C↑-[↑]T : {Γ : Con i}(A : Ty Γ)(B : Ty (Γ ▹ A)){x : Ob}(γ : Yᶜ Γ x){y : Ob}(f : Hom y x)
         → ∣ B ∣ (C↑ A γ) Cₛ.[ Ct.↑ f ]T ~ ∣ B ∣ (C↑ A (γ |ᶜ f))
  C↑-[↑]T A B γ {y} f = B .rel (C↑ A γ) (Ct.↑ f) ◼ cong₂ (λ x → ∣ B ∣ {x}) (cong (Cₛ._▹_ y) (A .rel γ f)) (C↑-↑ A γ f)

  C↑-[↑]t : {Γ : Con i}(A : Ty Γ)(B : Ty (Γ ▹ A))(t : Tm (Γ ▹ A) B){x : Ob}(γ : Yᶜ Γ x){y : Ob}(f : Hom y x)
         → Ĉ.∣ t ∣ (C↑ A γ) Cₛ.[ Ct.↑ f ]t ~ Ĉ.∣ t ∣ (C↑ A (γ |ᶜ f))
  C↑-[↑]t A B t γ {y} f = t .Ĉ.rel (C↑ A γ) (Ct.↑ f) ◼ cong₂ (λ x → Ĉ.∣ t ∣ {x}) (cong (Cₛ._▹_ y) (A .rel γ f)) (C↑-↑ A γ f)

  C↑-[sg]T : {Γ : Con i}(A : Ty Γ)(a : Tm Γ A)(B : Ty (Γ ▹ A)){x : Ob}(γ : Yᶜ Γ x)
           → ∣ B ∣ (C↑ A γ) Cₛ.[ Ct.sg (Ĉ.∣ a ∣ γ) ]T ~ ∣ B [ Ĉ.sg a ]T ∣ γ
  C↑-[sg]T A a B γ = B .rel (C↑ A γ) (Ct.sg (Ĉ.∣ a ∣ γ)) ◼ cong ∣ B ∣ (C↑-sg A a γ)

  C↑-[sg]t : {Γ : Con i}(A : Ty Γ)(a : Tm Γ A)(B : Ty (Γ ▹ A))(t : Tm (Γ ▹ A) B){x : Ob}(γ : Yᶜ Γ x)
           → Ĉ.∣ t ∣ (C↑ A γ) Cₛ.[ Ct.sg (Ĉ.∣ a ∣ γ) ]t ~ Ĉ.∣ _[_]t {A = B} t (Ĉ.sg a) ∣ γ
  C↑-[sg]t A a B t γ = t .Ĉ.rel (C↑ A γ) (Ct.sg (Ĉ.∣ a ∣ γ)) ◼ cong Ĉ.∣ t ∣ (C↑-sg A a γ)

  -- Dependent products
  Π : ∀{Γ : Con i}(A : Ty Γ) → Ty (Γ ▹ A) → Ty Γ
  Π {Γ = Γ} A B =
    mkSub
      (λ {x} γ → Mₛ.Π (∣ A ∣ γ) (∣ B ∣ (C↑ A γ)))
      (λ {x} γ {y} f → Mₛ.Π[] {γ = f} ◼ cong₂ Mₛ.Π (A .rel γ f) (C↑-[↑]T A B γ f))

  lam : ∀{Γ : Con i}(A : Ty Γ){B : Ty (Γ ▹ A)}(t : Tm (Γ ▹ A) B) → Tm Γ (Π A B)
  lam {Γ = Γ} A {B} t =
    Ĉ.mkTm
      (λ {x} γ → Mₛ.lam (∣ A ∣ γ) {∣ B ∣ (C↑ A γ)} (Ĉ.∣ t ∣ (C↑ A γ)))
      (λ {x} γ {y} f → Mₛ.lam[] {γ = f} ◼ cong₃ (λ A B → Mₛ.lam A {B}) (A .rel γ f) (C↑-[↑]T A B γ f) (C↑-[↑]t A B t γ f))

  app : ∀{Γ : Con i}{A : Ty Γ}{B : Ty (Γ ▹ A)}(t : Tm Γ (Π A B))(u : Tm Γ A) → Tm Γ (B [ Ĉ.sg u ]T)
  app {Γ = Γ}{A}{B} t u =
    Ĉ.mkTm
      (λ {x} γ → coe (cong (Cₛ.Tm x) (C↑-[sg]T A u B γ))
                     (Mₛ.app {A = ∣ A ∣ γ}{B = ∣ B ∣ (C↑ A γ)} (Ĉ.∣ t ∣ γ) (Ĉ.∣ u ∣ γ)))
      (λ {x} γ {y} f → Ct.coe[]t (C↑-[sg]T A u B γ) (Mₛ.app (Ĉ.∣ t ∣ γ) (Ĉ.∣ u ∣ γ)) f
                        ◼ coe≡-eq _ (Mₛ.app (Ĉ.∣ t ∣ γ) (Ĉ.∣ u ∣ γ) Cₛ.[ f ]t) ⁻¹
                        ◼ Mₛ.app[] {γ = f}
                        ◼ cong₄ (λ A B → Mₛ.app {A = A} {B = B}) (A .rel γ f) (C↑-[↑]T A B γ f)
                                (coe≡-eq _ (Ĉ.∣ t ∣ γ Cₛ.[ f ]t) ⁻¹ ◼ t .Ĉ.rel γ f) (u .Ĉ.rel γ f)
                        ◼ coe≡-eq _ (Mₛ.app (Ĉ.∣ t ∣ (γ |ᶜ f)) (Ĉ.∣ u ∣ (γ |ᶜ f))))

  Πβ : ∀{Γ : Con i}{A : Ty Γ}{B : Ty (Γ ▹ A)}{t : Tm (Γ ▹ A) B}{a : Tm Γ A}
     → app {A = A}{B = B} (lam A {B} t) a ~ _[_]t {A = B} t (Ĉ.sg a)
  Πβ {Γ = Γ}{A}{B}{t}{a} = Ĉ.Tm≡ (funextHᵢᵣ λ {x} γ →
    coe≡-eq _ (Mₛ.app (Mₛ.lam (∣ A ∣ γ) (Ĉ.∣ t ∣ (C↑ A γ))) (Ĉ.∣ a ∣ γ)) ⁻¹ ◼ Mₛ.Πβ ◼ C↑-[sg]t A a B t γ)

  Πη : ∀{Γ : Con i}{A : Ty Γ}{B : Ty (Γ ▹ A)}{t : Tm Γ (Π A B)}
     → t ~ lam A {B = B [ Ĉ.↑ (p {A = A}) ]T [ Ĉ.sg (q {A = A}) ]T}
                 (app {A = A [ p {A = A} ]T} {B = B [ Ĉ.↑ (p {A = A}) ]T} (_[_]t {A = Π A B} t (p {A = A})) (q {A = A}))
  Πη {Γ = Γ}{A}{B}{t} = Ĉ.Tm≡ (funextHᵢᵣ λ {x} γ →
    Mₛ.Πη ◼ cong₂ (λ B → Mₛ.lam (∣ A ∣ γ){B = B}) (e₁ γ) (e₂ γ))
    where
      e₁ : {x : Ob} (γ : Yᶜ Γ x) → ∣ B ∣ (C↑ A γ) Cₛ.[ Ct.↑ Cₛ.p ]T Cₛ.[ Ct.sg Cₛ.q ]T ~ ∣ B ∣ (C↑ A γ)
      e₁ γ = Cₛ.[∘]T {γ = Ct.↑ Cₛ.p} {δ = Ct.sg Cₛ.q} ⁻¹ ◼ cong (λ f → ∣ B ∣ (C↑ A γ) Cₛ.[ f ]T) Ct.↑p-sgq ◼ Cₛ.[id]T

      e₂ : {x : Ob} (γ : Yᶜ Γ x) → Mₛ.app (coe (cong (Cₛ.Tm (x Cₛ.▹ ∣ A ∣ γ)) (Mₛ.Π[] {γ = Cₛ.p})) (Ĉ.∣ t ∣ γ Cₛ.[ Cₛ.p ]t)) Cₛ.q
                  ~ Ĉ.∣ app {A = A [ p {A = A} ]T} {B = B [ Ĉ.↑ (p {A = A}) ]T} (_[_]t {A = Π A B} t (p {A = A})) (q {A = A}) ∣ (C↑ A γ)
      e₂ γ = cong₄ (λ A B → Mₛ.app {A = A} {B = B}) (A .rel γ Cₛ.p) (C↑-[↑]T A B γ Cₛ.p)
                   (coe≡-eq _ (Ĉ.∣ t ∣ γ Cₛ.[ Cₛ.p {A = ∣ A ∣ γ} ]t) ⁻¹ ◼ t .Ĉ.rel γ Cₛ.p)
                   (Cₛ.[id]t ⁻¹ ◼ coe≡-eq _ (Cₛ.q {A = ∣ A ∣ γ} Cₛ.[ Cₛ.id ]t))
             ◼ coe≡-eq _ (Mₛ.app (Ĉ.∣ (_[_]t {A = Π A B} t (p {A = A})) ∣ (C↑ A γ)) (Ĉ.∣ (q {A = A}) ∣ (C↑ A γ)))

  -- Booleans with large elimination
  𝔹 : Ty Ĉ.◇
  𝔹 = mkSub
    (λ _ → Mₛ.𝔹 Cₛ.[ Cₛ.ε ]T)
    (λ f g → Ct.ε[]T {γ = g})

  𝕥 : Tm Ĉ.◇ 𝔹
  𝕥 = Ĉ.mkTm
    (λ _ → Mₛ.𝕥 Cₛ.[ Cₛ.ε ]t)
    (λ f g → Ct.ε[]t {γ = g})

  𝕗 : Tm Ĉ.◇ 𝔹
  𝕗 = Ĉ.mkTm
    (λ _ → Mₛ.𝕗 Cₛ.[ Cₛ.ε ]t)
    (λ f g → Ct.ε[]t {γ = g})

  ifᵀ : ∀{Γ} → Tm Γ (𝔹 [ Ĉ.ε ]T) → Ty Γ → Ty Γ → Ty Γ
  ifᵀ b A𝕥 A𝕗 =
    mkSub
      (λ γ → Mₛ.ifᵀ (Ĉ.∣ b ∣ γ) (∣ A𝕥 ∣ γ) (∣ A𝕗 ∣ γ))
      (λ γ f → Mₛ.ifᵀ[] {γ = f}
               ◼ cong₃ Mₛ.ifᵀ (coe≡-eq _ (Ĉ.∣ b ∣ γ Cₛ.[ f ]t) ⁻¹ ◼ b .Ĉ.rel γ f) (A𝕥 .rel γ f) (A𝕗 .rel γ f))

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

  ifᵀβ₁ : ∀{Γ}{A B : Ty Γ} → ifᵀ (_[_]t {A = 𝔹} 𝕥 Ĉ.ε) A B ~ A
  ifᵀβ₁ {Γ}{A}{B} = Sub≡ (funextHᵢᵣ λ {x} γ → Mₛ.ifᵀβ₁)

  ifᵀβ₂ : ∀{Γ}{A B : Ty Γ} → ifᵀ (_[_]t {A = 𝔹} 𝕗 Ĉ.ε) A B ~ B
  ifᵀβ₂ {Γ}{A}{B} = Sub≡ (funextHᵢᵣ λ {x} γ → Mₛ.ifᵀβ₂)

  ifᵗ : ∀{Γ} (P : Ty (Γ ▹ (𝔹 [ Ĉ.ε ]T))) (P𝕥 : Tm Γ (P [ Ĉ.sg (_[_]t {A = 𝔹} 𝕥 Ĉ.ε) ]T))
             (P𝕗 : Tm Γ (P [ Ĉ.sg (_[_]t {A = 𝔹} 𝕗 Ĉ.ε) ]T)) (b : Tm Γ (𝔹 [ Ĉ.ε ]T)) → Tm Γ (P [ Ĉ.sg b ]T)
  ifᵗ {Γ = Γ} P P𝕥 P𝕗 b =
    Ĉ.mkTm
      (λ {x} γ → coe (cong (Cₛ.Tm x) (C↑-[sg]T (𝔹 [ Ĉ.ε ]T) b P γ))
        (Mₛ.ifᵗ (∣ P ∣ (C↑ (𝔹 [ Ĉ.ε ]T) γ)) (coe (e𝕥 γ Cₛ.id) (Ĉ.∣ P𝕥 ∣ γ)) (coe (e𝕗 γ Cₛ.id) (Ĉ.∣ P𝕗 ∣ γ)) (Ĉ.∣ b ∣ γ)))
      (λ {x} γ {y} f → Ct.coe[]t (C↑-[sg]T (𝔹 [ Ĉ.ε ]T) b P γ) _ f
        ◼ coe≡-eq _ (Mₛ.ifᵗ (∣ P ∣ (C↑ (𝔹 [ Ĉ.ε ]T) γ)) (coe (e𝕥 γ Cₛ.id) (Ĉ.∣ P𝕥 ∣ γ)) (coe (e𝕗 γ Cₛ.id) (Ĉ.∣ P𝕗 ∣ γ)) (Ĉ.∣ b ∣ γ) Cₛ.[ f ]t) ⁻¹
        ◼ Mₛ.ifᵗ[] {γ = f}
        ◼ cong₄ Mₛ.ifᵗ
                (cong₂ (λ y (f : Hom y _) → ∣ P ∣ (C↑ (𝔹 [ Ĉ.ε ]T) γ) Cₛ.[ f ]T) (cong (Cₛ._▹_ y) (Ct.ε[]T {γ = f} ⁻¹)) (Ct.↑ε≡↑ f)
                  ◼ C↑-[↑]T (𝔹 [ Ĉ.ε ]T) P γ f)
                (coe≡-eq _ (coe (e𝕥 γ Cₛ.id) (Ĉ.∣ P𝕥 ∣ γ) Cₛ.[ f ]t) ⁻¹
                  ◼ Ct.coe[]t (C↑-[sg]T (𝔹 [ Ĉ.ε ]T) (_[_]t {A = 𝔹} 𝕥 Ĉ.ε) P γ ⁻¹) (Ĉ.∣ P𝕥 ∣ γ) f
                  ◼ coe≡-eq _ (Ĉ.∣ P𝕥 ∣ γ Cₛ.[ f ]t) ⁻¹ ◼ P𝕥 .Ĉ.rel γ f ◼ coe≡-eq _ (Ĉ.∣ P𝕥 ∣ (γ |ᶜ f)))
                (coe≡-eq _ (coe (e𝕗 γ Cₛ.id) (Ĉ.∣ P𝕗 ∣ γ) Cₛ.[ f ]t) ⁻¹
                  ◼ Ct.coe[]t (C↑-[sg]T (𝔹 [ Ĉ.ε ]T) (_[_]t {A = 𝔹} 𝕗 Ĉ.ε) P γ ⁻¹) (Ĉ.∣ P𝕗 ∣ γ) f
                  ◼ coe≡-eq _ (Ĉ.∣ P𝕗 ∣ γ Cₛ.[ f ]t) ⁻¹ ◼ P𝕗 .Ĉ.rel γ f ◼ coe≡-eq _ (Ĉ.∣ P𝕗 ∣ (γ |ᶜ f)))
                (coe≡-eq _ (Ĉ.∣ b ∣ γ Cₛ.[ f ]t) ⁻¹ ◼ b .Ĉ.rel γ f)
        ◼ coe≡-eq _ (Mₛ.ifᵗ (∣ P ∣ (C↑ (𝔹 [ Ĉ.ε ]T) (γ |ᶜ f))) (coe (e𝕥 γ f) (Ĉ.∣ P𝕥 ∣ (γ |ᶜ f)))
                           (coe (e𝕗 γ f) (Ĉ.∣ P𝕗 ∣ (γ |ᶜ f))) (Ĉ.∣ b ∣ (γ |ᶜ f))))
    where
      e𝕥 : {x : Ob} (γ : Yᶜ Γ x) {y : Ob} (f : Hom y x)
         → Cₛ.Tm y (∣ P [ Ĉ.sg (_[_]t {A = 𝔹} 𝕥 Ĉ.ε) ]T ∣ (γ |ᶜ f))
           ~ Cₛ.Tm y (∣ P ∣ (C↑ (𝔹 [ Ĉ.ε ]T) (γ |ᶜ f)) Cₛ.[ Ct.sg (Cₛ._[_]t {A = Mₛ.𝔹} Mₛ.𝕥 Cₛ.ε) ]T)
      e𝕥 {x} γ {y} f = cong (Cₛ.Tm y) (C↑-[sg]T (𝔹 [ Ĉ.ε ]T) (_[_]t {A = 𝔹} 𝕥 Ĉ.ε) P (γ |ᶜ f) ⁻¹)

      e𝕗 : {x : Ob} (γ : Yᶜ Γ x) {y : Ob} (f : Hom y x)
         → Cₛ.Tm y (∣ P [ Ĉ.sg (_[_]t {A = 𝔹} 𝕗 Ĉ.ε) ]T ∣ (γ |ᶜ f))
           ~ Cₛ.Tm y (∣ P ∣ (C↑ (𝔹 [ Ĉ.ε ]T) (γ |ᶜ f)) Cₛ.[ Ct.sg (Cₛ._[_]t {A = Mₛ.𝔹} Mₛ.𝕗 Cₛ.ε) ]T)
      e𝕗 {x} γ {y} f = cong (Cₛ.Tm y) (C↑-[sg]T (𝔹 [ Ĉ.ε ]T) (_[_]t {A = 𝔹} 𝕗 Ĉ.ε) P (γ |ᶜ f) ⁻¹)

  ifᵗβ₁ : ∀{Γ} {P : Ty (Γ ▹ (𝔹 [ Ĉ.ε ]T))} {P𝕥 : Tm Γ (P [ Ĉ.sg (_[_]t {A = 𝔹} 𝕥 Ĉ.ε) ]T)} {P𝕗 : Tm Γ (P [ Ĉ.sg (_[_]t {A = 𝔹} 𝕗 Ĉ.ε) ]T)}
        → ifᵗ P P𝕥 P𝕗 (_[_]t {A = 𝔹} 𝕥 Ĉ.ε) ~ P𝕥
  ifᵗβ₁ {Γ = Γ}{P}{P𝕥}{P𝕗} = Ĉ.Tm≡ (funextHᵢᵣ λ {x} γ →
    coe≡-eq _ (Mₛ.ifᵗ (∣ P ∣ (C↑ (𝔹 [ Ĉ.ε ]T) γ))
                     (coe (cong (Cₛ.Tm x) (C↑-[sg]T (𝔹 [ Ĉ.ε ]T) (_[_]t {A = 𝔹} 𝕥 Ĉ.ε) P γ ⁻¹)) (Ĉ.∣ P𝕥 ∣ γ))
                     (coe (cong (Cₛ.Tm x) (C↑-[sg]T (𝔹 [ Ĉ.ε ]T) (_[_]t {A = 𝔹} 𝕗 Ĉ.ε) P γ ⁻¹)) (Ĉ.∣ P𝕗 ∣ γ))
                     (Ĉ.∣ _[_]t {A = 𝔹} 𝕥 Ĉ.ε ∣ γ)) ⁻¹
    ◼ Mₛ.ifᵗβ₁ ◼ coe≡-eq _ (Ĉ.∣ P𝕥 ∣ γ) ⁻¹)

  ifᵗβ₂ : ∀{Γ} {P : Ty (Γ ▹ (𝔹 [ Ĉ.ε ]T))} {P𝕥 : Tm Γ (P [ Ĉ.sg (_[_]t {A = 𝔹} 𝕥 Ĉ.ε) ]T)} {P𝕗 : Tm Γ (P [ Ĉ.sg (_[_]t {A = 𝔹} 𝕗 Ĉ.ε) ]T)}
        → ifᵗ P P𝕥 P𝕗 (_[_]t {A = 𝔹} 𝕗 Ĉ.ε) ~ P𝕗
  ifᵗβ₂ {Γ = Γ}{P}{P𝕥}{P𝕗} = Ĉ.Tm≡ (funextHᵢᵣ λ {x} γ →
    coe≡-eq _ (Mₛ.ifᵗ (∣ P ∣ (C↑ (𝔹 [ Ĉ.ε ]T) γ))
                     (coe (cong (Cₛ.Tm x) (C↑-[sg]T (𝔹 [ Ĉ.ε ]T) (_[_]t {A = 𝔹} 𝕥 Ĉ.ε) P γ ⁻¹)) (Ĉ.∣ P𝕥 ∣ γ))
                     (coe (cong (Cₛ.Tm x) (C↑-[sg]T (𝔹 [ Ĉ.ε ]T) (_[_]t {A = 𝔹} 𝕗 Ĉ.ε) P γ ⁻¹)) (Ĉ.∣ P𝕗 ∣ γ))
                     (Ĉ.∣ _[_]t {A = 𝔹} 𝕗 Ĉ.ε ∣ γ)) ⁻¹
    ◼ Mₛ.ifᵗβ₂ ◼ coe≡-eq _ (Ĉ.∣ P𝕗 ∣ γ) ⁻¹)

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