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

module model where

open import lib

record CwF {i}{j}{k}{l} : Set (lsuc (i ⊔ j ⊔ k ⊔ l)) where
  infixl  _∘_
  infixl  _,[_]_
  infixl  _[_]T _[_]t
  infixl  _▹_

  -- Base CwF signature
  field
    Con      : Set i
    Sub      : Con → Con → Set j
    _∘_      : ∀{Γ Δ} → Sub Δ Γ → ∀{Θ} → Sub Θ Δ → Sub Θ Γ
    ass      : ∀{Γ Δ}{γ : Sub Δ Γ}{Θ}{δ : Sub Θ Δ}{Ξ}{θ : Sub Ξ Θ} → ((γ ∘ δ) ∘ θ) ~ (γ ∘ (δ ∘ θ))
    id       : ∀{Γ} → Sub Γ Γ
    idl      : ∀{Γ Δ}{γ : Sub Δ Γ} → (id ∘ γ) ~ γ
    idr      : ∀{Γ Δ}{γ : Sub Δ Γ} → (γ ∘ id) ~ γ
    ◇        : Con
    ε        : ∀{Γ} → Sub Γ ◇
    ◇η       : ∀{Γ}{σ : Sub Γ ◇} → σ ~ (ε {Γ})

    Ty       : Con → Set k
    _[_]T    : ∀{Γ} → Ty Γ → ∀{Δ} → Sub Δ Γ → Ty Δ
    [∘]T     : ∀{Γ}{A : Ty Γ}{Δ}{γ : Sub Δ Γ}{Θ}{δ : Sub Θ Δ} → A [ γ ∘ δ ]T ~ A [ γ ]T [ δ ]T
    [id]T    : ∀{Γ}{A : Ty Γ} → A [ id ]T ~ A

    Tm       : (Γ : Con) → Ty Γ → Set l
    _[_]t    : ∀{Γ}{A : Ty Γ} → Tm Γ A → ∀{Δ}(γ : Sub Δ Γ) → Tm Δ (A [ γ ]T)
    [∘]t     : ∀{Γ}{A : Ty Γ}{a : Tm Γ A}{Δ}{γ : Sub Δ Γ}{Θ}{δ : Sub Θ Δ} → a [ γ ∘ δ ]t ~ a [ γ ]t [ δ ]t
    [id]t    : ∀{Γ}{A : Ty Γ}{a : Tm Γ A} → a [ id ]t ~ a

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

module CwF-tools {i j k l : Level} (M : CwF {i}{j}{k}{l}) where
  open CwF M

  -- Proving two extended substitutions equal
  cong-subExt : ∀ {Γ}{Δ}{γ : Sub Δ Γ}{γ' : Sub Δ Γ} (γe : γ ~ γ')
                  {A}{B}{B'} (Be : B ~ B')
                  (e : A [ γ ]T ~ B) (e' : A [ γ' ]T ~ B')
                  {a}{a'} (ae : a ~ a')
                 → γ ,[ e ] a ~ γ' ,[ e' ] a'
  cong-subExt ~refl ~refl e e' ~refl = ~refl

  cong-subExt-EX : ∀ {Γ Γ' : Con}(Γe : Γ ~ Γ'){Δ Δ' : Con}(Δe : Δ ~ Δ')
                    {γ : Sub Δ Γ}{γ' : Sub Δ' Γ'}(γe : γ ~ γ')
                    {A A'}(Ae : A ~ A'){B B'}(Be : B ~ B')
                    (e : A [ γ ]T ~ B) (e' : A' [ γ' ]T ~ B')
                    {a a'}(ae : a ~ a')
                   → γ ,[ e ] a ~ γ' ,[ e' ] a'
  cong-subExt-EX ~refl ~refl ~refl ~refl ~refl e e' ~refl = ~refl

  -- β₁ but with arbitrary equalities
  ▹β₁-EX : ∀{Γ Δ}{γ : Sub Δ Γ}{A A'}{e : A [ γ ]T ~ A'}{a : Tm Δ A'} → p ∘ (γ ,[ e ] a) ~ γ
  ▹β₁-EX {Γ} {Δ} {γ} {A} {A'} {e} {a} =
    let
      a' = coe (cong (Tm Δ) (e ⁻¹)) a
      a≡a' = coe-eq (cong (Tm Δ) (e ⁻¹)) a
      e₀ : (γ ,[ e ] a) ~ (γ ,[ ~refl ] a')
      e₀ = cong-subExt ~refl (e ⁻¹) e ~refl a≡a'
    in (cong (λ x → p ∘ x) e₀) ◼ ▹β₁

  -- β₂ but with arbitrary equalities
  ▹β₂-EX : ∀{Γ Δ}{γ : Sub Δ Γ}{A A'}{e : A [ γ ]T ~ A'}{a : Tm Δ A'} → q [ γ ,[ e ] a ]t ~ a
  ▹β₂-EX {Γ} {Δ} {γ} {A} {A'} {e} {a} =
    let
      a' = coe (cong (Tm Δ) (e ⁻¹)) a
      a≡a' = coe-eq (cong (Tm Δ) (e ⁻¹)) a
      e₀ : (γ ,[ e ] a) ~ (γ ,[ ~refl ] a')
      e₀ = cong-subExt ~refl (e ⁻¹) e ~refl a≡a'
    in cong (λ x → q [ x ]t) e₀ ◼ ▹β₂ ◼ a≡a' ⁻¹

  -- composition with an extended substitution on the left (uses η)
  subExt∘ : ∀{Γ Δ Θ}(γ : Sub Δ Γ) → ∀ {A A'} → (e : A [ γ ]T ~ A') → (a : Tm Δ A') → (δ : Sub Θ Δ)
        → (γ ,[ e ] a) ∘ δ ~ (γ ∘ δ) ,[ [∘]T ◼ cong (λ A → A [ δ ]T) e ] a [ δ ]t
  subExt∘ {Γ} {Δ} {Θ} γ {A} {A'} e a δ =
    let
      e₀ : p ∘ ((γ ,[ e ] a) ∘ δ) ~ p ∘ (γ ∘ δ ,[ [∘]T ◼ cong (λ A → A [ δ ]T) e ] a [ δ ]t)
      e₀ = ass ⁻¹ ◼ cong (λ f → f ∘ δ) ▹β₁-EX ◼ (▹β₁-EX ⁻¹)
    in ▹η ⁻¹
      ◼ cong-subExt e₀ ([∘]T ⁻¹ ◼ cong (λ f → A [ f ]T) e₀ ◼ [∘]T) [∘]T [∘]T
                  ([∘]t ◼ cong₂ (λ C (b : Tm Δ C) → b [ δ ]t) ([∘]T ⁻¹ ◼ cong (λ f → A [ f ]T) ▹β₁-EX ◼ e) ▹β₂-EX ◼ (▹β₂-EX ⁻¹))
      ◼ ▹η

  -- substitution lift
  ↑ : ∀ {Γ} {A : Ty Γ} {Δ} → (γ : Sub Δ Γ) → (Sub (Δ ▹ A [ γ ]T) (Γ ▹ A))
  ↑ {Γ} {A} γ = γ ∘ p ,[ [∘]T ] q

  -- singleton substitution
  sg : ∀ {Γ} {A : Ty Γ} → Tm Γ A → Sub Γ (Γ ▹ A)
  sg a = id ,[ [id]T ] a

  ↑p-sgq : ∀ {Γ} {A : Ty Γ} → ↑ (p {A = A}) ∘ sg (q {A = A}) ~ id {Γ = Γ ▹ A}
  ↑p-sgq {Γ} {A} = subExt∘ (p ∘ p) [∘]T q (sg (q {A = A}))
    ◼ cong-subExt (ass ◼ cong (_∘_ p) ▹β₁-EX) ([∘]T ⁻¹ ◼ cong (_[_]T (A [ p ]T)) ▹β₁-EX)
                  ([∘]T ◼ cong (λ A → A [ sg q ]T) [∘]T) [∘]T (▹β₂-EX ◼ [id]t ⁻¹)
    ◼ ▹η

  -- commutation of sg and ↑ (uses η)
  ↑-sg : ∀ {Γ} {A : Ty Γ} (a : Tm Γ A) {Δ} (γ : Sub Δ Γ)
       → sg a ∘ γ ~ (↑ γ) ∘ sg (a [ γ ]t)
  ↑-sg {Γ} {A} a {Δ} γ =
    subExt∘ id _ a γ
    ◼ cong-subExt (idl ◼ idr ⁻¹ ◼ cong (_∘_ γ) (▹β₁-EX ⁻¹) ◼ ass ⁻¹)
                  ([id]T ⁻¹ ◼ cong (_[_]T (A [ γ ]T)) (▹β₁-EX ⁻¹) ◼ [∘]T)
                  (cong (_[_]T A) idl) ([∘]T ◼ cong (λ A → A [ sg (a [ γ ]t) ]T) [∘]T)
                  (▹β₂-EX ⁻¹)
    ◼ (subExt∘ (γ ∘ p) _ q (sg (a [ γ ]t))) ⁻¹

  ε[]T : ∀ {A : Ty ◇}{Γ}{Δ}{γ : Sub Δ Γ} → A [ ε ]T [ γ ]T ~ A [ ε ]T
  ε[]T {A} {Γ} {Δ} {γ} = ([∘]T ⁻¹) ◼ cong (_[_]T A) ◇η

  ε[]t : ∀ {A : Ty ◇}{a : Tm ◇ A}{Γ}{Δ}{γ : Sub Δ Γ} → a [ ε ]t [ γ ]t ~ a [ ε ]t
  ε[]t {A} {a} {Γ} {Δ} {γ} = ([∘]t ⁻¹) ◼ cong (_[_]t a) ◇η

  -- variation on ↑
  ↑ε : ∀ {Γ} {A : Ty ◇} {Δ} → (γ : Sub Δ Γ) → (Sub (Δ ▹ A [ ε ]T) (Γ ▹ A [ ε ]T))
  ↑ε {Γ} {A} {Δ} γ = γ ∘ p ,[ ε[]T ◼ ε[]T ⁻¹ ] q

  ↑ε≡↑ : ∀ {Γ} {A : Ty ◇} {Δ} (γ : Sub Δ Γ) → ↑ε {A = A} γ ~ ↑ {A = A [ ε ]T} γ
  ↑ε≡↑ {Γ} {A} {Δ} γ =
    congᵣᵣᵣᵢᵣ (λ a b c d e → _,[_]_ {Γ} {a} b {A [ ε ]T} {c} d e) (cong (_▹_ Δ) (ε[]T ⁻¹)) (cong (λ A → γ ∘ p {A = A}) (ε[]T ⁻¹))
              (cong (λ A → A [ p {A = A} ]T) (ε[]T ⁻¹)) (cong (λ A → q {A = A}) (ε[]T ⁻¹))

  -- commutation of ↑ε and sg (uses η)
  ↑ε-sg : ∀ {Γ} {A : Ty ◇} (a : Tm ◇ A) {Δ} (γ : Sub Δ Γ)
        → (sg (a [ ε ]t)) ∘ γ ~ (↑ε γ) ∘ (sg (a [ ε ]t))
  ↑ε-sg {Γ} {A} a {Δ} γ =
    subExt∘ id _ (a [ ε ]t) γ
    ◼ cong-subExt (idl ◼ idr ⁻¹ ◼ cong (_∘_ γ) (▹β₁-EX ⁻¹) ◼ ass ⁻¹)
                  (ε[]T ◼ (ε[]T ⁻¹) ◼ [∘]T)
                  (cong (_[_]T _) idl) ([∘]T ◼ cong (λ A → A [ sg (a [ ε ]t) ]T) (ε[]T ◼ ε[]T ⁻¹))
                  ([∘]t ⁻¹ ◼ cong (_[_]t a) ◇η ◼ (▹β₂-EX ⁻¹))
    ◼ (subExt∘ (γ ∘ p) _ q (sg (a [ ε ]t))) ⁻¹

  Ty-↑ε-sg : ∀ {Γ} {A : Ty ◇} (a : Tm ◇ A) (P : Ty (Γ ▹ A [ ε ]T)) {Δ} (γ : Sub Δ Γ)
           → P [ sg (a [ ε ]t) ]T [ γ ]T ~ P [ ↑ε γ ]T [ sg (a [ ε ]t) ]T
  Ty-↑ε-sg {Γ} {A} a P {Δ} γ = [∘]T ⁻¹ ◼ cong (_[_]T P) (↑ε-sg a γ) ◼ [∘]T

  -- substitution commutes with type coercion
  coe[]t : {Γ : Con} {A B : Ty Γ} (e : A ~ B) (t : Tm Γ A) {Δ : Con} (γ : Sub Δ Γ)
         → (coe (cong (Tm Γ) e) t) [ γ ]t ~ coe (cong (λ X → Tm Δ (X [ γ ]T)) e) (t [ γ ]t)
  coe[]t {Γ} {A} {.A} ~refl t {Δ} γ = ~refl

record Model {i}{j}{k}{l}(M : CwF {i}{j}{k}{l}) : Set (lsuc (i ⊔ j ⊔ k ⊔ l)) where
  open CwF M
  open CwF-tools M
  field
    Π        : ∀{Γ}(A : Ty Γ) → Ty (Γ ▹ A) → Ty Γ
    Π[]      : ∀{Γ}{A : Ty Γ}{B : Ty (Γ ▹ A)}{Δ}{γ : Sub Δ Γ} → (Π A B) [ γ ]T ~ Π (A [ γ ]T) (B [ ↑ γ ]T)

    lam      : ∀{Γ}(A : Ty Γ){B : Ty (Γ ▹ A)}(t : Tm (Γ ▹ A) B) → Tm Γ (Π A B)
    lam[]    : ∀{Γ}{A : Ty Γ}{B : Ty (Γ ▹ A)}{t : Tm (Γ ▹ A) B}{Δ}{γ : Sub Δ Γ} → (lam A t) [ γ ]t ~ lam (A [ γ ]T) (t [ ↑ γ ]t)

    app      : ∀{Γ}{A : Ty Γ}{B : Ty (Γ ▹ A)}(t : Tm Γ (Π A B))(u : Tm Γ A) → Tm Γ (B [ sg u ]T)
    app[]    : ∀{Γ}{A : Ty Γ}{B : Ty (Γ ▹ A)}{t : Tm Γ (Π A B)}{u : Tm Γ A}{Δ}{γ : Sub Δ Γ}
                → (app t u) [ γ ]t ~ app (coe (cong (Tm Δ) Π[]) (t [ γ ]t)) (u [ γ ]t)

    Πβ       : ∀{Γ}{A : Ty Γ}{B : Ty (Γ ▹ A)}{t : Tm (Γ ▹ A) B}{a : Tm Γ A} → app (lam A t) a ~ t [ sg a ]t
    Πη       : ∀{Γ}{A : Ty Γ}{B : Ty (Γ ▹ A)}{t : Tm Γ (Π A B)}
                → t ~ lam A {B = B [ ↑ p ]T [ sg q ]T} (app (coe (cong (Tm (Γ ▹ A)) Π[]) (t [ p ]t)) q)

    𝔹        : Ty ◇
    𝕥        : Tm ◇ 𝔹
    𝕗        : Tm ◇ 𝔹

    -- Large recursor
    ifᵀ      : ∀{Γ} → Tm Γ (𝔹 [ ε ]T) → Ty Γ → Ty Γ → Ty Γ
    ifᵀ[]    : ∀{Γ}{b : Tm Γ (𝔹 [ ε ]T)}{A B : Ty Γ}{Δ}{γ : Sub Δ Γ}
                → (ifᵀ b A B) [ γ ]T ~ ifᵀ (coe (cong (Tm Δ) ε[]T) (b [ γ ]t)) (A [ γ ]T) (B [ γ ]T)
    ifᵀβ₁    : ∀{Γ}{A B : Ty Γ} → ifᵀ (𝕥 [ ε ]t) A B ~ A
    ifᵀβ₂    : ∀{Γ}{A B : Ty Γ} → ifᵀ (𝕗 [ ε ]t) A B ~ B

    -- Small induction principle
    ifᵗ      : ∀{Γ} (P : Ty (Γ ▹ 𝔹 [ ε ]T)) (P𝕥 : Tm Γ (P [ sg (𝕥 [ ε ]t) ]T)) (P𝕗 : Tm Γ (P [ sg (𝕗 [ ε ]t) ]T))
               (b : Tm Γ (𝔹 [ ε ]T)) → Tm Γ (P [ sg b ]T)
    ifᵗ[]    : ∀{Γ} {P : Ty (Γ ▹ 𝔹 [ ε ]T)} {P𝕥 : Tm Γ (P [ sg (𝕥 [ ε ]t) ]T)} {P𝕗 : Tm Γ (P [ sg (𝕗 [ ε ]t) ]T)}
               {b : Tm Γ (𝔹 [ ε ]T)}{Δ}{γ : Sub Δ Γ}
               → (ifᵗ P P𝕥 P𝕗 b) [ γ ]t ~ ifᵗ (P [ ↑ε γ ]T) (coe (cong (Tm Δ) (Ty-↑ε-sg 𝕥 P γ)) (P𝕥 [ γ ]t))
                                              (coe (cong (Tm Δ) (Ty-↑ε-sg 𝕗 P γ)) (P𝕗 [ γ ]t)) (coe (cong (Tm Δ) ε[]T) (b [ γ ]t))
    ifᵗβ₁    : ∀{Γ} {P : Ty (Γ ▹ 𝔹 [ ε ]T)} {P𝕥 : Tm Γ (P [ sg (𝕥 [ ε ]t) ]T)} {P𝕗 : Tm Γ (P [ sg (𝕗 [ ε ]t) ]T)}
               → ifᵗ P P𝕥 P𝕗 (𝕥 [ ε ]t) ~ P𝕥
    ifᵗβ₂    : ∀{Γ} {P : Ty (Γ ▹ 𝔹 [ ε ]T)} {P𝕥 : Tm Γ (P [ sg (𝕥 [ ε ]t) ]T)} {P𝕗 : Tm Γ (P [ sg (𝕗 [ ε ]t) ]T)}
               → ifᵗ P P𝕥 P𝕗 (𝕗 [ ε ]t) ~ P𝕗