TT in TT using Prop + setoid fibrations

TTinTTasSetoid.agda

{-# OPTIONS --prop --without-K --show-irrelevant --safe #-}

{-
Challenge:
- Define a deeply embedded faithfully represented syntax of a dependently typed
  TT in Agda.
- Use an Agda fragment which has canonicity. This means that the combination of
  indexed inductive types & cubical equality is not allowed!
- Prove consistency.

The TT here has an empty universe U and Π. Consistency means that there's no
closed term with type U.
-}

-- Prop library
--------------------------------------------------------------------------------

open import Level

variable
  i j k : Level

infix 5 _≡_
data _≡_ {A : Set i}(a : A) : A → Prop i where
  rfl : a ≡ a
{-# BUILTIN EQUALITY _≡_ #-} -- used for "rewrite" in pattern matching

_⁻¹ : {A : Set i}{x y : A} → x ≡ y → y ≡ x
rfl ⁻¹ = rfl

_◼_ : {A : Set i}{x y z : A} → x ≡ y → y ≡ z → x ≡ z
rfl ◼ e' = e'

coep : ∀ {A B : Prop i} → A ≡ B → A → B
coep rfl x = x

happly : {A : Prop i}{B : A → Set j}{f g : ∀ a → B a} → f ≡ g → ∀ a → f a ≡ g a
happly rfl a = rfl

J : ∀ {A : Set i}{x : A}(B : ∀ y → x ≡ y → Prop j) → ∀ {y} → (p : x ≡ y) → B x rfl → B y p
J B rfl br = br

data ⊤ : Prop where
  tt : ⊤

data ⊥ : Prop where

exfalso : ⊥ → (A : Set i) → A
exfalso ()

record Σ {i j}(A : Prop i)(B : A → Prop j) : Prop (i ⊔ j) where
  constructor _,_
  field
    fst : A
    snd : B fst
open Σ

-- Syntax
--------------------------------------------------------------------------------

data Con  : Set
data Ty   : Con → Set
data Sub  : Con → Con → Set
data Tm   : ∀ Γ → Ty Γ → Set
data Con~ : Con → Con → Prop
data Ty~  : ∀ {Γ₀ Γ₁} → Con~ Γ₀ Γ₁ → Ty Γ₀ → Ty Γ₁ → Prop
data Sub~ : ∀ {Γ₀ Γ₁ Δ₀ Δ₁} → Con~ Γ₀ Γ₁ → Con~ Δ₀ Δ₁ → Sub Γ₀ Δ₀ → Sub Γ₁ Δ₁ → Prop
data Tm~  : ∀ {Γ₀ Γ₁ A₀ A₁}(Γ₂ : Con~ Γ₀ Γ₁) → Ty~ Γ₂ A₀ A₁ → Tm Γ₀ A₀ → Tm Γ₁ A₁ → Prop

variable
  Γ Δ Γ₀ Γ₁ Δ₀ Δ₁ θ θ₀ θ₁ : Con
  A B C A₀ A₁ B₀ B₁       : Ty _
  t u v t₀ t₁ u₀ u₁       : Tm _ _
  σ δ ν σ₀ σ₁ δ₀ δ₁ ν₀ ν₁ : Sub _ _
  Γ₂                      : Con~ Γ₀ Γ₁
  Δ₂                      : Con~ Δ₀ Δ₁
  θ₂                      : Con~ θ₀ θ₁
  A₂                      : Ty~ _ A₀ A₁
  B₂                      : Ty~ _ B₀ B₁

infixl 4 _,_
infixr 5 _∘_
infix 5 _[_]

data Con where
  ∙   : Con
  _,_ : ∀ Γ → Ty Γ → Con

data Ty where
  coe  : Con~ Γ₀ Γ₁ → Ty Γ₀ → Ty Γ₁

  ------------------------------------------------------------
  _[_] : Ty Δ → Sub Γ Δ → Ty Γ
  U    : Ty Γ
  Π    : (A : Ty Γ) → Ty (Γ , A) → Ty Γ
  El   : Tm Γ U → Ty Γ

data Sub where
  coe : Con~ Γ₀ Γ₁ → Con~ Δ₀ Δ₁ → Sub Γ₀ Δ₀ → Sub Γ₁ Δ₁

  ------------------------------------------------------------
  id  : Sub Γ Γ
  _∘_ : Sub Δ θ → Sub Γ Δ → Sub Γ θ
  ε   : Sub Γ ∙
  p   : Sub (Γ , A) Γ
  _,_ : (σ : Sub Γ Δ) → Tm Γ (A [ σ ]) → Sub Γ (Δ , A)

data Tm where
  coe  : ∀ Γ₂ → Ty~ Γ₂ A₀ A₁ → Tm Γ₀ A₀ → Tm Γ₁ A₁

  ------------------------------------------------------------
  _[_] : Tm Δ A → (σ : Sub Γ Δ) → Tm Γ (A [ σ ])
  q    : Tm (Γ , A) (A [ p ])
  lam  : Tm (Γ , A) B → Tm Γ (Π A B)
  app  : Tm Γ (Π A B) → Tm (Γ , A) B

data Con~ where
  rfl : Con~ Γ Γ
  sym : Con~ Γ Δ → Con~ Δ Γ
  trs : Con~ Γ Δ → Con~ Δ θ → Con~ Γ θ

  ------------------------------------------------------------
  ∙   : Con~ ∙ ∙
  _,_ : ∀ Γ₂ → Ty~ Γ₂ A₀ A₁ → Con~ (Γ₀ , A₀) (Γ₁ , A₁)

data Ty~ where
  rfl  : Ty~ rfl A A
  sym  : ∀ {Γ₀₁} → Ty~ Γ₀₁ A B → Ty~ (sym Γ₀₁) B A
  trs  : ∀ {Γ₀₁ Γ₁₂} → Ty~ Γ₀₁ A B → Ty~ Γ₁₂ B C → Ty~ (trs Γ₀₁ Γ₁₂) A C
  coh  : ∀ Γ₂ A → Ty~ {Γ₀}{Γ₁} Γ₂ A (coe Γ₂ A)

  ------------------------------------------------------------
  _[_] : Ty~ Δ₂ A₀ A₁ → Sub~ Γ₂ Δ₂ σ₀ σ₁ → Ty~ Γ₂ (A₀ [ σ₀ ]) (A₁ [ σ₁ ])
  U    : Ty~ Γ₂ U U
  Π    : (A₂ : Ty~ Γ₂ A₀ A₁) → Ty~ (Γ₂ , A₂) B₀ B₁ → Ty~ Γ₂ (Π A₀ B₀) (Π A₁ B₁)
  El   : Tm~ Γ₂ U t₀ t₁ → Ty~ Γ₂ (El t₀) (El t₁)

  ------------------------------------------------------------
  [id] : Ty~ rfl (A [ id ]) A
  [∘]  : Ty~ rfl (A [ σ ∘ δ ]) (A [ σ ] [ δ ])
  U[]  : Ty~ rfl (U [ σ ]) U
  Π[]  : Ty~ rfl (Π A B [ σ ]) (Π (A [ σ ]) (B [ σ ∘ p , coe rfl (sym [∘]) q ]))
  El[] : Ty~ rfl (El t [ σ ]) (El (coe rfl U[] (t [ σ ])))

data Sub~ where
  rfl  : Sub~ rfl rfl σ σ
  sym  : ∀ {Γ₀₁ Δ₀₁} → Sub~ Γ₀₁ Δ₀₁ σ δ → Sub~ (sym Γ₀₁) (sym Δ₀₁) δ σ
  trs  : ∀ {Γ₀₁ Δ₀₁ Γ₁₂ Δ₁₂} → Sub~ Γ₀₁ Δ₀₁ σ δ → Sub~ Γ₁₂ Δ₁₂ δ ν → Sub~ (trs Γ₀₁ Γ₁₂) (trs Δ₀₁ Δ₁₂) σ ν
  coh  : ∀ Γ₂ Δ₂ σ → Sub~ {Γ₀}{Γ₁} {Δ₀}{Δ₁} Γ₂ Δ₂ σ (coe Γ₂ Δ₂ σ)

  ------------------------------------------------------------
  id  : Sub~ Γ₂ Γ₂ id id
  _∘_ : Sub~ Δ₂ θ₂ σ₀ σ₁ → Sub~ Γ₂ Δ₂ δ₀ δ₁ → Sub~ Γ₂ θ₂ (σ₀ ∘ δ₀) (σ₁ ∘ δ₁)
  ε   : Sub~ Γ₂ ∙ ε ε
  p   : Sub~ (Γ₂ , A₂) Γ₂ p p
  _,_ : (σ₂ : Sub~ Γ₂ Δ₂ σ₀ σ₁) → Tm~ Γ₂ (A₂ [ σ₂ ]) t₀ t₁ → Sub~ Γ₂ (Δ₂ , A₂) (σ₀ , t₀) (σ₁ , t₁)

  ------------------------------------------------------------
  εη  : Sub~ rfl rfl σ ε
  idl : Sub~ rfl rfl (id ∘ σ) σ
  idr : Sub~ rfl rfl (σ ∘ id) σ
  ass : Sub~ rfl rfl (σ ∘ δ ∘ ν) ((σ ∘ δ) ∘ ν)
  p∘  : Sub~ rfl rfl (p ∘ (σ , t)) σ
  pq  : Sub~ rfl rfl (p , q) (id {Γ , A})
  ,∘  : Sub~ rfl rfl ((σ , t) ∘ δ) (σ ∘ δ , coe rfl (sym [∘]) (t [ δ ]))

data Tm~ where
  rfl  : Tm~ rfl rfl t t
  sym  : ∀ {Γ₀₁ A₀₁} → Tm~ Γ₀₁ A₀₁ t u → Tm~ (sym Γ₀₁) (sym A₀₁) u t
  trs  : ∀ {Γ₀₁ A₀₁ Γ₁₂ A₁₂} → Tm~ Γ₀₁ A₀₁ t u → Tm~ Γ₁₂ A₁₂ u v → Tm~ (trs Γ₀₁ Γ₁₂) (trs A₀₁ A₁₂) t v
  coh  : ∀ Γ₂ A₂ t → Tm~ {Γ₀}{Γ₁} {A₀}{A₁} Γ₂ A₂ t (coe Γ₂ A₂ t)

  ------------------------------------------------------------
  _[_] : Tm~ Δ₂ A₂ t₀ t₁ → (σ₂ : Sub~ Γ₂ Δ₂ σ₀ σ₁) → Tm~ Γ₂ (A₂ [ σ₂ ]) (t₀ [ σ₀ ]) (t₁ [ σ₁ ])
  q    : Tm~ (Γ₂ , A₂) (A₂ [ p {A₂ = A₂} ]) q q
  lam  : Tm~ (Γ₂ , A₂) B₂ t₀ t₁ → Tm~ Γ₂ (Π A₂ B₂) (lam t₀) (lam t₁)
  app  : Tm~ Γ₂ (Π A₂ B₂) t₀ t₁ → Tm~ (Γ₂ , A₂) B₂ (app t₀) (app t₁)

  ------------------------------------------------------------
  q[]   : Tm~ rfl (trs (sym [∘]) (rfl [ p∘ ])) (q [ σ , t ]) t
  lam[] : Tm~ rfl Π[] (lam t [ σ ]) (lam (t [ σ ∘ p , coe rfl (sym [∘]) q ]))
  Πβ    : Tm~ rfl rfl (app (lam t)) t
  Πη    : Tm~ rfl rfl (lam (app t)) t


-- Example
--------------------------------------------------------------------------------

var₀U : Tm (Γ , U) U
var₀U = coe rfl U[] q

var₁U : Tm (Γ , U , A) U
var₁U = coe rfl U[] (var₀U [ p ])

var₀El : Tm (Γ , El t) (El (coe rfl U[] (t [ p ])))
var₀El = coe rfl El[] q

-- idFun : (A : U) → El A → El A
-- idFun = λ A x. x

idFun : Tm Γ (Π U (Π (El var₀U) (El var₁U)))
idFun = lam (lam var₀El)


-- Proof of consistency
--------------------------------------------------------------------------------

Conᴹ  : Con → Prop
Tyᴹ   : Ty Γ → Conᴹ Γ → Prop
Subᴹ  : Sub Γ Δ → Conᴹ Γ → Conᴹ Δ
Tmᴹ   : Tm Γ A → (γ : Conᴹ Γ) → Tyᴹ A γ
Con~ᴹ : Con~ Γ₀ Γ₁ → Conᴹ Γ₀ ≡ Conᴹ Γ₁
Ty~ᴹ  : Ty~ Γ₂ A₀ A₁ → Tyᴹ A₀ ≡ (λ γ → Tyᴹ A₁ (coep (Con~ᴹ Γ₂) γ))

Conᴹ ∙       = ⊤
Conᴹ (Γ , A) = Σ (Conᴹ Γ) (Tyᴹ A)

Tyᴹ (coe Γ₂ A) γ = Tyᴹ A (coep (Con~ᴹ Γ₂ ⁻¹) γ)
Tyᴹ (A [ σ ]) γ  = Tyᴹ A (Subᴹ σ γ)
Tyᴹ U γ          = ⊥
Tyᴹ (Π A B) γ    = (x : Tyᴹ A γ) → Tyᴹ B (γ , x)
Tyᴹ (El t) γ     = exfalso (Tmᴹ t γ) _

Con~ᴹ rfl          = rfl
Con~ᴹ (sym Γ~)     = Con~ᴹ Γ~ ⁻¹
Con~ᴹ (trs Γ~ Γ~') = Con~ᴹ Γ~ ◼ Con~ᴹ Γ~'
Con~ᴹ ∙            = rfl
Con~ᴹ (Γ~ , A~)    rewrite Ty~ᴹ A~ | Con~ᴹ Γ~ = rfl

Ty~ᴹ rfl = rfl
Ty~ᴹ (sym A~) rewrite Ty~ᴹ A~ = rfl
Ty~ᴹ (trs A~ A~') rewrite Ty~ᴹ A~ | Ty~ᴹ A~' = rfl
Ty~ᴹ (coh Γ₂ A) = rfl
Ty~ᴹ (A~ [ σ~ ]) rewrite Ty~ᴹ A~ = rfl
Ty~ᴹ U = rfl
Ty~ᴹ {_}{_}{_}(Π {Γ₀}{Γ₁}{Γ₂}{A₀}{A₁}{B₀}{B₁} A~ B~) =

    J (λ f e → (λ γ → ∀ x → Tyᴹ B₀ (γ , x)) ≡
               (λ γ → ∀ x → Tyᴹ B₁ (coep (Con~ᴹ Γ₂) γ , coep (happly ((e ⁻¹) ◼ hyp1) γ) x)))
      hyp1
      (J (λ f e → (λ γ → ∀ x → Tyᴹ B₀ (γ , x)) ≡ (λ γ → ∀ x → f (γ , x)))
         hyp2
         rfl)
    where
  hyp1 = Ty~ᴹ A~
  hyp2 = Ty~ᴹ B~

Ty~ᴹ (El t~) = rfl
Ty~ᴹ [id]    = rfl
Ty~ᴹ [∘]     = rfl
Ty~ᴹ U[]     = rfl
Ty~ᴹ Π[]     = rfl
Ty~ᴹ El[]    = rfl

Subᴹ (coe Γ~ Δ~ σ) γ = coep (Con~ᴹ Δ~) (Subᴹ σ (coep (Con~ᴹ Γ~ ⁻¹) γ))
Subᴹ id γ            = γ
Subᴹ (σ ∘ δ) γ       = Subᴹ σ (Subᴹ δ γ)
Subᴹ ε γ             = tt
Subᴹ p (γ , α)       = γ
Subᴹ (σ , t) γ       = Subᴹ σ γ , Tmᴹ t γ

Tmᴹ (coe Γ~ A~ t) γ = coep (happly (Ty~ᴹ A~) _) (Tmᴹ t (coep (Con~ᴹ Γ~ ⁻¹) γ))
Tmᴹ (t [ σ ]) γ     = Tmᴹ t (Subᴹ σ γ)
Tmᴹ q γ             = snd γ
Tmᴹ (lam t) γ       = λ x → Tmᴹ t (γ , x)
Tmᴹ (app t) (γ , α) = Tmᴹ t γ α

--------------------------------------------------------------------------------

consistent : Tm ∙ U → ⊥
consistent t = Tmᴹ t tt