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

module initialStrict where

open import lib
open import model
open import morphism
open import depModel
open import initialObs
import strictifyCat
open import strictifyPMP
open import strictifyPMPMorphism
import strictifyIso

-- In this file, we apply the strictification construction to the initial model

open str Ci Mi

-- strictified initial model
Ciₛₛ : CwF {lzero}{lzero}{lzero}{lzero}
Ciₛₛ = Cₛₛ

Miₛₛ : Model Ciₛₛ
Miₛₛ = Mₛₛ

module initElimₛₛ {i j k l : Level} (Cd : DepCwF {lzero}{i}{lzero}{j}{lzero}{k}{lzero}{l} Ciₛₛ)
                                    (Md : DepModel {lzero}{i}{lzero}{j}{lzero}{k}{lzero}{l} Ciₛₛ Cd Miₛₛ) where
  open initIte Ciₛₛ Miₛₛ
  open DepCwF Cd
  open DepModel Md
  open strictifyPMP→ Ci Mi
  open strictifyIso
  private module Cₛₛ = CwF Ciₛₛ
  private module Mₛₛ = Model Miₛₛ

  Cd' : DepCwF {lzero}{i}{lzero}{j}{lzero}{k}{lzero}{l} Ci
  Cd' =
    record
     { Con∙ = λ Γ → Con∙ (iteCon Γ)
     ; Sub∙ = λ Δ∙ Γ∙ γ → Sub∙ Δ∙ Γ∙ (iteSub γ)
     ; _∘∙_ = λ γ∙ δ∙ → γ∙ ∘∙ δ∙
     ; ass∙ = ass∙
     ; id∙ = id∙
     ; idl∙ = idl∙
     ; idr∙ = idr∙
     ; ◇∙ = ◇∙
     ; ε∙ = ε∙
     ; ◇η∙ = ◇η∙
     ; Ty∙ = λ Γ∙ A → Ty∙ Γ∙ (iteTy A)
     ; _[_]T∙ = λ A∙ γ∙ → A∙ [ γ∙ ]T∙
     ; [∘]T∙ = [∘]T∙
     ; [id]T∙ = [id]T∙
     ; Tm∙ = λ Γ∙ A∙ a → Tm∙ Γ∙ A∙ (iteTm a)
     ; _[_]t∙ = λ a∙ γ∙ → a∙ [ γ∙ ]t∙
     ; [∘]t∙ = [∘]t∙
     ; [id]t∙ = [id]t∙
     ; _▹∙_ = λ Γ∙ A∙ → Γ∙ ▹∙ A∙
     ; _,[_][_]∙_ = λ γ∙ e e∙ a∙ → γ∙ ,[ cong iteTy e ][ e∙ ]∙ a∙
     ; p∙ = p∙
     ; q∙ = q∙
     ; ▹β₁∙ = ▹β₁∙
     ; ▹β₂∙ = ▹β₂∙
     ; ▹η∙ = ▹η∙
     }

  Md' : DepModel {lzero}{i}{lzero}{j}{lzero}{k}{lzero}{l} Ci Cd' Mi
  Md' =
    record
     { Π∙ = λ A∙ B∙ → Π∙ A∙ B∙
     ; Π[]∙ = Π[]∙
     ; lam∙ = λ A∙ t∙ → lam∙ A∙ t∙
     ; lam[]∙ = lam[]∙
     ; app∙ = λ t∙ u∙ → app∙ t∙ u∙
     ; app[]∙ = app[]∙
     ; Πβ∙ = Πβ∙
     ; Πη∙ = Πη∙
     ; 𝔹∙ = 𝔹∙
     ; 𝕥∙ = 𝕥∙
     ; 𝕗∙ = 𝕗∙
     ; 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ᵗβ₁∙
     ; ifᵗβ₂∙ = ifᵗβ₂∙
     }

  open initElim Cd' Md'

  elimConₛₛ : (Γ : Cₛₛ.Con) → Con∙ Γ
  elimConₛₛ Γ = coe (cong Con∙ (Con-sec Γ)) (elimCon (Con→ Γ))

  elimSubₛₛ : ∀{Γ Δ}(γ : Cₛₛ.Sub Δ Γ) → Sub∙ (elimConₛₛ Δ) (elimConₛₛ Γ) γ
  elimSubₛₛ {Γ}{Δ} γ =
    coe (cong₅ (λ Δ Δ∙ Γ Γ∙ γ → Sub∙ {Δ} Δ∙ {Γ} Γ∙ γ)
               (Con-sec Δ)
               (coe≡-eq _ (elimCon (Con→ Δ)))
               (Con-sec Γ)
               (coe≡-eq _ (elimCon (Con→ Γ)))
               (Sub-sec Γ Δ γ))
        (elimSub {Con→ Δ}{Con→ Γ}(strictifyCat.Sub.γ (Sub→ {Γ}{Δ} γ) (CwF.id Ci)))

  elimTyₛₛ : ∀{Γ}(A : Cₛₛ.Ty Γ) → Ty∙ (elimConₛₛ Γ) A
  elimTyₛₛ {Γ} A =
    coe (cong₃ (λ Γ Γ∙ A → Ty∙ {Γ} Γ∙ A)
               (Con-sec Γ)
               (coe≡-eq _ (elimCon (Con→ Γ)))
               (Ty-sec Γ A))
        (elimTy (Ty→ Γ A))

  elimTmₛₛ : ∀{Γ}{A : Cₛₛ.Ty Γ}(a : Cₛₛ.Tm Γ A) → Tm∙ (elimConₛₛ Γ) (elimTyₛₛ A) a
  elimTmₛₛ {Γ}{A} a =
    coe (cong₅ (λ Γ Γ∙ A A∙ a → Tm∙ {Γ} Γ∙ {A} A∙ a)
               (Con-sec Γ)
               (coe≡-eq _ (elimCon (Con→ Γ)))
               (Ty-sec Γ A)
               (coe≡-eq _ (elimTy (Ty→ Γ A)))
               (Tm-sec Γ A a))
        (elimTm (Tm→ Γ A a))