mini-lob.agda

{-# OPTIONS --without-K #-}
module mini-lob where
open import Agda.Primitive public
  using    (Level; _⊔_; lzero; lsuc)
open import Data.Unit
open import Data.Product
open import Level
infixl 2 _▻_
infixl 3 _‘’_
infixr 1 _‘→’_
infixl 3 _‘’ₐ_
mutual
  data Context : Set where
    ε : Context
    _▻_ : (Γ : Context) → Type Γ → Context

  data Type : Context → Set where
    _‘’_ : ∀ {Γ A} → Type (Γ ▻ A) → Term {Γ} A → Type Γ
    ‘Type’ : ∀ {Γ} → Type Γ
    ‘□’ : ∀ Γ → Type (Γ ▻ ‘Type’)
    _‘→’_ : ∀ {Γ} → Type Γ → Type Γ → Type Γ

  data Term : {Γ : Context} → Type Γ → Set where
    ⌜_⌝ : ∀ {Γ} → Type Γ → Term {Γ} ‘Type’
    _‘’ₐ_ : ∀ {Γ A B} → Term {Γ} (A ‘→’ B) → Term {Γ} A → Term {Γ} B
    Lӧb : ∀ {Γ X} → Term {Γ} (‘□’ Γ ‘’ ⌜ X ⌝ ‘→’ X) -> Term {Γ} X

□ = Term {ε}
max-level = lzero

mutual
  Context⇓ : (Γ : Context) → Set (lsuc max-level)
  Context⇓ ε = Lift ⊤
  Context⇓ (Γ ▻ T) = Σ (Context⇓ Γ) (Type⇓ T)

  Type⇓ : {Γ : Context} → Type Γ → Context⇓ Γ → Set max-level
  Type⇓ (T ‘’ x) Γ⇓ = Type⇓ T (Γ⇓ , Term⇓ x Γ⇓)
  Type⇓ (‘Type’ {Γ}) Γ⇓ = Lift (Type Γ)
  Type⇓ (‘□’ Γ) Γ⇓ = Lift (Term {Γ} (lower (proj₂ Γ⇓)))
  Type⇓ (A ‘→’ B) Γ⇓ = Type⇓ A Γ⇓ → Type⇓ B Γ⇓

  Term⇓ : ∀ {Γ : Context} {T : Type Γ} → Term T → (Γ⇓ : Context⇓ Γ) → Type⇓ T Γ⇓
  Term⇓ ⌜ x ⌝ Γ⇓ = lift x
  Term⇓ (f ‘’ₐ x) Γ⇓ = Term⇓ f Γ⇓ (Term⇓ x Γ⇓)
  Term⇓ (Lӧb s) Γ⇓ = Term⇓ s Γ⇓ (lift (Lӧb s))

⌞_⌟ : Type ε → Set _
⌞ T ⌟ = Type⇓ T _

löb : ∀ {‘X’} → Term (‘□’ ε ‘’ ⌜ ‘X’ ⌝ ‘→’ ‘X’) → ⌞ ‘X’ ⌟
löb f = Term⇓ (Löb f) _

gödel : Term (‘□’ ε ‘’ ⌜ ‘false’ ⌝ ‘→’ ‘false’) → ⊥
gödel f = lower (Term⇓ (Löb f) _)