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

module canon where

open import lib
open import model
open import depModel
import strictifyPMP
open import initialStrict

-- In this file, we prove boolean canonicity for dependent type theory
-- The proof is short and elegant!

Ci = Ciₛₛ
Mi = Miₛₛ
module Ct = CwF-tools Ci

open CwF Ci
open Model Mi

data Canon𝔹 (b : Tm ◇ 𝔹) : Set where
  canon-𝕥 : (b ~ 𝕥) → Canon𝔹 b
  canon-𝕗 : (b ~ 𝕗) → Canon𝔹 b

cong-canon-𝕥 : ∀ (b₁ b₂ : Tm ◇ 𝔹) (e : b₁ ~ b₂) (e₁ : b₁ ~ 𝕥) (e₂ : b₂ ~ 𝕥) → canon-𝕥 {b₁} e₁ ~ canon-𝕥 {b₂} e₂
cong-canon-𝕥 b₁ b₂ ~refl e₁ e₂ = ~refl

cong-canon-𝕗 : ∀ (b₁ b₂ : Tm ◇ 𝔹) (e : b₁ ~ b₂) (e₁ : b₁ ~ 𝕗) (e₂ : b₂ ~ 𝕗) → canon-𝕗 {b₁} e₁ ~ canon-𝕗 {b₂} e₂
cong-canon-𝕗 b₁ b₂ ~refl e₁ e₂ = ~refl

CanonIfT : (b : Tm ◇ 𝔹) (b∙ : Canon𝔹 b) (A : Ty ◇) (A∙ : Tm ◇ A → Set) (B : Ty ◇) (B∙ : Tm ◇ B → Set) (t : Tm ◇ (ifᵀ {◇} b A B)) → Set
CanonIfT b (canon-𝕥 Hb) A A∙ B B∙ t = A∙ (coe (cong (Tm ◇) (cong (λ b → ifᵀ {◇} b A B) Hb ◼ ifᵀβ₁ {◇}{A}{B})) t)
CanonIfT b (canon-𝕗 Hb) A A∙ B B∙ t = B∙ (coe (cong (Tm ◇) (cong (λ b → ifᵀ {◇} b A B) Hb ◼ ifᵀβ₂ {◇}{A}{B})) t)

CanonIfᵗ : (P : Ty (◇ ▹ 𝔹))
           (P∙ : (b : Tm ◇ 𝔹) (b∙ : Canon𝔹 b) → Tm ◇ (_[_]T {◇ ▹ 𝔹} P {◇} (Ct.sg {◇}{𝔹} b)) → Set)
           (P𝕥 : Tm ◇ (_[_]T {◇ ▹ 𝔹} P {◇} (Ct.sg {◇}{𝔹} 𝕥)))
           (P𝕥∙ : P∙ 𝕥 (canon-𝕥 ~refl) P𝕥)
           (P𝕗 : Tm ◇ (_[_]T {◇ ▹ 𝔹} P {◇} (Ct.sg {◇}{𝔹} 𝕗)))
           (P𝕗∙ : P∙ 𝕗 (canon-𝕗 ~refl) P𝕗)
           (b : Tm ◇ 𝔹) (b∙ : Canon𝔹 b)
           → P∙ b b∙ (ifᵗ {◇} P P𝕥 P𝕗 b)
CanonIfᵗ P P∙ P𝕥 P𝕥∙ P𝕗 P𝕗∙ b (canon-𝕥 Hb) =
  coe ((cong₃ P∙ (Hb ⁻¹) (cong-canon-𝕥 𝕥 b (Hb ⁻¹) ~refl Hb) ((ifᵗβ₁ {◇}{P}{P𝕥}{P𝕗} ⁻¹ ◼ cong (ifᵗ {◇} P P𝕥 P𝕗) Hb ⁻¹)))) P𝕥∙
CanonIfᵗ P P∙ P𝕥 P𝕥∙ P𝕗 P𝕗∙ b (canon-𝕗 Hb) =
  coe ((cong₃ P∙ (Hb ⁻¹) (cong-canon-𝕗 𝕗 b (Hb ⁻¹) ~refl Hb) ((ifᵗβ₂ {◇}{P}{P𝕥}{P𝕗} ⁻¹ ◼ cong (ifᵗ {◇} P P𝕥 P𝕗) Hb ⁻¹)))) P𝕗∙

CanonCwF : DepCwF Ci
CanonCwF = record
   { Con∙ = λ Γ → (Sub ◇ Γ → Set)
   ; Sub∙ = λ {Δ} Δ∙ {Γ} Γ∙ σ → (δ : Sub ◇ Δ) (δ∙ : Δ∙ δ) → Γ∙ (_∘_ {Γ}{Δ} σ {◇} δ)
   ; _∘∙_ = λ {Γ Γ∙ Δ Δ∙ σ} σ∙ {Θ Θ∙ τ} τ∙ γ γ∙ → σ∙ (_∘_ {Δ}{Θ} τ {◇} γ) (τ∙ γ γ∙)
   ; ass∙ = ~refl
   ; id∙ = λ {Γ Γ∙} δ δ∙ → δ∙
   ; idl∙ = ~refl
   ; idr∙ = ~refl
   ; ◇∙ = λ _ → ⊤
   ; ε∙ = λ _ _ → tt
   ; ◇η∙ = ~refl
   ; Ty∙ = λ {Γ} Γ∙ A → (γ : Sub ◇ Γ) (γ∙ : Γ∙ γ) (a : Tm ◇ (_[_]T {Γ} A {◇} γ)) → Set
   ; _[_]T∙ = λ {Γ Γ∙ A} A∙ {Δ Δ∙ σ} σ∙ δ δ∙ a → A∙ (_∘_ {Γ}{Δ} σ {◇} δ) (σ∙ δ δ∙) a
   ; [∘]T∙ = ~refl
   ; [id]T∙ = ~refl
   ; Tm∙ = λ {Γ} Γ∙ {A} A∙ a → (γ : Sub ◇ Γ) (γ∙ : Γ∙ γ) → A∙ γ γ∙ (_[_]t {Γ} {A} a {◇} γ)
   ; _[_]t∙ = λ {Γ Γ∙ A A∙ a} a∙ {Δ Δ∙ σ} σ∙ δ δ∙ → a∙ (_∘_ {Γ}{Δ} σ {◇} δ) (σ∙ δ δ∙)
   ; [∘]t∙ = ~refl
   ; [id]t∙ = ~refl
   ; _▹∙_ = λ {Γ} Γ∙ {A} A∙ γa → Σ (Γ∙ (_∘_ {Γ}{Γ ▹ A} (p {Γ}{A}) {◇} γa))
                                   (λ γ∙ → A∙ _ γ∙ (_[_]t {Γ ▹ A}{_[_]T {Γ} A {Γ ▹ A} (p {Γ}{A})} (q {Γ}{A}) {◇} γa))
   ; _,[_][_]∙_ = λ {Γ Γ∙ Δ Δ∙ σ} σ∙ {A A∙ A' A'∙} e e∙ {a} a∙ δ δ∙ →
     let H = ~cong (~cong (~cong e∙ (~refl {a = δ})) (~refl {a = δ∙}))
                   (Ct.▹β₂-EX {Γ}{◇}{_∘_ {Γ}{Δ} σ {◇} δ}{A}{_[_]T {Δ} A' {◇} δ}{cong (λ A → _[_]T {Δ} A {◇} δ) e}{_[_]t {Δ} {A'} a {◇} δ})
     in (σ∙ δ δ∙) ,Σ coe (H ⁻¹) (a∙ δ δ∙)
   ; p∙ = λ {Γ Γ∙ A A∙} γa γa∙ → π₁ γa∙
   ; q∙ = λ {Γ Γ∙ A A∙} γa γa∙ → π₂ γa∙
   ; ▹β₁∙ = ~refl
   ; ▹β₂∙ = ~refl
   ; ▹η∙ = ~refl
   }

open DepCwF CanonCwF
module dCt = DepCwF-tools Ci CanonCwF

CanonModel : DepModel Ci CanonCwF Mi
CanonModel = record
   { Π∙ = λ {Γ Γ∙ A} A∙ {B} B∙ γ γ∙ f → (a : Tm ◇ (_[_]T {Γ} A {◇} γ)) (a∙ : A∙ γ γ∙ a) →
            let
              A[γ] = _[_]T {Γ} A {◇} γ
              A[γ]∙ = _[_]T∙ {Γ}{Γ∙}{A} A∙ {◇}{◇∙}{γ} (λ _ _ → γ∙)
              γ↑ = Ct.↑ {Γ}{A}{◇} γ
              γ↑∙ = dCt.↑∙ {Γ}{Γ∙}{A}{A∙}{◇}{◇∙}{γ} (λ _ _ → γ∙)
              B[γ↑] = _[_]T {Γ ▹ A} B {◇ ▹ A[γ]} γ↑
              B[γ↑]∙ = _[_]T∙ {Γ ▹ A}{_▹∙_ {Γ} Γ∙ {A} A∙}{B} B∙ {◇ ▹ A[γ]}{_▹∙_ {◇} ◇∙ {A[γ]} A[γ]∙}{γ↑} γ↑∙
              sg-a = Ct.sg {◇}{A[γ]} a
              sg-a∙ = dCt.sg∙ {◇}{◇∙}{A[γ]}{A[γ]∙}{a} (λ _ _ → a∙)
              fa = app {◇}{A[γ]}{B[γ↑]} f a
            in B∙ (_∘_ {Γ ▹ A}{◇ ▹ A[γ]} γ↑ {◇} sg-a)
                  (_∘∙_ {Γ ▹ A}{_▹∙_ {Γ} Γ∙ {A} A∙}{◇ ▹ A[γ]}{_▹∙_ {◇} ◇∙ {A[γ]} A[γ]∙}{γ↑} γ↑∙ {◇}{◇∙}{sg-a} sg-a∙ (id {◇}) tt)
                  fa
   ; Π[]∙ = ~refl
   ; lam∙ = λ {Γ Γ∙ A} A∙ {B B∙ t} t∙ γ γ∙ a a∙ →
            let
              A[γ] = _[_]T {Γ} A {◇} γ
              A[γ]∙ = _[_]T∙ {Γ}{Γ∙}{A} A∙ {◇}{◇∙}{γ} (λ _ _ → γ∙)
              γ↑ = Ct.↑ {Γ}{A}{◇} γ
              γ↑∙ = dCt.↑∙ {Γ}{Γ∙}{A}{A∙}{◇}{◇∙}{γ} (λ _ _ → γ∙)
              B[γ↑] = _[_]T {Γ ▹ A} B {◇ ▹ A[γ]} γ↑
              B[γ↑]∙ = _[_]T∙ {Γ ▹ A}{_▹∙_ {Γ} Γ∙ {A} A∙}{B} B∙ {◇ ▹ A[γ]}{_▹∙_ {◇} ◇∙ {A[γ]} A[γ]∙}{γ↑} γ↑∙
              sg-a = Ct.sg {◇}{A[γ]} a
              sg-a∙ = dCt.sg∙ {◇}{◇∙}{A[γ]}{A[γ]∙}{a} (λ _ _ → a∙)
              γ↑∘sg-a = _∘_ {Γ ▹ A}{◇ ▹ A[γ]} γ↑ {◇} sg-a
              γ↑∘sg-a∙ = _∘∙_ {Γ ▹ A}{_▹∙_ {Γ} Γ∙ {A} A∙}{◇ ▹ A[γ]}{_▹∙_ {◇} ◇∙ {A[γ]} A[γ]∙}{γ↑} γ↑∙ {◇}{◇∙}{sg-a} sg-a∙ (id {◇}) tt
              t[γ↑] = _[_]t {Γ ▹ A}{B} t {◇ ▹ A[γ]} γ↑
            in coe (cong (B∙ γ↑∘sg-a γ↑∘sg-a∙) (Πβ {◇}{A[γ]}{B[γ↑]}{t[γ↑]}{a} ⁻¹)) (t∙ γ↑∘sg-a γ↑∘sg-a∙)
   ; lam[]∙ = ~refl
   ; app∙ = λ {Γ Γ∙ A A∙ B B∙ t} t∙ {u} u∙ γ γ∙ → t∙ γ γ∙ (_[_]t {Γ} {A} u {◇} γ) (u∙ γ γ∙)
   ; app[]∙ = ~refl
   ; Πβ∙ =  λ {Γ Γ∙ A A∙ B B∙ t t∙ a a∙} → funexth λ γ → funexth λ γ∙ →
            let
              sg-a = Ct.sg {Γ}{A} a
              sg-a∙ = dCt.sg∙ {Γ}{Γ∙}{A}{A∙}{a} a∙
            in coe-eq (cong (B∙ (_∘_ {Γ ▹ A}{Γ} sg-a {◇} γ) (sg-a∙ γ γ∙))
                            (cong (λ t → _[_]t {Γ}{_[_]T {Γ ▹ A} B {Γ} sg-a} t {◇} γ) (Πβ {Γ}{A}{B}{t}{a}) ⁻¹))
                      (t∙ (_∘_ {Γ ▹ A}{Γ} sg-a {◇} γ) (sg-a∙ γ γ∙)) ⁻¹
   ; Πη∙ = λ {Γ Γ∙ A A∙ B B∙ t t∙} → funexth λ γ → funexth λ γ∙ → funexth λ a → funexth λ a∙ → coe≡-eq _ (t∙ γ γ∙ a a∙)
   ; 𝔹∙ = λ γ γ∙ b → Canon𝔹 b
   ; 𝕥∙ = λ γ γ∙ → canon-𝕥 ~refl
   ; 𝕗∙ = λ γ γ∙ → canon-𝕗 ~refl
   ; ifᵀ∙ = λ {Γ Γ∙ b} b∙ {A} A∙ {B} B∙ γ γ∙ t →
              CanonIfT (_[_]t {Γ}{_[_]T {◇} 𝔹 {Γ} (ε {Γ})} b {◇} γ) (b∙ γ γ∙) (_[_]T {Γ} A {◇} γ) (A∙ γ γ∙) (_[_]T {Γ} B {◇} γ) (B∙ γ γ∙) t
   ; ifᵀ[]∙ = ~refl
   ; ifᵀβ₁∙ = λ {Γ Γ∙ A A∙ B B∙} → funexth λ γ → funexth λ γ∙ → funext λ {a₀} {a₁} aₑ → cong (A∙ γ γ∙) (coe≡-eq _ a₀ ⁻¹ ◼ aₑ)
   ; ifᵀβ₂∙ = λ {Γ Γ∙ A A∙ B B∙} → funexth λ γ → funexth λ γ∙ → funext λ {b₀} {b₁} bₑ → cong (B∙ γ γ∙) (coe≡-eq _ b₀ ⁻¹ ◼ bₑ)
   ; ifᵗ∙ = λ {Γ Γ∙ P} P∙ {P𝕥} P𝕥∙ {P𝕗} P𝕗∙ {b} b∙ γ γ∙ →
            let
              𝔹∙ = λ (γ : Sub ◇ ◇) (γ∙ : ⊤) (b : Tm ◇ 𝔹) → Canon𝔹 b
              𝕥∙ = λ (γ : Sub ◇ ◇) (γ∙ : ⊤) → canon-𝕥 {𝕥} ~refl
              𝕗∙ = λ (γ : Sub ◇ ◇) (γ∙ : ⊤) → canon-𝕗 {𝕗} ~refl
              𝔹[ε] = _[_]T {◇} 𝔹 {Γ} (ε {Γ})
              𝔹[ε]∙ = _[_]T∙ {◇}{◇∙}{𝔹} 𝔹∙ {Γ}{Γ∙}{ε {Γ}}(ε∙ {Γ}{Γ∙})
              γ↑ = Ct.↑ {Γ}{𝔹[ε]}{◇} γ
              γ↑∙ = dCt.↑∙ {Γ}{Γ∙}{𝔹[ε]}{𝔹[ε]∙}{◇}{◇∙}{γ} (λ _ _ → γ∙)
              P[γ↑] = _[_]T {Γ ▹ 𝔹[ε]} P {◇ ▹ 𝔹} γ↑
              P[γ↑]∙ = _[_]T∙ {Γ ▹ 𝔹[ε]}{_▹∙_ {Γ} Γ∙ {𝔹[ε]} 𝔹[ε]∙}{P} P∙ {◇ ▹ 𝔹}{_▹∙_ {◇} ◇∙ {𝔹} 𝔹∙}{γ↑} γ↑∙
              P[γ↑]∙' : (b : Tm ◇ 𝔹) (b∙ : Canon𝔹 b) → Tm ◇ (_[_]T {◇ ▹ 𝔹} P[γ↑] {◇} (Ct.sg {◇}{𝔹} b)) → Set
              P[γ↑]∙' b b∙ t = P∙ (_∘_ {Γ ▹ 𝔹[ε]}{◇ ▹ 𝔹} γ↑ {◇} (Ct.sg {◇}{𝔹} b))
                                  (_∘∙_ {Γ ▹ 𝔹[ε]}{_▹∙_ {Γ} Γ∙ {𝔹[ε]} 𝔹[ε]∙}{◇ ▹ 𝔹}{_▹∙_ {◇} ◇∙ {𝔹} 𝔹∙}{γ↑} γ↑∙ {◇}{◇∙}{Ct.sg {◇}{𝔹} b}
                                        (dCt.sg∙ {◇}{◇∙}{𝔹}{𝔹∙}{b} (λ _ _ → b∙)) (id {◇}) tt) t
              sg𝕥 = Ct.sg {Γ}{𝔹[ε]} (_[_]t {◇}{𝔹} 𝕥 {Γ} (ε {Γ}))
              sg𝕥∙ = dCt.sg∙ {Γ}{Γ∙}{𝔹[ε]}{𝔹[ε]∙}{_[_]t {◇}{𝔹} 𝕥 {Γ} (ε {Γ})} (_[_]t∙ {◇}{◇∙}{𝔹}{𝔹∙}{𝕥} 𝕥∙ {Γ}{Γ∙}{ε {Γ}} (ε∙ {Γ}{Γ∙}))
              P[sg𝕥] = _[_]t {Γ}{_[_]T {Γ ▹ 𝔹[ε]} P {Γ} sg𝕥} P𝕥 {◇} γ
              P[sg𝕥]∙ = _[_]t∙ {Γ}{Γ∙}{_[_]T {Γ ▹ 𝔹[ε]} P {Γ} sg𝕥}{_[_]T∙ {Γ ▹ 𝔹[ε]}
                               {_▹∙_ {Γ} Γ∙ {𝔹[ε]} 𝔹[ε]∙}{P} P∙ {Γ}{Γ∙}{sg𝕥} sg𝕥∙}{P𝕥} P𝕥∙ {◇}{◇∙}{γ} (λ _ _ → γ∙) (id {◇}) tt
              sg𝕗 = Ct.sg {Γ}{𝔹[ε]} (_[_]t {◇}{𝔹} 𝕗 {Γ} (ε {Γ}))
              sg𝕗∙ = dCt.sg∙ {Γ}{Γ∙}{𝔹[ε]}{𝔹[ε]∙}{_[_]t {◇}{𝔹} 𝕗 {Γ} (ε {Γ})} (_[_]t∙ {◇}{◇∙}{𝔹}{𝔹∙}{𝕗} 𝕗∙ {Γ}{Γ∙}{ε {Γ}} (ε∙ {Γ}{Γ∙}))
              P[sg𝕗] = _[_]t {Γ}{_[_]T {Γ ▹ 𝔹[ε]} P {Γ} sg𝕗} P𝕗 {◇} γ
              P[sg𝕗]∙ = _[_]t∙ {Γ}{Γ∙}{_[_]T {Γ ▹ 𝔹[ε]} P {Γ} sg𝕗}{_[_]T∙ {Γ ▹ 𝔹[ε]}
                               {_▹∙_ {Γ} Γ∙ {𝔹[ε]} 𝔹[ε]∙}{P} P∙ {Γ}{Γ∙}{sg𝕗} sg𝕗∙}{P𝕗} P𝕗∙ {◇}{◇∙}{γ} (λ _ _ → γ∙) (id {◇}) tt
              b[γ] = _[_]t {Γ}{𝔹[ε]} b {◇} γ
            in CanonIfᵗ P[γ↑] P[γ↑]∙' P[sg𝕥] P[sg𝕥]∙ P[sg𝕗] P[sg𝕗]∙ b[γ] (b∙ γ γ∙)
   ; ifᵗ[]∙ = ~refl
   ; ifᵗβ₁∙ = λ {Γ Γ∙ P P∙ P𝕥 P𝕥∙ P𝕗 P𝕗∙} → funexth λ γ → funexth λ γ∙ → coe≡-eq _ (P𝕥∙ γ γ∙) ⁻¹
   ; ifᵗβ₂∙ = λ {Γ Γ∙ P P∙ P𝕥 P𝕥∙ P𝕗 P𝕗∙} → funexth λ γ → funexth λ γ∙ → coe≡-eq _ (P𝕗∙ γ γ∙) ⁻¹
   }

module canonElim = initElimₛₛ CanonCwF CanonModel

canonCon : (Γ : Con) → Sub ◇ Γ → Set
canonCon Γ = canonElim.elimConₛₛ Γ

canonSub : (Γ Δ : Con) (σ : Sub Δ Γ) (δ : Sub ◇ Δ) (δ∙ : canonCon Δ δ) → canonCon Γ (_∘_ {Γ}{Δ} σ {◇} δ)
canonSub Γ Δ σ = canonElim.elimSubₛₛ {Γ}{Δ} σ

canonTy : (Γ : Con) (A : Ty Γ) (γ : Sub ◇ Γ) (γ∙ : canonCon Γ γ) (a : Tm ◇ (_[_]T {Γ} A {◇} γ)) → Set
canonTy Γ A = canonElim.elimTyₛₛ {Γ} A

canonTm : (Γ : Con) (A : Ty Γ) (a : Tm Γ A) (γ : Sub ◇ Γ) (γ∙ : canonCon Γ γ) → canonTy Γ A γ γ∙ (_[_]t {Γ} {A} a {◇} γ)
canonTm Γ A a = canonElim.elimTmₛₛ {Γ}{A} a

canon𝔹 : (b : Tm ◇ 𝔹) → Canon𝔹 b
canon𝔹 b = canonTm ◇ 𝔹 b (id {◇}) tt