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

open import lib
open import model
open import morphism

-- CwF morphism from the strictified CwF to the original one

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

open import strictifyCat C M
open Sub renaming (γ to ∣_∣)

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

Con→ : Cₛ.Con → C.Con
Con→ Γ = Γ

Sub→ : ∀ {Γ Δ} → Cₛ.Sub Δ Γ → C.Sub (Con→ Δ) (Con→ Γ)
Sub→ γ = ∣ γ ∣ C.id

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

Tm→ : ∀ {Γ A} → Cₛ.Tm Γ A → C.Tm (Con→ Γ) (Ty→ A)
Tm→ a = a

∘→ : ∀ {Γ Δ} (γ : Cₛ.Sub Δ Γ) {Θ} (δ : Cₛ.Sub Θ Δ) → Sub→ (γ Cₛ.∘ δ) ~ (Sub→ γ) C.∘ (Sub→ δ)
∘→ γ δ = cong ∣ γ ∣ (C.idl ⁻¹) ◼ (γ .nat {δ = C.id} {θ = ∣ δ ∣ C.id}) ⁻¹

,→ : ∀ {Γ Δ} (γ : Cₛ.Sub Δ Γ) {A A'} (e : A Cₛ.[ γ ]T ~ A') (a : Cₛ.Tm Δ A')
       → Sub→ (γ Cₛ.,[ e ] a) ~ (Sub→ γ) C.,[ cong Ty→ e ] (Tm→ a)
,→ γ e a = Ct.cong-subExt ~refl C.[id]T (e ◼ C.[id]T ⁻¹) e C.[id]t

p→ : ∀ {Γ} (A : Cₛ.Ty Γ) → Sub→ (Cₛ.p {A = A}) ~ C.p {A = Ty→ A}
p→ A = C.idr

q→ : ∀ {Γ} (A : Cₛ.Ty Γ) → Tm→ (Cₛ.q {A = A}) ~ C.q {A = Ty→ A}
q→ A = coe≡-eq _ C.q ⁻¹

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

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

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

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