ETU.Rules

module ETU.Rules where

open import Prelude
open import WSLN

open import ETU.Syntax
open import ETU.Judgement

----------------------------------------------------------------------
-- Provable judgements in context, using cofinite quantification
-- instead of freshness assumptions
----------------------------------------------------------------------
infix 1 _⊢_
data Ok : Cx → Set
data _⊢_ (Γ : Cx) : Jg → Set

{- Some rules include helper hypotheses that aid proofs by structural
induction. -}

data Ok where
  -----------------------------
  -- Well-formed contexts: Ok Γ
  -----------------------------
  ok◇ : Ok ◇
  ok⨟ :
    {l : ℕ}
    {Γ : Cx}
    {A : Ty}
    {x : 𝔸}
    (q₀ : Γ ⊢ A ∶𝐔 l)
    (q₁ : x # Γ)
    -- helper hypothesis
    (h : Ok Γ)
    → -----------------
    Ok (Γ ⨟ x ∶[ l ] A)

data _⊢_  Γ where
  ------------------------------------
  -- Well-formed terms: Γ ⊢ a ∶[ l ] A
  ------------------------------------
  ⊢conv :
    {l : ℕ}
    {a : Tm}
    {A A' : Ty}
    (q₀ : Γ ⊢ a ∶[ l ] A)
    (q₁ : Γ ⊢ A ＝ A' ∶𝐔 l)
    → ---------------------
    Γ ⊢ a ∶[ l ] A'

  ⊢𝐯 :
    {l : ℕ}
    {A : Ty}
    {x : 𝔸}
    (q₀ : Ok Γ)
    (q₁ : (x , A , l) isIn Γ)
    → -----------------------
    Γ ⊢ 𝐯 x ∶[ l ] A

  ⊢𝐔 :
    {l : ℕ}
    (q : Ok Γ)
    → ---------------
    Γ ⊢ 𝐔 l ∶𝐔 (1+ l)

  ⊢𝚷 :
    {l l' : ℕ}
    {A : Tm}
    {B : Tm[ 1 ]}
    (S : Fset𝔸)
    (q₀ : Γ ⊢ A ∶𝐔 l)
    (q₁ : ∀ x → x # S →
      (Γ ⨟ x ∶[ l ] A) ⊢ B [ x ] ∶𝐔 l')
    → -------------------------------
    Γ ⊢ 𝚷 l l' A B ∶𝐔 (max l l')

  ⊢𝛌 :
    {l l' : ℕ}
    {A : Ty}
    {B : Ty[ 1 ]}
    {b : Tm[ 1 ]}
    (S : Fset𝔸)
    (q₀ : ∀ x → x # S →
      (Γ ⨟ x ∶[ l ] A) ⊢ b [ x ] ∶[ l' ] B [ x ])
    -- helper hypotheses
    (h₀ : Γ ⊢ A ∶𝐔 l)
    (h₁ : ∀ x → x # S →
      (Γ ⨟ x ∶[ l ] A) ⊢ B [ x ] ∶𝐔 l')
    → -------------------------------------------
    Γ ⊢ 𝛌 A b ∶[ max l l' ] 𝚷 l l' A B

  ⊢∙ :
    {l l' : ℕ}
    {A : Ty}
    {B : Ty[ 1 ]}
    {a b : Tm}
    (S : Fset𝔸)
    (q₀ : Γ ⊢ b ∶[ max l l' ] 𝚷 l l' A B)
    (q₁ : Γ ⊢ a ∶[ l ] A)
    (q₂ : ∀ x → x # S →
      (Γ ⨟ x ∶[ l ] A) ⊢ B [ x ] ∶𝐔 l')
    -- helper hypothesis
    (h : Γ ⊢ A ∶𝐔 l)
    → -----------------------------------
    Γ ⊢ b ∙[ A , B ] a ∶[ l' ] B [ a ]

  ⊢𝐄𝐪 :
    {l : ℕ}
    {A a b : Tm}
    (q₀ : Γ ⊢ a ∶[ l ] A)
    (q₁ : Γ ⊢ b ∶[ l ] A)
    -- helper hypothesis
    (h : Γ ⊢ A ∶𝐔 l)
    → -------------------
    Γ ⊢ 𝐄𝐪 A a b ∶𝐔 l

  ⊢𝐫𝐞𝐟𝐥 :
    {l : ℕ}
    {A : Ty}
    {a : Tm}
    (q : Γ ⊢ a ∶[ l ] A)
    -- helper hypothesis
    (h : Γ ⊢ A ∶𝐔 l)
    → ---------------------------
    Γ ⊢ 𝐫𝐞𝐟𝐥 A a ∶[ l ] 𝐄𝐪 A a a

  ⊢𝐄𝐦𝐩 :
    (q : Ok Γ)
    → ---------
    Γ ⊢ 𝐄𝐦𝐩 ∶𝐔 0

  ⊢𝐞𝐦𝐩 :
    {l : ℕ}
    {A : Ty}
    {e : Tm}
    (q₀ : Γ ⊢ A ∶𝐔 l)
    (q₁ : Γ ⊢ e ∶[ 0 ] 𝐄𝐦𝐩)
    → ---------------------
    Γ ⊢ 𝐞𝐦𝐩 A e ∶[ l ] A

  ⊢𝐍𝐚𝐭 :
    (q : Ok Γ)
    → ---------
    Γ ⊢ 𝐍𝐚𝐭 ∶𝐔 0

  ⊢𝐳𝐞𝐫𝐨 :
    (q : Ok Γ)
    → -----------------
    Γ ⊢ 𝐳𝐞𝐫𝐨 ∶[ 0 ] 𝐍𝐚𝐭

  ⊢𝐬𝐮𝐜𝐜 :
    {a : Tm}
    (q : Γ ⊢ a ∶[ 0 ] 𝐍𝐚𝐭)
    → --------------------
    Γ ⊢ 𝐬𝐮𝐜𝐜 a ∶[ 0 ] 𝐍𝐚𝐭

  ⊢𝐧𝐫𝐞𝐜 :
    {l : ℕ}
    {C : Ty[ 1 ]}
    {c₀ a : Tm}
    {c₊ : Tm[ 2 ]}
    (S : Fset𝔸)
    (q₀ : Γ ⊢ c₀ ∶[ l ] C [ 𝐳𝐞𝐫𝐨 ])
    (q₁ : ∀ x y → x # y # S →
      (Γ ⨟ x ∶[ 0 ] 𝐍𝐚𝐭 ⨟ y ∶[ l ] C [ x ]) ⊢
      c₊ [ x ][ y ] ∶[ l ] C [ 𝐬𝐮𝐜𝐜 (𝐯 x) ])
    (q₂ : Γ ⊢ a ∶[ 0 ] 𝐍𝐚𝐭)
    --  helper hypothesis
    (h : ∀ x → x # S →
      (Γ ⨟ x ∶[ 0 ] 𝐍𝐚𝐭) ⊢ C [ x ] ∶𝐔 l)
    → --------------------------------------
    Γ ⊢ 𝐧𝐫𝐞𝐜 C c₀ c₊ a ∶[ l ] C [ a ]

  ----------------------------------------------
  -- Definitional equality: Γ ⊢ a ＝ a' ∶[ l ] A
  ----------------------------------------------
  Refl :
    {l : ℕ}
    {A : Ty}
    {a : Tm}
    (q : Γ ⊢ a ∶[ l ] A)
    → ------------------
    Γ ⊢ a ＝ a ∶[ l ] A

  Symm :
    {l : ℕ}
    {A : Ty}
    {a a' : Tm}
    (q : Γ ⊢ a ＝ a' ∶[ l ] A)
    → ------------------------
    Γ ⊢ a' ＝ a ∶[ l ] A

  Trans :
    {l : ℕ}
    {A : Ty}
    {a a' a'' : Tm}
    (q₀ : Γ ⊢ a ＝ a' ∶[ l ] A)
    (q₁ : Γ ⊢ a' ＝ a'' ∶[ l ] A)
    → ---------------------------
    Γ ⊢ a ＝ a'' ∶[ l ] A

  ＝conv :
    {l : ℕ}
    {A A' : Ty}
    {a a' : Tm}
    (q₀ : Γ ⊢ a ＝ a' ∶[ l ] A)
    (q₁ : Γ ⊢ A ＝ A' ∶𝐔 l)
    → ------------------------
    Γ ⊢ a ＝ a' ∶[ l ] A'

  𝚷Cong :
    {l l' : ℕ}
    {A A' : Ty}
    {B B' : Ty[ 1 ]}
    (S : Fset𝔸)
    (q₀ : Γ ⊢ A ＝ A' ∶𝐔 l)
    (q₁ : ∀ x → x # S →
      (Γ ⨟ x ∶[ l ] A) ⊢ B [ x ] ＝ B' [ x ] ∶𝐔 l')
    -- helper hypothesis
    (h : Γ ⊢ A ∶𝐔 l)
    → -------------------------------------------
    Γ ⊢ 𝚷 l l' A B ＝ 𝚷 l l' A' B' ∶𝐔 (max l l')

  𝛌Cong :
    {l l' : ℕ}
    {A A' : Ty}
    {B : Ty[ 1 ]}
    {b b' : Tm[ 1 ]}
    (S : Fset𝔸)
    (q₀ : Γ ⊢ A ＝ A' ∶𝐔 l)
    (q₁ : ∀ x → x # S →
      (Γ ⨟ x ∶[ l ] A) ⊢ b [ x ] ＝ b' [ x ] ∶[ l' ] B [ x ])
    -- helper hypothesis
    (h₀ : Γ ⊢ A ∶𝐔 l)
    (h₁ : ∀ x → x # S →
      (Γ ⨟ x ∶[ l ] A) ⊢ B [ x ] ∶𝐔 l')
    → -----------------------------------------------------
    Γ ⊢ 𝛌 A b ＝ 𝛌 A' b' ∶[ max l l' ] 𝚷 l l' A B

  ∙Cong :
    {l l' : ℕ}
    {A A' : Ty}
    {B B' : Ty[ 1 ]}
    {a a' b b' : Tm}
    (S : Fset𝔸)
    (q₀ : Γ ⊢ A ＝ A' ∶𝐔 l)
    (q₁ : ∀ x → x # S →
      (Γ ⨟ x ∶[ l ] A) ⊢ B [ x ] ＝ B' [ x ] ∶𝐔 l')
    (q₂ : Γ ⊢ b ＝ b' ∶[ max l l' ] 𝚷 l l' A B)
    (q₃ : Γ ⊢ a ＝ a' ∶[ l ] A)
    -- helper hypotheses
    (h₀ : Γ ⊢ A ∶𝐔 l)
    (h₁ : ∀ x → x # S →
      (Γ ⨟ x ∶[ l ] A) ⊢ B [ x ] ∶𝐔 l')
    → ------------------------------------------------------
    Γ ⊢ b ∙[ A , B ] a ＝ b' ∙[ A' , B' ] a' ∶[ l' ] B [ a ]

  𝐄𝐪Cong :
    {l : ℕ}
    {A A' : Ty}
    {a a' b b' : Tm}
    (q₀ : Γ ⊢ A ＝ A' ∶𝐔 l)
    (q₁ : Γ ⊢ a ＝ a' ∶[ l ] A)
    (q₂ : Γ ⊢ b ＝ b' ∶[ l ] A)
    → -----------------------------
    Γ ⊢ 𝐄𝐪 A a b ＝ 𝐄𝐪 A' a' b' ∶𝐔 l

  𝐫𝐞𝐟𝐥Cong :
    {l : ℕ}
    {A A' : Ty}
    {a a' : Tm}
    (q₀ : Γ ⊢ A ＝ A' ∶𝐔 l)
    (q₁ : Γ ⊢ a ＝ a' ∶[ l ] A)
    → ----------------------------------------
    Γ ⊢ 𝐫𝐞𝐟𝐥 A a ＝ 𝐫𝐞𝐟𝐥 A' a' ∶[ l ] 𝐄𝐪 A a a

  𝐞𝐦𝐩Cong :
    {l : ℕ}
    {A A' : Ty}
    {e e' : Tm}
    (q₀ : Γ ⊢ A ＝ A' ∶𝐔 l)
    (q₁ : Γ ⊢ e ＝ e' ∶[ 0 ] 𝐄𝐦𝐩 )
    → -------------------------------
    Γ ⊢ 𝐞𝐦𝐩 A e ＝ 𝐞𝐦𝐩 A' e' ∶[ l ] A

  𝐬𝐮𝐜𝐜Cong :
    {a a' : Tm}
    (q : Γ ⊢ a ＝ a' ∶[ 0 ] 𝐍𝐚𝐭)
    → ------------------------------
    Γ ⊢ 𝐬𝐮𝐜𝐜 a ＝ 𝐬𝐮𝐜𝐜 a' ∶[ 0 ] 𝐍𝐚𝐭

  𝐧𝐫𝐞𝐜Cong :
    {l : ℕ}
    {C C' : Ty[ 1 ]}
    {c₀ c₀' a a'  : Tm}
    {c₊ c₊' : Tm[ 2 ]}
    (S : Fset𝔸)
    (q₀ : ∀ x → x # S →
      (Γ ⨟ x ∶[ 0 ] 𝐍𝐚𝐭) ⊢ C [ x ] ＝ C' [ x ] ∶𝐔 l)
    (q₁ : Γ ⊢ c₀ ＝ c₀' ∶[ l ] C [ 𝐳𝐞𝐫𝐨 ])
    (q₂ : ∀ x y → x # y # S →
      (Γ ⨟ x ∶[ 0 ] 𝐍𝐚𝐭 ⨟ y ∶[ l ] C [ x ]) ⊢
      c₊ [ x ][ y ] ＝ c₊' [ x ][ y ] ∶[ l ] C [ 𝐬𝐮𝐜𝐜 (𝐯 x) ])
    (q₃ : Γ ⊢ a ＝ a' ∶[ 0 ] 𝐍𝐚𝐭)
    -- helper hypothesis
    (h : ∀ x → x # S →
      (Γ ⨟ x ∶[ 0 ] 𝐍𝐚𝐭) ⊢ C [ x ] ∶𝐔 l)
    → --------------------------------------------------------
    Γ ⊢ 𝐧𝐫𝐞𝐜 C c₀ c₊ a ＝ 𝐧𝐫𝐞𝐜 C' c₀' c₊' a' ∶[ l ] C [ a ]

  𝚷Beta :
    {l l' : ℕ}
    {A : Ty}
    {a : Tm}
    {B : Ty[ 1 ]}
    {b : Tm[ 1 ]}
    (S : Fset𝔸)
    (q₀ : ∀ x → x # S →
      (Γ ⨟ x ∶[ l ] A) ⊢ b [ x ] ∶[ l' ] B [ x ])
    (q₁ : Γ ⊢ a ∶[ l ] A)
    -- helper hypotheses
    (h₀ : Γ ⊢ A ∶𝐔 l)
    (h₁ : ∀ x → x # S →
      (Γ ⨟ x ∶[ l ] A) ⊢ B [ x ] ∶𝐔 l')
    → -----------------------------------------------
    Γ ⊢ 𝛌 A b ∙[ A , B ] a ＝ b [ a ] ∶[ l' ] B [ a ]

  𝐍𝐚𝐭Beta₀ :
    {l : ℕ}
    {C : Ty[ 1 ]}
    {c₀ : Tm}
    {c₊ : Tm[ 2 ]}
    (S : Fset𝔸)
    (q₀ : Γ ⊢ c₀ ∶[ l ] C [ 𝐳𝐞𝐫𝐨 ])
    (q₁ : ∀ x y → x # y # S →
      (Γ ⨟ x ∶[ 0 ] 𝐍𝐚𝐭 ⨟ y ∶[ l ] C [ x ]) ⊢
      c₊ [ x ][ y ] ∶[ l ] C [ 𝐬𝐮𝐜𝐜 (𝐯 x) ])
    -- helper hypothesis
    (h : ∀ x → x # S →
      (Γ ⨟ x ∶[ 0 ] 𝐍𝐚𝐭) ⊢ C [ x ] ∶𝐔 l)
    → -------------------------------------------
    Γ ⊢ 𝐧𝐫𝐞𝐜 C c₀ c₊ 𝐳𝐞𝐫𝐨 ＝ c₀ ∶[ l ] C [ 𝐳𝐞𝐫𝐨 ]

  𝐍𝐚𝐭Beta₊ :
    {l : ℕ}
    {C : Ty[ 1 ]}
    {c₀ a : Tm}
    {c₊ : Tm[ 2 ]}
    (S : Fset𝔸)
    (q₀ : Γ ⊢ c₀ ∶[ l ] C [ 𝐳𝐞𝐫𝐨 ])
    (q₁ : ∀ x y → x # y # S →
      (Γ ⨟ x ∶[ 0 ] 𝐍𝐚𝐭 ⨟ y ∶[ l ] C [ x ]) ⊢
      c₊ [ x ][ y ] ∶[ l ] C [ 𝐬𝐮𝐜𝐜 (𝐯 x) ])
    (q₂ : Γ ⊢ a ∶[ 0 ] 𝐍𝐚𝐭)
    -- helper hypothesis
    (h : ∀ x → x # S →
      (Γ ⨟ x ∶[ 0 ] 𝐍𝐚𝐭) ⊢ C [ x ] ∶𝐔 l)
    → ---------------------------------------------
    Γ ⊢ 𝐧𝐫𝐞𝐜 C c₀ c₊ (𝐬𝐮𝐜𝐜 a) ＝
    c₊ [ a ][ 𝐧𝐫𝐞𝐜 C c₀ c₊ a ] ∶[ l ] C [ 𝐬𝐮𝐜𝐜 a ]

  𝚷Eta :
    {l l' : ℕ}
    {A : Ty}
    {B : Ty[ 1 ]}
    {b b' : Tm}
    (S : Fset𝔸)
    (q₀ : Γ ⊢ b ∶[ max l l' ] 𝚷 l l' A B)
    (q₁ : Γ ⊢ b' ∶[ max l l' ] 𝚷 l l' A B)
    (q₂ : ∀ x → x # S → (Γ ⨟ x ∶[ l ] A) ⊢
      b ∙[ A , B ] 𝐯 x ＝ b' ∙[ A , B ] 𝐯 x ∶[ l' ] B [ x ])
    -- helper hypotheses
    (h₀ : Γ ⊢ A ∶𝐔 l)
    (h₁ : ∀ x → x # S →
      (Γ ⨟ x ∶[ l ] A) ⊢ B [ x ] ∶𝐔 l')
    → ------------------------------------------------------
    Γ ⊢ b ＝ b' ∶[ max l l' ] 𝚷 l l' A B

  Reflect :
    {l : ℕ}
    {A : Ty}
    {a b e : Tm}
    (q₀ : Γ ⊢ a ∶[ l ] A)
    (q₁ : Γ ⊢ b ∶[ l ] A)
    (q₂ : Γ ⊢ e ∶[ l ] 𝐄𝐪 A a b)
    -- helper hypothesis
    (h : Γ ⊢ A ∶𝐔 l)
    → -------------------------
    Γ ⊢ a ＝ b ∶[ l ] A

  UIP :
    {l : ℕ}
    {A : Ty}
    {a b e e' : Tm}
    (q₀ : Γ ⊢ a ∶[ l ] A)
    (q₁ : Γ ⊢ b ∶[ l ] A)
    (q₂ : Γ ⊢ e ∶[ l ] 𝐄𝐪 A a b)
    (q₃ : Γ ⊢ e' ∶[ l ] 𝐄𝐪 A a b)
    -- helper hypothesis
    (h : Γ ⊢ A ∶𝐔 l)
    → ---------------------------
    Γ ⊢ e ＝ e' ∶[ l ] 𝐄𝐪 A a b

----------------------------------------------------------------------
-- Definitional equality of contexts
----------------------------------------------------------------------
infix 4 ⊢_＝_
data ⊢_＝_ : (Γ Γ' : Cx) → Set where
  ＝◇ : ⊢ ◇ ＝ ◇
  ＝⨟ :
    {l : ℕ}
    {Γ Γ' : Cx}
    {A A' : Ty}
    {x : 𝔸}
    (q₀ : ⊢ Γ ＝ Γ')
    (q₁ : Γ ⊢ A ＝ A' ∶𝐔 l)
    (q₂ : x # (Γ ,  Γ'))
    -- helper hypotheses
    (h₀ : Γ ⊢ A ∶𝐔 l)
    (h₁ : Γ' ⊢ A' ∶𝐔 l)
    → --------------------------------------
    ⊢ (Γ ⨟ x ∶[ l ] A) ＝ (Γ' ⨟ x ∶[ l ] A')

----------------------------------------------------------------------
-- Context weakening
----------------------------------------------------------------------
infix 4 _▷_
data _▷_ : (Δ Γ : Cx) → Set where
    ▷◇ : ◇ ▷ ◇
    ▷proj :
      {l : ℕ}
      {Δ Γ : Cx}
      {A : Ty}
      {x : 𝔸}
      (q₀ : Δ ▷ Γ)
      (q₁ : Δ ⊢ A ∶𝐔 l)
      (q₂ : x # Δ)
      → ----------------
      Δ ⨟ x ∶[ l ] A ▷ Γ
    ▷⨟ :
      {l : ℕ}
      {Δ Γ : Cx}
      {A : Ty}
      {x : 𝔸}
      (q₀ : Δ ▷ Γ)
      (q₁ : Γ ⊢ A ∶𝐔 l)
      (q₂ : x # Δ)
      -- helper hypothesis
      (h : Δ ⊢ A ∶𝐔 l)
      → -----------------------------
      Δ ⨟ x ∶[ l ] A ▷ Γ ⨟ x ∶[ l ] A

----------------------------------------------------------------------
-- Well-typed substitutions
----------------------------------------------------------------------
infix 4 _⊢ˢ_∶_
data _⊢ˢ_∶_ (Γ' : Cx) : Sb → Cx → Set where
  ◇ˢ :
    {σ : Sb}
    (q : Ok Γ')
    → ---------
    Γ' ⊢ˢ σ ∶ ◇
  ⨟ˢ :
    {l : ℕ}
    {Γ : Cx}
    {σ : Sb}
    {A : Ty}
    {x : 𝔸}
    (q₀ : Γ' ⊢ˢ σ ∶ Γ)
    (q₁ : Γ ⊢ A ∶𝐔 l)
    (q₂ : Γ' ⊢ σ x ∶[ l ] σ * A)
    (q₃ : x # Γ)
    → --------------------------
    Γ' ⊢ˢ σ ∶ (Γ ⨟ x ∶[ l ] A)

----------------------------------------------------------------------
-- Well-typed renamings
----------------------------------------------------------------------
infix 4 _⊢ʳ_∶_
_⊢ʳ_∶_ : Cx → Rn → Cx → Set
(Δ ⊢ʳ ρ ∶ Γ) = Δ ⊢ˢ 𝐚 ∘ ρ ∶ Γ

----------------------------------------------------------------------
-- Definitionally equal well-typed substitutions
----------------------------------------------------------------------
infix 4 _⊢ˢ_＝_∶_
data _⊢ˢ_＝_∶_ (Γ' : Cx) : Sb → Sb → Cx → Set where
  ＝◇ˢ :
    {σ σ' : Sb}
    (q : Ok Γ')
    → ---------------
    Γ' ⊢ˢ σ ＝ σ' ∶ ◇
  ＝⨟ˢ :
    {l : ℕ}
    {Γ : Cx}
    {σ σ' : Sb}
    {A : Ty}
    {x : 𝔸}
    (q₀ : Γ' ⊢ˢ σ ＝ σ' ∶ Γ)
    (q₁ : Γ ⊢ A ∶𝐔 l)
    (q₂ : Γ' ⊢ σ x ＝ σ' x ∶[ l ] σ * A)
    (q₃ : x # Γ)
    → ----------------------------------
    Γ' ⊢ˢ σ ＝ σ' ∶ (Γ ⨟ x ∶[ l ] A )