module univTypes.SubjectReduction.Specification where

open import Data.Nat using (ℕ; zero; suc)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

open import univTypes.Util.Fin using (Fin; zero; suc)

-- Fixities --------------------------------------------------------------------

infix  4 _↪_ _↪*_
infix  4 _⊢_⦂_
infixl 5 _,_
infix  5 `λ_
infixl 7 _·_
infix  9 `_
infixl 9 _[_]

-- Axioms ----------------------------------------------------------------------

-- Functional Extensionality
postulate
  fun-ext : ∀ {ℓ₁ ℓ₂} {A : Set ℓ₁} {B : A → Set ℓ₂} {f g : (x : A) → B x}
    → (∀ x → f x ≡ g x)
    → f ≡ g

-- No other postulates are allowed!

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

data Term : ℕ → Set where
  `_      : ∀ {n} → Fin n → Term n
  `λ_     : ∀ {n} → Term (suc n) → Term n
  _·_     : ∀ {n} → Term n → Term n → Term n
  ∀[x⦂_]_ : ∀ {n} → Term n → Term (suc n) → Term n

    -- My Extension
  `Setω_  : ∀ {n} (l : Term n) → Term n
  `Setn_  : ∀ {n} (l : Term n) → Term n
  `Level  : ∀ {n} → Term n
  `lzero     : ∀ {n} → Term n
  `lsuc     : ∀ {n} → Term n → Term n
  _`⊔_    : ∀ {n} → Term n → Term n → Term n

  -- Extension
  ∃[x⦂_]_ : ∀ {n} → Term n → Term (suc n) → Term n
  _`,_    : ∀ {n} → Term n → Term n → Term n
  `proj₁  : ∀ {n} → Term n → Term n
  `proj₂  : ∀ {n} → Term n → Term n
  _`≡_    : ∀ {n} → Term n → Term n → Term n
  `refl   : ∀ {n} → Term n
  `subst  : ∀ {n} → Term (suc n) → Term n → Term n → Term n

-- Substitution ----------------------------------------------------------------

`Set : ∀ {n} → Term n
`Set = `Setn (`lzero)

-- Renamings

Ren : ℕ → ℕ → Set
Ren m n = Fin m → Fin n

extᵣ : ∀ {m n} → Ren m n → Ren (suc m) (suc n)
extᵣ ρ zero    = zero
extᵣ ρ (suc x) = suc (ρ x)

ren : ∀ {m n}
  → Ren m n
  → (Term m → Term n)
ren ρ (` x)                = ` (ρ x)
ren ρ (`λ e)               = `λ (ren (extᵣ ρ) e)
ren ρ (e₁ · e₂)            = (ren ρ e₁) · (ren ρ e₂)
ren ρ (∀[x⦂ e₁ ] e₂)       = ∀[x⦂ ren ρ e₁ ] ren (extᵣ ρ) e₂
ren ρ (`Setω l) = `Setω (ren ρ l)
ren ρ (`Setn x) = `Setn ren ρ x
ren ρ `Level               = `Level
ren ρ `lzero               = `lzero
ren ρ (`lsuc l)            = `lsuc (ren ρ l)
ren ρ (l `⊔ r)            = (ren ρ l) `⊔ (ren ρ r)
ren ρ (∃[x⦂ t₁ ] t₂)       = ∃[x⦂ ren ρ t₁ ] ren (extᵣ ρ) t₂
ren ρ (e₁ `, e₂)           = (ren ρ e₁) `, (ren ρ e₂)
ren ρ (`proj₁ e)           = `proj₁ (ren ρ e)
ren ρ (`proj₂ e)           = `proj₂ (ren ρ e)
ren ρ `refl                = `refl
ren ρ (e₁ `≡ e₂)           = ren ρ e₁ `≡ ren ρ e₂
ren ρ (`subst t e₁ e₂)     = `subst (ren (extᵣ ρ) t) (ren ρ e₁) (ren ρ e₂)

wk : ∀ {n} → Ren n (suc n)
wk x = suc x

-- Substitutions

Sub : ℕ → ℕ → Set
Sub m n = Fin m → Term n

extₛ : ∀ {m n} → Sub m n → Sub (suc m) (suc n)
extₛ σ zero    = ` zero
extₛ σ (suc x) = ren wk (σ x)

sub : ∀ {m n}
  → Sub m n
  → (Term m → Term n)
sub σ (` x)                = σ x
sub σ (`λ e)               = `λ (sub (extₛ σ) e)
sub σ (e₁ · e₂)            = (sub σ e₁) · (sub σ e₂)
sub σ (∀[x⦂ e₁ ] e₂)       = ∀[x⦂ sub σ e₁ ] sub (extₛ σ) e₂
sub σ (`Setω l)            = `Setω (sub σ l)
sub σ (`Setn l)            = `Setn sub σ l
sub σ (`Level)             = `Level
sub σ `lzero               = `lzero
sub σ (`lsuc l)            = `lsuc (sub σ l)
sub σ (l `⊔ r)             = (sub σ l) `⊔ (sub σ r)
sub σ (∃[x⦂ t₁ ] t₂)       = ∃[x⦂ sub σ t₁ ] sub (extₛ σ) t₂
sub σ (e₁ `, e₂)           = (sub σ e₁) `, (sub σ e₂)
sub σ (`proj₁ e)           = `proj₁ (sub σ e)
sub σ (`proj₂ e)           = `proj₂ (sub σ e)
sub σ `refl                = `refl
sub σ (e₁ `≡ e₂)           = sub σ e₁ `≡ sub σ e₂
sub σ (`subst t e₁ e₂)     = `subst (sub (extₛ σ) t) (sub σ e₁) (sub σ e₂)

0↦ : ∀ {n} → Term n → Sub (suc n) n
(0↦ e) zero    = e
(0↦ e) (suc x) = ` x

_[_] : ∀ {n} → Term (suc n) → Term n → Term n
e₁ [ e₂ ] = sub (0↦ e₂) e₁

-- Semantics -------------------------------------------------------------------

-- Values

mutual
  data Value : ∀ {n} → Term n → Set where
    val-λ : ∀ {n} {e : Term (suc n)}
      → Value e
        ------------
      → Value (`λ e)
    val-∀ : ∀ {n} {e₁ : Term n} {e₂ : Term (suc n)}
      → Value e₁
      → Value e₂
        --------------------
      → Value (∀[x⦂ e₁ ] e₂)
    val-Setω : ∀ {n l}
      → Value {n = n} (`Setω l)
    val-Setn : ∀ {n l}
      → Value l
      → Value {n = n} (`Setn l)

    val-Level : ∀ {n}
      → Value {n = n} `Level

    val-l : ∀ {n v}
      → Value {n = n} (`lzero)

    val-lsuc : ∀ {n v l}
      → Value l
      → Value {n = n} (`lsuc l)

    val-neu : ∀ {n} {e : Term n}
      → Neutral e
        ---------
      → Value e
    val-∃ : ∀ {n} {e₁ : Term n} {e₂ : Term (suc n)}
      → Value e₁
      → Value e₂
        --------------------
      → Value (∃[x⦂ e₁ ] e₂)
    val-, : ∀ {n} {e₁ e₂ : Term n}
      → Value e₁
      → Value e₂
        ---------
      → Value (e₁ `, e₂)
    val-≡ : ∀ {n} {e₁ : Term n} {e₂ : Term n}
      → Value e₁
      → Value e₂
        --------------------
      → Value (e₁ `≡ e₂)
    val-refl : ∀ {n}
      → Value {n = n} `refl

  data Neutral : ∀ {n} → Term n → Set where
    neu-` : ∀ {n} {x : Fin n}
      → Neutral (` x)
    neu-· : ∀ {n} {e₁ e₂ : Term n}
      → Neutral e₁
      → Value e₂
        -----------------
      → Neutral (e₁ · e₂)
    neu-proj₁ : ∀ {n} {e : Term n}
      → Neutral e
        -----------------
      → Neutral (`proj₁ e)
    neu-proj₂ : ∀ {n} {e : Term n}
      → Neutral e
        -----------------
      → Neutral (`proj₂ e)
    neu-subst : ∀ {n} {t : Term (suc n)} {e₁ e₂ : Term n}
      → Value t
      → Neutral e₁
      → Value e₂
        ------------------------
      → Neutral (`subst t e₁ e₂)

-- Reduction

data _↪_ : ∀ {n} → Term n → Term n → Set where
  β-λ : ∀ {n} {e₁ : Term (suc n)} {e₂ : Term n}
    → (`λ e₁) · e₂ ↪ e₁ [ e₂ ]

  ξ-λ : ∀ {n} {e e' : Term (suc n)}
    → e ↪ e'
    ---------------
    → `λ e ↪ `λ e'

  ξ-·₁ : ∀ {n} {e₁ e₂ e₁' : Term n}
    → e₁ ↪ e₁'
    ---------------------
    → e₁ · e₂ ↪ e₁' · e₂ 

  ξ-·₂ : ∀ {n} {e₁ e₂ e₂' : Term n}
    → e₂ ↪ e₂'
    ---------------------
    → e₁ · e₂ ↪ e₁ · e₂'

  ξ-∀₁ : ∀ {n} {t₁ t₁' : Term n} {t₂ : Term (suc n)}
    → t₁ ↪ t₁'
    -------------------------------
    → ∀[x⦂ t₁ ] t₂ ↪ ∀[x⦂ t₁' ] t₂

  ξ-∀₂ : ∀ {n} {t₁ : Term n} {t₂ t₂' : Term (suc n)}
    → t₂ ↪ t₂'
    -------------------------------
    → ∀[x⦂ t₁ ] t₂ ↪ ∀[x⦂ t₁ ] t₂'

  β-proj₁ : ∀ {n} {e₁ e₂ : Term n}
    → `proj₁ (e₁ `, e₂) ↪ e₁

  β-proj₂ : ∀ {n} {e₁ e₂ : Term n}
    → `proj₂ (e₁ `, e₂) ↪ e₂

  β-subst : ∀ {n} {t : Term (suc n)} {e : Term n}
    → `subst t `refl e ↪ e

  ξ-∃₁ : ∀ {n} {t₁ t₁' : Term n} {t₂ : Term (suc n)}
    → t₁ ↪ t₁'
    -------------------------------
    → ∃[x⦂ t₁ ] t₂ ↪ ∃[x⦂ t₁' ] t₂

  ξ-∃₂ : ∀ {n} {t₁ : Term n} {t₂ t₂' : Term (suc n)}
    → t₂ ↪ t₂'
    -------------------------------
    → ∃[x⦂ t₁ ] t₂ ↪ ∃[x⦂ t₁ ] t₂'

  ξ-proj₁ : ∀ {n} {e e' : Term n}
    → e ↪ e'
    → `proj₁ e ↪ `proj₁ e'

  ξ-proj₂ : ∀ {n} {e e' : Term n}
    → e ↪ e'
    → `proj₂ e ↪ `proj₂ e'

  ξ-,₁ : ∀ {n} {e₁ e₁' e₂ : Term n}
    → e₁ ↪ e₁'
    → (e₁ `, e₂) ↪ (e₁' `, e₂)

  ξ-,₂ : ∀ {n} {e₁ e₂ e₂' : Term n}
    → e₂ ↪ e₂'
    → (e₁ `, e₂) ↪ (e₁ `, e₂')

  ξ-≡₁ : ∀ {n} {t₁ t₁' : Term n} {t₂ : Term n}
    → t₁ ↪ t₁'
    -------------------------------
    → (t₁ `≡ t₂) ↪ (t₁' `≡ t₂)

  ξ-≡₂ : ∀ {n} {t₁ : Term n} {t₂ t₂' : Term n}
    → t₂ ↪ t₂'
    -------------------------------
    → (t₁ `≡ t₂) ↪ (t₁ `≡ t₂')

  ξ-subst₁ : ∀ {n} {t t' : Term (suc n)} {e₁ e₂ : Term n}
    → t ↪ t'
    → `subst t e₁ e₂ ↪ `subst t' e₁ e₂

  ξ-subst₂ : ∀ {n} {t : Term (suc n)} {e₁ e₁' e₂ : Term n}
    → e₁ ↪ e₁'
    → `subst t e₁ e₂ ↪ `subst t e₁' e₂

  ξ-subst₃ : ∀ {n} {t : Term (suc n)} {e₁ e₂ e₂' : Term n}
    → e₂ ↪ e₂'
    → `subst t e₁ e₂ ↪ `subst t e₁ e₂'

-- Extension:
  ξ-⊔₁ : ∀ {n} {t₁ t₁' : Term n} {t₂ : Term n}
    → t₁ ↪ t₁'
    -------------------------------
    → (t₁ `⊔ t₂) ↪ (t₁' `⊔ t₂)

  ξ-⊔₂ : ∀ {n} {t₁ : Term n} {t₂ t₂' : Term n}
    → t₂ ↪ t₂'
    -------------------------------
    → (t₁ `⊔ t₂) ↪ (t₁ `⊔ t₂')

  ξ-Setn : ∀ {n} {l l' : Term n}
    → l ↪ l'
    → `Setn l ↪ `Setn l'

  ξ-Setω : ∀ {n} {l l' : Term n}
    → l ↪ l'
    → `Setω l ↪ `Setω l'

-- Reflexive, Transitive Closure of Reduction

data _↪*_ : ∀ {n} → Term n → Term n → Set where
  ↪*-refl : ∀ {n} {e : Term n}
    → e ↪* e
  ↪*-step : ∀ {n} {e₁ e₂ e₃ : Term n}
    → e₁ ↪  e₂
    → e₂ ↪* e₃
    → e₁ ↪* e₃

↪*-trans : ∀ {n} {e₁ e₂ e₃ : Term n}
  → e₁ ↪* e₂
  → e₂ ↪* e₃
  → e₁ ↪* e₃
↪*-trans ↪*-refl q = q
↪*-trans (↪*-step x p) q = ↪*-step x (↪*-trans p q)

module ↪*-Reasoning where
  infix 1 begin_
  infixr 2 _↪⟨_⟩_ _↪*⟨_⟩_ _≡⟨_⟩_ _≡⟨⟩_
  infix 3 _∎

  begin_ : ∀ {n} {e₁ e₂ : Term n} → e₁ ↪* e₂ → e₁ ↪* e₂
  begin p = p

  _↪⟨_⟩_ : ∀ {n} (e₁ {e₂} {e₃} : Term n) → e₁ ↪ e₂ → e₂ ↪* e₃ → e₁ ↪* e₃
  _ ↪⟨ p ⟩ q = ↪*-step p q

  _↪*⟨_⟩_ : ∀ {n} (e₁ {e₂} {e₃} : Term n) → e₁ ↪* e₂ → e₂ ↪* e₃ → e₁ ↪* e₃
  _ ↪*⟨ p ⟩ q = ↪*-trans p q

  _≡⟨_⟩_ : ∀ {n} (e₁ {e₂} {e₃} : Term n) → e₁ ≡ e₂ → e₂ ↪* e₃ → e₁ ↪* e₃
  _ ≡⟨ refl ⟩ q = q

  _≡⟨⟩_ : ∀ {n} (e₁ {e₂} {e₃} : Term n) → e₁ ↪* e₂ → e₁ ↪* e₂
  _ ≡⟨⟩ q = q

  _∎ : ∀ {n} (e : Term n) → e ↪* e
  _ ∎ = ↪*-refl

-- Conversion

-- Two terms are convertible iff they reduce to a common term.

infix 4 _≈_
record _≈_ {n} (e₁ e₂ : Term n) : Set where
  constructor mk-≈
  field
    e-common     : Term n
    e₁↪*e-common : e₁ ↪* e-common
    e₂↪*e-common : e₂ ↪* e-common

open _≈_ public

-- Typing ----------------------------------------------------------------------

data Context : ℕ → Set where
  ∅   : Context zero
  _,_ : ∀ {n} → Context n → Term n → Context (suc n)

lookup : ∀ {n} → Context n → Fin n → Term n
lookup (Γ , e) zero    = ren wk e
lookup (Γ , e) (suc x) = ren wk (lookup Γ x)

data _⊢_⦂_ : ∀ {n} → Context n → Term n → Term n → Set where

  ⊢-` : ∀ {n t} {Γ : Context n} (x : Fin n)
    → lookup Γ x ≡ t
      --------------
    → Γ ⊢ ` x ⦂ t

  ⊢-λ : ∀ {n} {Γ : Context n} {e : Term (suc n)} {t₁ l : Term n} {t₂ : Term (suc n)}
    → Γ ⊢ t₁ ⦂ `Setn l
    → Γ , t₁ ⊢ e ⦂ t₂
      -----------------------
    → Γ ⊢ `λ e ⦂ ∀[x⦂ t₁ ] t₂

  ⊢-· : ∀ {n} {Γ : Context n} {e₁ e₂ : Term n} {t₁ : Term n} {t₂ : Term (suc n)}
    → Γ ⊢ e₁ ⦂ ∀[x⦂ t₁ ] t₂
    → Γ ⊢ e₂ ⦂ t₁ 
      -----------------------
    → Γ ⊢ e₁ · e₂ ⦂ t₂ [ e₂ ]

  ⊢-∀ : ∀ {n} {Γ : Context n} {t₁ l₁ l₃ : Term n} {t₂ l₂  : Term (suc n)}
    → Γ ⊢ t₁ ⦂ `Setn l₁
    → Γ , t₁ ⊢ t₂ ⦂ `Setn l₂
      -----------------------
    → Γ ⊢ ∀[x⦂ t₁ ] t₂ ⦂ `Setn l₃

  ⊢-≈ : ∀ {n} {Γ : Context n} {e : Term n} {t t' : Term n}
    → t ≈ t'
    → Γ ⊢ e ⦂ t
    ------------
    → Γ ⊢ e ⦂ t'

  ⊢-∃ : ∀ {n} {Γ : Context n} {t₁ : Term n} {t₂ : Term (suc n)}
    → Γ ⊢ t₁ ⦂ `Set
    → Γ , t₁ ⊢ t₂ ⦂ `Set
      -----------------------
    → Γ ⊢ ∃[x⦂ t₁ ] t₂ ⦂ `Set

  ⊢-, : ∀ {n} {Γ : Context n} {e₁ e₂ : Term n} {t₁ : Term n} {t₂ : Term (suc n)}
    → Γ ⊢ e₁ ⦂ t₁
    → Γ ⊢ e₂ ⦂ t₂ [ e₁ ]
      -----------------------
    → Γ ⊢ (e₁ `, e₂) ⦂ ∃[x⦂ t₁ ] t₂

  ⊢-proj₁ : ∀ {n} {Γ : Context n} {e : Term n} {t₁ : Term n} {t₂ : Term (suc n)}
    → Γ ⊢ e ⦂ ∃[x⦂ t₁ ] t₂
    → Γ ⊢ `proj₁ e ⦂ t₁

  ⊢-proj₂ : ∀ {n} {Γ : Context n} {e : Term n} {t₁ : Term n} {t₂ : Term (suc n)}
    → Γ ⊢ e ⦂ ∃[x⦂ t₁ ] t₂
    → Γ ⊢ `proj₂ e ⦂ t₂ [ `proj₁ e ]

  ⊢-≡ : ∀ {n} {Γ : Context n} {e₁ e₂ t : Term n}
    → Γ ⊢ e₁ ⦂ t
    → Γ ⊢ e₂ ⦂ t
      -----------------------
    → Γ ⊢ (e₁ `≡ e₂) ⦂ `Set

  ⊢-refl : ∀ {n} {Γ : Context n} {e t : Term n}
    → Γ ⊢ e ⦂ t
      ------------------
    → Γ ⊢ `refl ⦂ e `≡ e

  ⊢-subst : ∀ {n} {Γ : Context n} {e₁ e₂ u₁ u₂ : Term n} {t' : Term n} {t : Term (suc n)}
    → Γ , t' ⊢ t ⦂ `Set
    → Γ ⊢ u₁ ⦂ t'
    → Γ ⊢ u₂ ⦂ t'
    → Γ ⊢ e₁ ⦂ (u₁ `≡ u₂)
    → Γ ⊢ e₂ ⦂ t [ u₁ ]
      ------------------------------
    → Γ ⊢ `subst t e₁ e₂ ⦂ t [ u₂ ]

-- Extension
  ⊢-Setn : ∀ {n} {Γ : Context n} {l}
    → Γ ⊢ `Setn l ⦂ (`Setn (`lsuc l))

  ⊢-Setω : ∀ {n} {Γ : Context n} {l}
    → Γ ⊢ `Setω l ⦂ (`Setω (`lsuc l))

  ⊢-lzero : ∀ {n} {Γ : Context n}
    → Γ ⊢ `lzero  ⦂ `Level

  ⊢-lsuc : ∀ {n} {Γ : Context n} {l}
    → Γ ⊢ l  ⦂ `Level
    → Γ ⊢ `lsuc l  ⦂ `Level

  ⊢-⊔ : ∀ {n} {Γ : Context n} {l₁ l₂}
    → Γ ⊢ l₁  ⦂ `Level
    → Γ ⊢ l₂  ⦂ `Level
    → Γ ⊢ (l₁ `⊔ l₂)  ⦂ `Level

  ⊢-Level : ∀ {n} {Γ : Context n}
    → Γ ⊢ `Level ⦂ `Set

cong₃ : ∀ {A B C D : Set} (f : A → B → C → D) {x y u v a b} → x ≡ y → u ≡ v → a ≡ b → f x u a ≡ f y v b
cong₃ f refl refl refl = refl