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

module morphism where

open import lib
open import model

record CwF→ {i}{i'}{j}{j'}{k}{k'}{l}{l'} (C : CwF {i}{j}{k}{l}) (D : CwF {i'}{j'}{k'}{l'})
       : Set (i ⊔ j ⊔ k ⊔ l ⊔ i' ⊔ j' ⊔ k' ⊔ l') where
  module C = CwF C
  module D = CwF D
  field
    Con→ : C.Con → D.Con
    Sub→ : ∀ {Γ Δ} → C.Sub Δ Γ → D.Sub (Con→ Δ) (Con→ Γ)
    ∘→   : ∀ {Γ Δ} (γ : C.Sub Δ Γ) {Θ} (δ : C.Sub Θ Δ) → Sub→ (γ C.∘ δ) ~ (Sub→ γ) D.∘ (Sub→ δ)
    id→  : ∀ {Γ} → Sub→ (C.id {Γ = Γ}) ~ D.id {Γ = Con→ Γ}
    ◇→   : Con→ (C.◇) ~ D.◇
    ε→   : ∀ {Γ} → Sub→ (C.ε {Γ = Γ}) ~ D.ε {Γ = Con→ Γ}

    Ty→  : ∀ {Γ} → C.Ty Γ → D.Ty (Con→ Γ)
    [→]T : ∀ {Γ} (A : C.Ty Γ) {Δ} (γ : C.Sub Δ Γ) → Ty→ (A C.[ γ ]T) ~ (Ty→ A) D.[ Sub→ γ ]T

    Tm→  : ∀ {Γ A} → C.Tm Γ A → D.Tm (Con→ Γ) (Ty→ A)
    [→]t : ∀ {Γ} (A : C.Ty Γ) (a : C.Tm Γ A) {Δ} (γ : C.Sub Δ Γ) → Tm→ (a C.[ γ ]t) ~ (Tm→ a) D.[ Sub→ γ ]t

    ▹→   : ∀ {Γ A} → Con→ (Γ C.▹ A) ~ (Con→ Γ) D.▹ (Ty→ A)
    ,→   : ∀ {Γ Δ} (γ : C.Sub Δ Γ) {A A'} (e : A C.[ γ ]T ~ A') (a : C.Tm Δ A')
             → Sub→ (γ C.,[ e ] a) ~ (Sub→ γ) D.,[ [→]T A γ ⁻¹ ◼ cong Ty→ e ] (Tm→ a)
    p→   : ∀ {Γ} (A : C.Ty Γ) → Sub→ (C.p {A = A}) ~ D.p {A = Ty→ A}
    q→   : ∀ {Γ} (A : C.Ty Γ) → Tm→ (C.q {A = A}) ~ D.q {A = Ty→ A}

module Tools→ {i j k l i' j' k' l'}{C : CwF {i}{j}{k}{l}}{D : CwF {i'}{j'}{k'}{l'}} (F : CwF→ C D) where
  open CwF→ F
  open CwF-tools

  [ε]T→ : ∀ {Γ A A'} → (Ty→ A ~ A') → Ty→ (A C.[ C.ε {Γ = Γ} ]T) ~ A' D.[ D.ε {Γ = Con→ Γ} ]T
  [ε]T→ e = [→]T _ _ ◼ cong₄ (λ Γ Δ A (γ : D.Sub Δ Γ) → A D.[ γ ]T) ◇→ ~refl e ε→

  [ε]t→ : ∀ {Γ A A'} (eA : Ty→ A ~ A') {a : C.Tm C.◇ A} {a' : D.Tm D.◇ A'} → (Tm→ a ~ a')
          → Tm→ (a C.[ C.ε {Γ = Γ} ]t) ~ a' D.[ D.ε {Γ = Con→ Γ} ]t
  [ε]t→ eA ea = [→]t _ _ _ ◼ cong₄ (λ Γ A (a : D.Tm Γ A) (γ : D.Sub _ Γ) → a D.[ γ ]t) ◇→ eA ea ε→

  ▹ε→ : ∀ {Γ A A'} → (Ty→ A ~ A') → Con→ (Γ C.▹ A C.[ C.ε ]T) ~ (Con→ Γ) D.▹ (A' D.[ D.ε ]T)
  ▹ε→ e = ▹→ ◼ cong (D._▹_ (Con→ _)) ([ε]T→ e)

  sg→ : ∀ {Γ} {A : C.Ty Γ} {a : C.Tm Γ A} → Sub→ (sg C a) ~ sg D (Tm→ a)
  sg→ = ,→ _ C.[id]T _ ◼ cong-subExt D id→ ~refl (cong (D._[_]T (Ty→ _)) id→ ◼ D.[id]T) D.[id]T ~refl

  [sgε]T→ : ∀ {Γ A a} (P : C.Ty (Γ C.▹ A C.[ C.ε ]T)) {A'} (eA : Ty→ A ~ A') {a'} (ea : Tm→ a ~ a')
           → Ty→ (P C.[ sg C (a C.[ C.ε ]t) ]T) ~ coe (cong D.Ty (▹ε→ eA)) (Ty→ P) D.[ sg D (a' D.[ D.ε ]t) ]T
  [sgε]T→ P eA ea = [→]T _ _ ◼ cong₄ (λ Γ Δ A (γ : D.Sub Δ Γ) → D._[_]T A γ)
                                     (▹ε→ eA) ~refl
                                     (coe-eq (cong D.Ty (▹ε→ eA)) (Ty→ P))
                                     (sg→ ◼ cong₂ (λ A → sg D {A = A}) ([ε]T→ eA) ([ε]t→ eA ea))

record Model→ {i}{i'}{j}{j'}{k}{k'}{l}{l'}{C : CwF {i}{j}{k}{l}}{D : CwF {i'}{j'}{k'}{l'}} (F : CwF→ C D)
              (M : Model C) (N : Model D) : Set (i ⊔ j ⊔ k ⊔ l ⊔ i' ⊔ j' ⊔ k' ⊔ l') where
  module M = Model M
  module N = Model N
  open Tools→ F
  open CwF→ F
  field
    Π→   : ∀{Γ}{A : C.Ty Γ}{B : C.Ty (Γ C.▹ A)} → Ty→ (M.Π A B) ~ N.Π (Ty→ A) (coe (cong D.Ty ▹→) (Ty→ B))
    lam→ : ∀{Γ}{A : C.Ty Γ}{B : C.Ty (Γ C.▹ A)}{t : C.Tm (Γ C.▹ A) B}
           → Tm→ (M.lam A t) ~ N.lam (Ty→ A) (coe (cong₂ D.Tm ▹→ (coe-eq (cong D.Ty ▹→) (Ty→ B))) (Tm→ t))
    app→ : ∀{Γ}{A : C.Ty Γ}{B : C.Ty (Γ C.▹ A)}(t : C.Tm Γ (M.Π A B))(u : C.Tm Γ A)
           → Tm→ (M.app t u) ~ N.app (coe (cong (D.Tm _) Π→) (Tm→ t)) (Tm→ u)

    𝔹→   : Ty→ (M.𝔹) ~ N.𝔹
    𝕥→   : Tm→ (M.𝕥) ~ N.𝕥
    𝕗→   : Tm→ (M.𝕗) ~ N.𝕗
    ifᵀ→ : ∀ {Γ} b (A B : C.Ty Γ)
           → Ty→ (M.ifᵀ b A B) ~ N.ifᵀ (coe (cong (D.Tm _) ([ε]T→ 𝔹→)) (Tm→ b)) (Ty→ A) (Ty→ B)
    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) ~ N.ifᵗ (coe (cong D.Ty (▹ε→ 𝔹→)) (Ty→ P))
                                            (coe (cong (D.Tm _) ([sgε]T→ P 𝔹→ 𝕥→)) (Tm→ P𝕥))
                                            (coe (cong (D.Tm _) ([sgε]T→ P 𝔹→ 𝕗→)) (Tm→ P𝕗))
                                            (coe (cong (D.Tm _) ([ε]T→ 𝔹→)) (Tm→ b))

module Identity→ {i}{j}{k}{l} (C : CwF {i}{j}{k}{l}) (M : Model C) where
  idCwF : CwF→ C C
  idCwF = record
           { Con→ = λ Γ → Γ
           ; Sub→ = λ γ → γ
           ; ∘→ = λ γ δ → ~refl
           ; id→ = ~refl
           ; ◇→ = ~refl
           ; ε→ = ~refl
           ; Ty→ = λ A → A
           ; [→]T = λ A γ → ~refl
           ; Tm→ = λ a → a
           ; [→]t = λ A a γ → ~refl
           ; ▹→ = ~refl
           ; ,→ = λ γ e a → ~refl
           ; p→ = λ A → ~refl
           ; q→ = λ A → ~refl
           }

  idModel : Model→ idCwF M M
  idModel = record
             { Π→ = ~refl
             ; lam→ = ~refl
             ; app→ = λ t u → ~refl
             ; 𝔹→ = ~refl
             ; 𝕥→ = ~refl
             ; 𝕗→ = ~refl
             ; ifᵀ→ = λ b A B → ~refl
             ; ifᵗ→ = λ P P𝕥 P𝕗 b → ~refl
             }

module Compose→ {i i' i'' j j' j'' k k' k'' l l' l''}
                {C1 : CwF {i}{j}{k}{l}}{M1 : Model C1}{C2 : CwF {i'}{j'}{k'}{l'}}{M2 : Model C2}{C3 : CwF {i''}{j''}{k''}{l''}}{M3 : Model C3}
                (F1 : CwF→ C2 C1) (G1 : Model→ F1 M2 M1) (F2 : CwF→ C3 C2) (G2 : Model→ F2 M3 M2) where
  private module F1 = CwF→ F1
  private module F2 = CwF→ F2
  private module T1 = Tools→ F1
  private module T2 = Tools→ F2
  private module G1 = Model→ G1
  private module G2 = Model→ G2

  compCwF : CwF→ C3 C1
  compCwF = record
    { Con→ = λ Γ → F1.Con→ (F2.Con→ Γ)
    ; Sub→ = λ γ → F1.Sub→ (F2.Sub→ γ)
    ; ∘→ = λ γ δ → cong F1.Sub→ (F2.∘→ γ δ) ◼ F1.∘→ (F2.Sub→ γ) (F2.Sub→ δ)
    ; id→ = cong F1.Sub→ F2.id→ ◼ F1.id→
    ; ◇→ = cong F1.Con→ F2.◇→ ◼ F1.◇→
    ; ε→ = cong₂ (λ Γ → F1.Sub→ {Γ}) F2.◇→ F2.ε→ ◼ F1.ε→
    ; Ty→ = λ A → F1.Ty→ (F2.Ty→ A)
    ; [→]T = λ A γ → cong F1.Ty→ (F2.[→]T A γ) ◼ F1.[→]T (F2.Ty→ A) (F2.Sub→ γ)
    ; Tm→ = λ a → F1.Tm→ (F2.Tm→ a)
    ; [→]t = λ A a γ → cong₂ (λ A → F1.Tm→ {A = A}) (F2.[→]T A γ) (F2.[→]t A a γ) ◼ F1.[→]t (F2.Ty→ A) (F2.Tm→ a) (F2.Sub→ γ)
    ; ▹→ = cong F1.Con→ F2.▹→ ◼ F1.▹→
    ; ,→ = λ γ e a → cong₂ (λ Γ → F1.Sub→ {Γ = Γ}) F2.▹→ (F2.,→ γ e a) ◼ F1.,→ (F2.Sub→ γ) (F2.[→]T _ γ ⁻¹ ◼ cong F2.Ty→ e) (F2.Tm→ a)
    ; p→ = λ A → cong₂ (λ Γ → F1.Sub→ {Δ = Γ}) F2.▹→ (F2.p→ A) ◼ F1.p→ (F2.Ty→ A)
    ; q→ = λ A → cong₃ (λ Γ A → F1.Tm→ {Γ} {A}) F2.▹→
                       (F2.[→]T A F2.C.p ◼ cong₂ (λ Γ → F2.D._[_]T (F2.Ty→ A) {Δ = Γ}) F2.▹→ (F2.p→ A)) (F2.q→ A) ◼ F1.q→ (F2.Ty→ A)
    }

  private
    aux : {Γ : F2.C.Con} {Γ' : F2.D.Con} {Γ'' : F1.D.Con} (A : F2.C.Ty Γ)
           (e1 : F2.Con→ Γ ~ Γ') (e2 : F1.Con→ Γ' ~  Γ'') (e3 : F1.D.Ty (F1.Con→ (F2.Con→ Γ)) ≡ F1.D.Ty Γ'')
         → coe (cong F1.D.Ty e2) (F1.Ty→ (coe (cong F2.D.Ty e1) (F2.Ty→ A))) ~ coe≡ e3 (F1.Ty→ (F2.Ty→ A))
    aux A ~refl ~refl e3 = ~refl

    aux2 : {Γ : F2.C.Con} {A : F2.C.Ty Γ} {A' : F2.D.Ty (F2.Con→ Γ)} {A'' : F1.D.Ty (F1.Con→ (F2.Con→ Γ))} (t : F2.C.Tm Γ A)
           (e1 : F2.Ty→ A ~ A')(e2 : F1.Ty→ A' ~ A'')(e3 : F1.D.Tm (F1.Con→ (F2.Con→ Γ)) (F1.Ty→ (F2.Ty→ A)) ≡ F1.D.Tm (F1.Con→ (F2.Con→ Γ)) A'')
           → coe (cong₂ F1.D.Tm ~refl e2) (F1.Tm→ (coe (cong₂ F2.D.Tm ~refl e1) (F2.Tm→ t))) ~ coe≡ e3 (F1.Tm→ (F2.Tm→ t))
    aux2 t ~refl ~refl e3 = ~refl

    aux3 : {Γ : F2.C.Con} {Γ' : F2.D.Con} {Γ'' : F1.D.Con}
           {A : F2.C.Ty Γ} {A' : F2.D.Ty Γ'} {A'' : F1.D.Ty Γ''} (t : F2.C.Tm Γ A)
           (e1 : F2.Con→ Γ ~ Γ')(e2 : F1.Con→ Γ' ~  Γ'')(e3 : F2.Ty→ A ~ A')(e4 : F1.Ty→ A' ~ A'')
           → coe (cong₂ F1.D.Tm e2 e4) (F1.Tm→ (coe (cong₂ F2.D.Tm e1 e3) (F2.Tm→ t))) ~ F1.Tm→ (F2.Tm→ t)
    aux3 t ~refl ~refl ~refl ~refl = ~refl

  compModel : Model→ compCwF M3 M1
  compModel = record
    { Π→ = λ {Γ A B} → cong F1.Ty→ G2.Π→ ◼ G1.Π→
                     ◼ cong (G1.N.Π (F1.Ty→ (F2.Ty→ A)))
                            (coe≡-eq _ (F1.Ty→ (coe (cong F2.D.Ty (F2.▹→)) (F2.Ty→ B))) ⁻¹
                             ◼ cong₂ (λ Γ → F1.Ty→ {Γ}) (F2.▹→ ⁻¹) (coe≡-eq _ (F2.Ty→ B) ⁻¹)
                             ◼ coe≡-eq _ (F1.Ty→ (F2.Ty→ B)))
    ; lam→ = λ {Γ A B t} →
        cong₂ (λ A → F1.Tm→ {A = A}) (G2.Π→ ◼ cong (G2.N.Π (F2.Ty→ A)) (coe≡-eq₂ (F2.Ty→ B))) G2.lam→
        ◼ G1.lam→
        ◼ cong₃ (λ A B t → G1.N.lam A {B} t) ~refl
                (aux B F2.▹→ F1.▹→ _)
                (aux3 t F2.▹→ F1.▹→ (coe≡-eq _ (F2.Ty→ B)) (coe≡-eq _ (F1.Ty→ (coe≡ _ (F2.Ty→ B)))) ◼ coe≡-eq _ (F1.Tm→ (F2.Tm→ t)))
    ; app→ = λ {Γ A B} t u →
        cong₂ (λ A → F1.Tm→ {A = A})
              (F2.[→]T B _ ◼ cong₃ (λ Γ A γ → F2.D._[_]T {Γ} A γ) F2.▹→ (coe≡-eq _ (F2.Ty→ B)) T2.sg→)
              (G2.app→ t u)
        ◼ G1.app→ (coe≡ _ (F2.Tm→ t)) (F2.Tm→ u)
        ◼ cong₃ (λ B t u → G1.N.app {B = B} t u)
                (aux B F2.▹→ F1.▹→ _)
                (aux3 t ~refl ~refl G2.Π→ G1.Π→ ◼ coe≡-eq _ (F1.Tm→ (F2.Tm→ t)))
                ~refl
    ; 𝔹→ = cong₂ (λ Γ → F1.Ty→ {Γ}) F2.◇→ G2.𝔹→ ◼ G1.𝔹→
    ; 𝕥→ = cong₃ (λ Γ A → F1.Tm→ {Γ} {A}) F2.◇→ G2.𝔹→ G2.𝕥→ ◼ G1.𝕥→
    ; 𝕗→ = cong₃ (λ Γ A → F1.Tm→ {Γ} {A}) F2.◇→ G2.𝔹→ G2.𝕗→ ◼ G1.𝕗→
    ; ifᵀ→ = λ {Γ} b A B →
        cong F1.Ty→ (G2.ifᵀ→ b A B)
        ◼ G1.ifᵀ→ (coe≡ _ (F2.Tm→ b)) (F2.Ty→ A) (F2.Ty→ B)
        ◼ cong₃ G1.N.ifᵀ (aux2 b (T2.[ε]T→ G2.𝔹→) (T1.[ε]T→ G1.𝔹→) _) ~refl ~refl
    ; ifᵗ→ = λ {Γ} P P𝕥 P𝕗 b →
        let
          e = F2.[→]T (G2.M.𝔹) _ ◼ cong₃ (λ Γ A γ → F2.D._[_]T {Γ} A γ) F2.◇→ G2.𝔹→ F2.ε→
          e₂ = F2.▹→ ◼ cong (F2.D._▹_ (F2.Con→ Γ)) e
        in cong₂ (λ A → F1.Tm→ {A = A})
             (F2.[→]T P _ ◼ cong₃ (λ Γ A γ → F2.D._[_]T {Γ} A γ) e₂ (coe≡-eq _ (F2.Ty→ P))
                                  (F2.,→ F2.C.id _ b ◼ CwF-tools.cong-subExt-EX C2 ~refl ~refl F2.id→ e e _ _ (coe≡-eq _ (F2.Tm→ b))))
             (G2.ifᵗ→ P P𝕥 P𝕗 b)
           ◼ G1.ifᵗ→ (coe≡ _ (F2.Ty→ P)) (coe≡ _ (F2.Tm→ P𝕥)) (coe≡ _ (F2.Tm→ P𝕗)) (coe≡ _ (F2.Tm→ b))
           ◼ cong₄ G1.N.ifᵗ
                   (coe≡-eq _ (F1.Ty→ (coe≡ _ (F2.Ty→ P))) ⁻¹ ◼ cong₂ (λ Γ → F1.Ty→ {Γ}) (e₂ ⁻¹) (coe≡-eq _ (F2.Ty→ P) ⁻¹)
                    ◼ coe≡-eq _ (F1.Ty→ (F2.Ty→ P)))
                   (aux3 P𝕥 ~refl ~refl (T2.[sgε]T→ P G2.𝔹→ G2.𝕥→) (T1.[sgε]T→ (coe≡ _ (F2.Ty→ P)) G1.𝔹→ G1.𝕥→) ◼ coe≡-eq _ (F1.Tm→ (F2.Tm→ P𝕥)))
                   (aux3 P𝕗 ~refl ~refl (T2.[sgε]T→ P G2.𝔹→ G2.𝕗→) (T1.[sgε]T→ (coe≡ _ (F2.Ty→ P)) G1.𝔹→ G1.𝕗→) ◼ coe≡-eq _ (F1.Tm→ (F2.Tm→ P𝕗)))
                   (aux2 b (T2.[ε]T→ G2.𝔹→) (T1.[ε]T→ G1.𝔹→) _)
    }