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

module strictifyIso where

open import lib
open import model
open import initialObs
open import morphism
import strictifyCat
import strictifyCatMorphism
open import strictifyPMP
open import strictifyPMPMorphism

open str Ci Mi
open strictifyPMP→ Ci Mi
open initIte Cₛₛ Mₛₛ

-- In this file, we show that the strictified CwF is isomorphic to the original one

module strC = strictifyCat Ci Mi
module strC→ = strictifyCatMorphism Ci Mi

private module Ci = CwF Ci
private module Mi = Model Mi
private module Cₛ = CwF strC.Cₛ
private module Mₛ = Model strC.Mₛ
private module Cₛₛ = CwF Cₛₛ
private module Mₛₛ = Model Mₛₛ

-- Composing Cₛₛ→Cₛ and Cₛ→C

Sub→→ : (Γ Δ : Cₛₛ.Con) → Cₛₛ.Sub Δ Γ → Ci.Sub (Con→ Δ) (Con→ Γ)
Sub→→ Γ Δ γ = strC→.Sub→ (Sub→ {Γ}{Δ} γ)

Cₛₛ→Ci : CwF→ Cₛₛ Ci
Cₛₛ→Ci = Compose→.compCwF strC→.Cₛ→C strC→.Mₛ→M Cₛₛ→Cₛ Mₛₛ→Mₛ

Mₛₛ→Mi : Model→ Cₛₛ→Ci Mₛₛ Mi
Mₛₛ→Mi = Compose→.compModel strC→.Cₛ→C strC→.Mₛ→M Cₛₛ→Cₛ Mₛₛ→Mₛ

-- Now we want to prove that Cₛₛ→Cᵢ is an isomorphism, with an inverse given by the recursor Cᵢ
-- By initiality, there is only one morphism from Ci to Ci, so we get that Cₛₛ→Ci ∘ elim = Id

Ci→Cₛₛ→Ci : CwF→ Ci Ci
Ci→Cₛₛ→Ci = Compose→.compCwF Cₛₛ→Ci Mₛₛ→Mi iteCwF iteModel

Mi→Mₛₛ→Mi : Model→ Ci→Cₛₛ→Ci Mi Mi
Mi→Mₛₛ→Mi = Compose→.compModel Cₛₛ→Ci Mₛₛ→Mi iteCwF iteModel

Con-ret : (Γ : Ci.Con) → Con→ (iteCon Γ) ~ Γ
Con-ret Γ = initUniqueEndo.uniqueEndoCon Ci→Cₛₛ→Ci Mi→Mₛₛ→Mi Γ

Sub-ret : (Γ Δ : Ci.Con) (γ : Ci.Sub Δ Γ) → Sub→→ (iteCon Γ) (iteCon Δ) (iteSub γ) ~ γ
Sub-ret Γ Δ γ = initUniqueEndo.uniqueEndoSub Ci→Cₛₛ→Ci Mi→Mₛₛ→Mi γ

Ty-ret : (Γ : Ci.Con) (A : Ci.Ty Γ) → Ty→ (iteCon Γ) (iteTy A) ~ A
Ty-ret Γ A = initUniqueEndo.uniqueEndoTy Ci→Cₛₛ→Ci Mi→Mₛₛ→Mi A

Tm-ret : (Γ : Ci.Con) (A : Ci.Ty Γ) (a : Ci.Tm Γ A) → Tm→ (iteCon Γ) (iteTy A) (iteTm a) ~ a
Tm-ret Γ A a = initUniqueEndo.uniqueEndoTm Ci→Cₛₛ→Ci Mi→Mₛₛ→Mi a

-- Then, we use the properties of the Yoneda embedding to show that elim ∘ Cₛₛ→Ci = Id

-- We start by defining left inverses to the proof-relevant components of Cₛₛ→Ci
-- These left inverses satisfy respectively

-- Ty-inv ∘ Ty→ = id
-- Tm-inv ∘ Tm→ = id
-- Sub-inv ∘ Sub→→ = id

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

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

Tm-inv : (Γ : Cₛₛ.Con) (A : Cₛₛ.Ty Γ) → Ci.Tm (Con→ Γ) (Ty→ Γ A) → Cₛₛ.Tm Γ A
Tm-inv Γ A a = Ĉ.mkTm (λ {Δ} γ → coe (cong (Ci.Tm Δ) (e γ)) (a Cₛ.[ φfun Γ γ ]t))
                      (λ {Δ} γ {Θ} δ → CwF-tools.coe[]t Cₛ (e γ) (a Cₛ.[ φfun Γ γ ]t) δ
                                       ◼ coe-eq (cong (λ A → Cₛ.Tm Θ (A Cₛ.[ δ ]T)) (e γ)) ((a Cₛ.[ φfun Γ γ ]t) Cₛ.[ δ ]t) ⁻¹
                                       ◼ (Cₛ.[∘]t {γ = φfun Γ γ}{δ = δ} ⁻¹
                                       ◼ cong (Cₛ._[_]t a) (φfun→ Γ γ δ ⁻¹))
                                       ◼ coe-eq (cong (Cₛ.Tm Θ) (e (γ |ᶜ δ))) (a Cₛ.[ φfun Γ (γ |ᶜ δ) ]t))
  where
    e : ∀ {Δ} (γ : Yᶜ (El Γ) Δ) → Ty→ Γ A Cₛ.[ φfun Γ γ ]T ~ ∣ A ∣ γ
    e γ = A .rel (φinv Γ Cₛ.id) (φfun Γ γ) ◼ cong ∣ A ∣ (φinv→ Γ Cₛ.id (φfun Γ γ) ⁻¹ ◼ φret Γ γ)

Tm-inv-l : (Γ : Cₛₛ.Con) (A : Cₛₛ.Ty Γ) (a : Cₛₛ.Tm Γ A) → Tm-inv Γ A (Tm→ Γ A a) ~ a
Tm-inv-l Γ A a = Ĉ.Tm≡ (funextHᵢᵣ λ {Δ} γ → coe-eq (cong (Cₛ.Tm Δ) (e γ)) (Ĉ.∣ a ∣ (φinv Γ strC.id) Cₛ.[ φfun Γ γ ]t) ⁻¹
                                            ◼ Ĉ.rel a (φinv Γ strC.id) (φfun Γ γ)
                                            ◼ cong Ĉ.∣ a ∣ (φinv→ Γ Cₛ.id (φfun Γ γ) ⁻¹ ◼ φret Γ γ))
  where
    e : ∀ {Δ} (γ : Yᶜ (El Γ) Δ) → Ty→ Γ A Cₛ.[ φfun Γ γ ]T ~ ∣ A ∣ γ
    e γ = A .rel (φinv Γ Cₛ.id) (φfun Γ γ) ◼ cong ∣ A ∣ (φinv→ Γ Cₛ.id (φfun Γ γ) ⁻¹ ◼ φret Γ γ)

Sub-inv₁ : (Γ Δ : Cₛₛ.Con) → Cₛ.Sub (Con→ Δ) (Con→ Γ) → Cₛₛ.Sub Δ Γ
Sub-inv₁ Γ Δ γ = mkSub (λ δ → ∣ φinv Γ γ ∣ (φfun Δ δ))
                      (λ δ → coeₚ ((cong (El Γ .rel) (funextHᵢᵣ λ θ → cong ∣ φinv Γ γ ∣ (φfun→ Δ δ θ ⁻¹)))) (φinv Γ γ .rel (φfun Δ δ)))

Sub-inv₁-l : (Γ Δ : Cₛₛ.Con) (γ : Cₛₛ.Sub Δ Γ) → Sub-inv₁ Γ Δ (Sub→ {Γ}{Δ} γ) ~ γ
Sub-inv₁-l Γ Δ γ =
  let
    e₀ : ∀ {Θ} (δ : Yᶜ (El Δ) Θ) → φinv Γ (φfun Γ (Yˢ γ (φinv Δ Cₛ.id))) ~ Yˢ γ (φinv Δ Cₛ.id)
    e₀ δ = φret Γ (Yˢ γ (φinv Δ strC.id))

    e₁ : ∀ {Θ} (δ : Yᶜ (El Δ) Θ) → (φinv Δ Cₛ.id) |ᶜ φfun Δ δ ~ δ
    e₁ δ = φinv→ Δ Cₛ.id (φfun Δ δ) ⁻¹ ◼ φret Δ δ
  in Sub≡ (funextHᵢᵣ λ {Θ} δ → cong (λ x → ∣ x ∣ (φfun Δ δ)) (e₀ δ) ◼ cong ∣ γ ∣ (e₁ δ))

Sub-inv₂ : (Γ Δ : Cₛ.Con) → Ci.Sub Δ Γ → Cₛ.Sub Δ Γ
Sub-inv₂ Γ Δ γ = strC.mkSub (λ δ → γ Ci.∘ δ) Ci.ass

Sub-inv₂-l : (Γ Δ : Cₛ.Con) (γ : Cₛ.Sub Δ Γ) → Sub-inv₂ Γ Δ (strC→.Sub→ γ) ~ γ
Sub-inv₂-l Γ Δ γ = strC.∣_∣≡ (funextHᵢᵣ λ δ → γ .strC.Sub.nat ◼ cong (γ .strC.Sub.γ) Ci.idl)

Sub-inv : (Γ Δ : Cₛₛ.Con) → Ci.Sub (Con→ Δ) (Con→ Γ) → Cₛₛ.Sub Δ Γ
Sub-inv Γ Δ γ = Sub-inv₁ Γ Δ (Sub-inv₂ (Con→ Γ) (Con→ Δ) γ)

Sub-inv-l : (Γ Δ : Cₛₛ.Con) (γ : Cₛₛ.Sub Δ Γ) → Sub-inv Γ Δ (Sub→→ Γ Δ γ) ~ γ
Sub-inv-l Γ Δ γ = cong (Sub-inv₁ Γ Δ) (Sub-inv₂-l (Con→ Γ) (Con→ Δ) (Sub→ {Γ}{Δ} γ)) ◼ Sub-inv₁-l Γ Δ γ

-- Finally, we use a little trick to obtain the desired equalities. For instance, in the case of types it becomes:

-- elimTy ∘ Ty→
-- = (Ty-inv ∘ Ty→) ∘ elimTy ∘ Ty→
-- = Ty-inv ∘ (Ty→ ∘ elimTy) ∘ Ty→
-- = Ty-inv ∘ Ty→
-- = Id

mutual
  Ty-sec : (Γ : Cₛₛ.Con) (A : Cₛₛ.Ty Γ) → iteTy (Ty→ Γ A) ~ A
  Ty-sec Γ A = Ty-inv-l (iteCon (Con→ Γ)) (iteTy (Ty→ Γ A)) ⁻¹
               ◼ cong₂ Ty-inv (Con-sec Γ) (Ty-ret (Con→ Γ) (Ty→ Γ A))
               ◼ Ty-inv-l Γ A

  Con-sec : (Γ : Cₛₛ.Con) → iteCon (Con→ Γ) ~ Γ
  Con-sec ◇ₜ = ~refl
  Con-sec (Γ ▹ₜ A) = cong₂ _▹ₜ_ (Con-sec Γ) (Ty-sec Γ A)

Sub-sec : (Γ : Cₛₛ.Con) (Δ : Cₛₛ.Con) (γ : Cₛₛ.Sub Δ Γ) → iteSub (Sub→→ Γ Δ γ) ~ γ
Sub-sec Γ Δ γ = Sub-inv-l (iteCon (Con→ Γ)) (iteCon (Con→ Δ)) (iteSub (Sub→→ Γ Δ γ)) ⁻¹
                ◼ cong₃ Sub-inv (Con-sec Γ) (Con-sec Δ) (Sub-ret (Con→ Γ) (Con→ Δ) (Sub→→ Γ Δ γ))
                ◼ Sub-inv-l Γ Δ γ

Tm-sec : (Γ : Cₛₛ.Con) (A : Cₛₛ.Ty Γ) (a : Cₛₛ.Tm Γ A) → iteTm (Tm→ Γ A a) ~ a
Tm-sec Γ A a = Tm-inv-l (iteCon (Con→ Γ)) (iteTy (Ty→ Γ A)) (iteTm (Tm→ Γ A a)) ⁻¹
               ◼ cong₃ Tm-inv (Con-sec Γ) (Ty-sec Γ A) (Tm-ret (Con→ Γ) (Ty→ Γ A) (Tm→ Γ A a))
               ◼ Tm-inv-l Γ A a