{-# OPTIONS --without-K #-}

module Model.Core where

open import lib
open import Agda.Primitive

open import Model.Decl

infixl 5 _▷_
infixl 7 _[_]T
infixl 5 _,_
infixr 6 _∘_
infixl 8 _[_]t

• : Con lzero
• = record
  { ∣_∣ = ⊤
  ; _~  = λ _ _ → ⊤
  ; ~p = refl
  }

_▷_ : ∀{i}(Γ : Con i){j} → Ty Γ j → Con (i ⊔ j)
_▷_ Γ A = record
  { ∣_∣ = Σ ∣ Γ ∣ ∣ A ∣
  ; _~ = λ { (γ ,Σ α)(γ' ,Σ α') → Σ ((Γ ~) γ γ') (λ z → (A ~) z α α') }
  ; ~p = ispropΣ1
    {D = ⊤ × (Σ ∣ Γ ∣ ∣ A ∣) × (Σ ∣ Γ ∣ ∣ A ∣)}
    {A = λ { (_ ,Σ (γ ,Σ _) ,Σ (γ' ,Σ _)) → (Γ ~) γ γ'}}
    {B = λ { (_ ,Σ (γ ,Σ α) ,Σ (γ' ,Σ α') ,Σ γ~) → (A ~) γ~ α α' }}
    (ap (λ { z (_ ,Σ (γ ,Σ _) ,Σ (γ' ,Σ _)) → z (_ ,Σ γ ,Σ γ') }) (~p Γ))
    (ap (λ { z (_ ,Σ (γ ,Σ α) ,Σ (γ' ,Σ α') ,Σ γ~) → z (_ ,Σ γ ,Σ γ' ,Σ γ~ ,Σ α ,Σ α') }) (~p A))
  ; R = λ { (γ ,Σ α) → R Γ γ ,Σ R A α }
  ; S = λ { (p ,Σ r) → S Γ p ,Σ S A r }
  ; T = λ { (p ,Σ r)(p' ,Σ r') → T Γ p p' ,Σ T A r r' }
  }

~p-deps[] : ∀{i}{Γ : Con i}{j}{∣_∣ : ∣ Γ ∣ → Set j}{k}{Δ : Con k}(γ : Tms Δ Γ) → ~p-deps Δ (λ δₓ → ∣_∣ (Tms.∣ γ ∣ δₓ)) → ~p-deps Γ ∣_∣
~p-deps[] γ (tt ,Σ δ₀ ,Σ δ₁ ,Σ δ₀₁ ,Σ a₀ ,Σ a₁) = (tt ,Σ ∣ γ ∣ δ₀ ,Σ ∣ γ ∣ δ₁ ,Σ (γ ~) δ₀₁ ,Σ a₀ ,Σ a₁)

_[_]T : ∀{i}{Γ : Con i}{j} → Ty Γ j → ∀{k}{Δ : Con k} → Tms Δ Γ → Ty Δ j
∣ _[_]T {Γ = Γ} A γ ∣ δₓ = ∣ A ∣ (∣ γ ∣ δₓ)
(_[_]T {Γ = Γ} A γ ~) δ₀₁ = (A ~) ((γ ~) δ₀₁)
~p (A [ γ ]T) = ap (λ z d → z (~p-deps[] γ d)) (~p A)
R (_[_]T {Γ = Γ} A γ) {δₓ} aₓ = transport (λ z → (A ~) z aₓ aₓ) (toProp1 (~p Γ) _ _) (R A aₓ)
S (_[_]T {Γ = Γ} A γ) {α = a₀}{a₁} a₀₁ = transport (λ z → (A ~) z a₁ a₀) (toProp1 (~p Γ) _ _) (S A a₀₁)
T (_[_]T {Γ = Γ} A γ) {α = a₀}{a₁}{a₂} a₀₁ a₁₂ = transport (λ z → (A ~) z a₀ a₂) (toProp1 (~p Γ) _ _) (T A a₀₁ a₁₂)
coeT (_[_]T {Γ = Γ} A γ) δ₀₁ a₀ = coeT A ((γ ~) δ₀₁) a₀ 
cohT (_[_]T {Γ = Γ} A γ) δ₀₁ a₀ = cohT A ((γ ~) δ₀₁) a₀ 

id : ∀{i}{Γ : Con i} → Tms Γ Γ
id = record
  { ∣_∣ = λ γ → γ
  ; _~  = λ p → p
  }

_∘_ : ∀{i}{Γ : Con i}{j}{Θ : Con j}{k}{Δ : Con k} → Tms Θ Δ → Tms Γ Θ → Tms Γ Δ
σ ∘ ν = record
  { ∣_∣ = λ γ → ∣ σ ∣ (∣ ν ∣ γ)
  ; _~  = λ p → (σ ~) ((ν ~) p)
  }

ε : ∀{i}{Γ : Con i} → Tms Γ •
ε = record
  { ∣_∣ = λ _ → tt
  }

_,_ : ∀{i}{Γ : Con i}{j}{Δ : Con j}(σ : Tms Γ Δ){b}{A : Ty Δ b} → Tm Γ (A [ σ ]T) → Tms Γ (Δ ▷ A)
σ , t = record { ∣_∣ = λ γ → ∣ σ ∣ γ ,Σ ∣ t ∣ γ ; _~ = λ p → (σ ~) p ,Σ (t ~) p }

π₁ : ∀{i}{Γ : Con i}{j}{Δ : Con j}{k}{A : Ty Δ k} → Tms Γ (Δ ▷ A) →  Tms Γ Δ
π₁ σ = record { ∣_∣ = λ γ → proj₁ (∣ σ ∣ γ) ; _~ = λ p → proj₁ ((σ ~) p) }

_[_]t : ∀{i}{Γ : Con i}{j}{Δ : Con j}{k}{A : Ty Δ k} → Tm Δ A → (σ : Tms Γ Δ) → Tm Γ (A [ σ ]T)
t [ σ ]t = record { ∣_∣ = λ γ → ∣ t ∣ (∣ σ ∣ γ) ; _~ = λ p → (t ~) ((σ ~) p) }

π₂ : ∀{i}{Γ : Con i}{j}{Δ : Con j}{k}{A : Ty Δ k}(σ : Tms Γ (Δ ▷ A)) → Tm Γ (A [ π₁ {A = A} σ ]T)
π₂ σ = record { ∣_∣ = λ γ → proj₂ (∣ σ ∣ γ) ; _~ = λ p → proj₂ ((σ ~) p) }

[id]T : ∀{i}{Γ : Con i}{j}{A : Ty Γ j} → A [ id ]T ≡ A
[][]T : ∀{i}{Γ : Con i}{j}{Θ : Con j}{k}{Δ : Con k}{l}{A : Ty Δ l}{σ : Tms Θ Δ}{δ : Tms Γ Θ} → (A [ σ ]T [ δ ]T) ≡ (A [ σ ∘ δ ]T)
idl   : ∀{i}{Γ : Con i}{j}{Δ : Con j}{δ : Tms Γ Δ} → (id ∘ δ) ≡ δ
idr   : ∀{i}{Γ : Con i}{j}{Δ : Con j}{δ : Tms Γ Δ} → (δ ∘ id) ≡ δ
ass   : ∀{i}{Γ : Con i}{j}{Θ : Con j}{k}{Ψ : Con k}{l}{Δ : Con l}{σ : Tms Ψ Δ}{δ : Tms Θ Ψ}{ν : Tms Γ Θ} →
  ((σ ∘ δ) ∘ ν) ≡ (σ ∘ (δ ∘ ν))
,∘    : ∀{i}{Γ : Con i}{j}{Θ : Con j}{k}{Δ : Con k}{σ : Tms Θ Δ}{δ : Tms Γ Θ}{l}{A : Ty Δ l}{t : Tm Θ (A [ σ ]T)} →
  (_,_ σ {A = A} t) ∘ δ ≡ _,_ (σ ∘ δ) {A = A} (transport (Tm Γ) ([][]T {A = A}{σ = σ}{δ}) (t [ δ ]t))
π₁β   : ∀{i}{Γ : Con i}{j}{Δ : Con j}{δ : Tms Γ Δ}{k}{A : Ty Δ k}{a : Tm Γ (A [ δ ]T)} → (π₁ {A = A}(_,_ δ {A = A} a)) ≡ δ
πη    : ∀{i}{Γ : Con i}{j}{Δ : Con j}{k}{A : Ty Δ k}{δ : Tms Γ (Δ ▷ A)} → (_,_ (π₁ {A = A} δ) {A = A} (π₂ {A = A} δ)) ≡ δ
εη    : ∀{i}{Γ : Con i}{σ : Tms Γ •} → σ ≡ ε
π₂β   : ∀{i}{Γ : Con i}{j}{Δ : Con j}{δ : Tms Γ Δ}{k}{A : Ty Δ k}{a : Tm Γ (A [ δ ]T)} → (π₂ {A = A}(_,_ δ {A = A} a)) ≡ a

[id]T {A = A} = Ty= (apid (~p A))
[][]T {A = A}{σ = σ}{δ = δ} = Ty= (apap (~p A) ⁻¹)
idl   = refl
idr   = refl
ass   = refl
,∘ {σ = σ}{δ}{A = A}{t} = Tms= (ap (λ z γ → ∣ σ ∣ (∣ δ ∣ γ) ,Σ z γ) (∣tr∣t (apap (~p A) ⁻¹) {t = t [ δ ]t}) ⁻¹)
π₁β   = refl
πη    = refl
εη    = refl
π₂β   = refl

wk : ∀{i}{Γ : Con i}{j}{A : Ty Γ j} → Tms (Γ ▷ A) Γ
wk {A = A} = π₁ {A = A} id

vz : ∀{i}{Γ : Con i}{j}{A : Ty Γ j} → Tm (Γ ▷ A) (A [ wk {A = A} ]T)
vz {A = A} = π₂ {A = A} id

vs : ∀{i}{Γ : Con i}{j}{A : Ty Γ j}{k}{B : Ty Γ k} → Tm Γ A → Tm (Γ ▷ B) (A [ wk {A = B} ]T)
vs {B = B} x = x [ wk {A = B} ]t

<_> : ∀{i}{Γ : Con i}{j}{A : Ty Γ j} → Tm Γ A → Tms Γ (Γ ▷ A)
∣ < t > ∣ γₓ = γₓ ,Σ ∣ t ∣ γₓ
(< t > ~) γ₀₁ = γ₀₁ ,Σ (t ~) γ₀₁

[id]T⁻¹ : ∀{i}{Γ : Con i}{j}{A : Ty Γ j} → A ≡ A [ id ]T
[id]T⁻¹ {A = A} = Ty= (apid (~p A) ⁻¹)

<>= : ∀{i}{Γ : Con i}{j}{A : Ty Γ j}{a : Tm Γ A} →
      <_> {i}{Γ}{j}{A} a ≡ _,_ id {A = A} (transport (Tm Γ) ([id]T⁻¹ {A = A}) a)
<>= {Γ = Γ} {A = A} {a = a} = Tms= (ap
    (λ ∣a∣ γₓ → γₓ ,Σ ∣a∣ γₓ)
    {a₀ = ∣ a ∣}
    {a₁ = ∣ transport (Tm Γ) ([id]T⁻¹) a ∣}
    (∣tr∣t (apid (~p A) ⁻¹) ⁻¹)
  )

infix 4 <_>

_^_ : ∀{i}{Γ : Con i}{j}{Δ : Con j}(δ : Tms Γ Δ){k}(A : Ty Δ k) → Tms (Γ ▷ A [ δ ]T) (Δ ▷ A)
∣ δ ^ A ∣   (γₓ ,Σ aₓ) = ∣ δ ∣ γₓ ,Σ aₓ
((δ ^ A) ~) (γ~ ,Σ a~) = (δ ~) γ~ ,Σ a~

infixl 5 _^_

^= : ∀{i}{Γ : Con i}{j}{Δ : Con j}{δ : Tms Γ Δ}{k}{A : Ty Δ k} →
  δ ^ A ≡ _,_ (δ ∘ wk {A = A [ δ ]T}) {A = A} (transport (Tm (Γ ▷ A [ δ ]T)) ([][]T {A = A}{σ = δ}{δ = wk {Γ = Γ}{A = A [ δ ]T}}) (vz {A = A [ δ ]T}))
^= {Γ = Γ}{Δ = Δ}{δ}{A = A} = Tms=
  (ap
    (λ (z : (γaₓ : ∣ Γ ▷ A [ δ ]T ∣) → ∣ A ∣ (∣ δ ∣ (proj₁ γaₓ))) → λ { (γₓ ,Σ aₓ) → ∣ δ ∣ γₓ ,Σ z (γₓ ,Σ aₓ) })
    {a₀ = λ { (γₓ ,Σ aₓ) → aₓ}}
    {a₁ = ∣ transport (Tm (Γ ▷ A [ δ ]T)) ([][]T {A = A}{σ = δ}{δ = wk {A = A [ δ ]T}}) vz ∣}
    (∣tr∣t (apap (~p A) ⁻¹) {t = vz {A = A [ δ ]T}} ⁻¹))

lem : ∀{i}{Γ : Con i}{j}{A : Ty Γ j}{k}{B : Ty (Γ ▷ A) k}{l}{Δ : Con l}{γ : Tms Δ Γ} →
-- (λ δₓ aₓ → ∣ B ∣ (∣ γ ^ A ∣ (δₓ ,Σ aₓ))) ≡ (λ δₓ aₓ → ∣ B ∣ (∣ γ ∣ δₓ ,Σ aₓ))
-- (λ δₓ aₓ → ∣ B ∣ (∣ γ ∣ δₓ ,Σ ∣ (transport (Tm (Δ ▷ A [ γ ]T)) ([][]T {A = A}{σ = γ}{δ = wk {Γ = Δ}{A = A [ γ ]T}}) (vz {A = A [ γ ]T})) ∣ (δₓ ,Σ aₓ))) ≡ (λ δₓ aₓ → ∣ B ∣ (∣ γ ∣ δₓ ,Σ aₓ))
   (λ δₓ aₓ → ∣ B ∣ (∣ γ ∣ δₓ ,Σ ∣ transport (Tm (Δ ▷ A [ γ ]T))
                                             {A [ γ ]T [ wk {Γ = Δ}{A = A [ γ ]T} ]T}
                                             {A [ γ ∘ wk {Γ = Δ}{A = A [ γ ]T} ]T}
                                             (Ty= (apap (~p A) ⁻¹))
                                             (vz {A = A [ γ ]T})
                                 ∣ (δₓ ,Σ aₓ))) ≡
   (λ δₓ aₓ → ∣ B ∣ (∣ γ ∣ δₓ ,Σ aₓ))
-- [][]T {A = A}{σ = σ}{δ = δ} = Ty= (apap (~p A) ⁻¹)
lem {Γ = Γ}{A = A}{B = B}{Δ = Δ}{γ} = ap
  (λ z → λ δₓ aₓ → ∣ B ∣ (∣ γ ∣ δₓ ,Σ z (δₓ ,Σ aₓ)))
  (∣tr∣t {~p₀ = ~p (A [ γ ]T [ wk {Γ = Δ}{A = A [ γ ]T} ]T)}{~p (A [ γ ∘ wk {Γ = Δ}{A = A [ γ ]T} ]T)}(apap (~p A) ⁻¹) {t = π₂ id})