In this file we specify typing judgments of the type theory as Prop-valued relations.

def judgment.quot : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Category.judgment : Category

Equations

• Lean.Parser.Category.judgment = { }

def «term_⊢[_]_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def judgment_ : Lean.ParserDescr

Equations

• judgment_ = Lean.ParserDescr.node `judgment_ 50 (Lean.ParserDescr.cat `term 51)

def «judgment_≡_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def «judgment_:_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def «judgment_≡_:_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Ctx : Type

A typing context consisting of expressions and their universe levels.

Equations

• Ctx = List (Expr × ℕ)

def univMax : ℕ

The maximum l for which Γ ⊢[l] 𝒥 makes sense. When set to 0, types cannot be quantified over at all.

Equations

• univMax = 37

inductive EqTp : Ctx → ℕ → Expr → Expr → Prop

• cong_pi {Γ : Ctx} {A A' B B' : Expr} {l l' : ℕ} : Γ ⊢[l] A ≡ A' → (A, l) :: Γ ⊢[l'] B ≡ B' → Γ ⊢[max l l'] Expr.pi l l' A B ≡ Expr.pi l l' A' B'
• cong_univ (Γ : Ctx) (l : ℕ) : l < univMax → Γ ⊢[l + 1] Expr.univ l
• cong_el {Γ : Ctx} {A A' : Expr} {l : ℕ} : Γ ⊢[l + 1] A ≡ A' : Expr.univ l → Γ ⊢[l] A.el ≡ A'.el
• inst_tp {Γ : List (Expr × ℕ)} {A B B' t u : Expr} {l l' : ℕ} : (A, l) :: Γ ⊢[l'] B ≡ B' → Γ ⊢[l] t ≡ u : A → Γ ⊢[l'] B.inst t ≡ B.inst u
• lift_tp {Γ : Ctx} {A A' : Expr} {l : ℕ} (B : Expr) (l' : ℕ) : Γ ⊢[l] A ≡ A' → (B, l') :: Γ ⊢[l] A.lift ≡ A'.lift
• symm_tp {Γ : Ctx} {A A' : Expr} {l : ℕ} : Γ ⊢[l] A ≡ A' → Γ ⊢[l] A' ≡ A
• trans_tp {Γ : Ctx} {A A' A'' : Expr} {l : ℕ} : Γ ⊢[l] A ≡ A' → Γ ⊢[l] A' ≡ A'' → Γ ⊢[l] A ≡ A''

inductive EqTm : Ctx → ℕ → Expr → Expr → Expr → Prop

• cong_bvar0 {Γ : Ctx} {A : Expr} {l : ℕ} : Γ ⊢[l] A → (A, l) :: Γ ⊢[l] Expr.bvar 0 : A.lift
• cong_lam {Γ : Ctx} {A A' B t t' : Expr} {l l' : ℕ} : Γ ⊢[l] A ≡ A' → (A, l) :: Γ ⊢[l'] t ≡ t' : B → Γ ⊢[max l l'] Expr.lam l l' A t ≡ Expr.lam l l' A' t' : Expr.pi l l' A B
• cong_app {Γ : List (Expr × ℕ)} {A B B' f f' a a' : Expr} {l l' : ℕ} : (A, l) :: Γ ⊢[l'] B ≡ B' → Γ ⊢[max l l'] f ≡ f' : Expr.pi l l' A B → Γ ⊢[l] a ≡ a' : A → Γ ⊢[l'] Expr.app l l' B f a ≡ Expr.app l l' B' f' a' : B.inst a
• cong_code {Γ : Ctx} {A A' : Expr} {l : ℕ} : l < univMax → Γ ⊢[l] A ≡ A' → Γ ⊢[l + 1] A.code ≡ A'.code : Expr.univ l
• app_lam {Γ : List (Expr × ℕ)} {A B t u : Expr} {l l' : ℕ} : (A, l) :: Γ ⊢[l'] t : B → Γ ⊢[l] u : A → Γ ⊢[l'] Expr.app l l' B (Expr.lam l l' A t) u ≡ t.inst u : B.inst u
• eta {Γ : Ctx} {A B f : Expr} {l l' : ℕ} : Γ ⊢[max l l'] f : Expr.pi l l' A B → Γ ⊢[max l l'] f ≡ Expr.lam l l' A (Expr.app l l' (Expr.liftN 1 B 1) f.lift (Expr.bvar 0)) : Expr.pi l l' A B
• conv {Γ : Ctx} {A A' t t' : Expr} {l : ℕ} : Γ ⊢[l] A ≡ A' → Γ ⊢[l] t ≡ t' : A → Γ ⊢[l] t ≡ t' : A'
• inst_tm {Γ : List (Expr × ℕ)} {A B a b t u : Expr} {l l' : ℕ} : (A, l) :: Γ ⊢[l'] a ≡ b : B → Γ ⊢[l] t ≡ u : A → Γ ⊢[l'] a.inst t ≡ b.inst u : B.inst t
• lift_tm {Γ : Ctx} {A t t' : Expr} {l : ℕ} (B : Expr) (l' : ℕ) : Γ ⊢[l] t ≡ t' : A → (B, l') :: Γ ⊢[l] t.lift ≡ t'.lift : A.lift
• symm_tm {Γ : Ctx} {A t t' : Expr} {l : ℕ} : Γ ⊢[l] t ≡ t' : A → Γ ⊢[l] t' ≡ t : A
• trans_tm {Γ : Ctx} {A t t' t'' : Expr} {l : ℕ} : Γ ⊢[l] t ≡ t' : A → Γ ⊢[l] t' ≡ t'' : A → Γ ⊢[l] t ≡ t'' : A

inductive Lookup : Ctx → ℕ → Expr → ℕ → Prop

Lookup Γ i A l means that (A, l) is stored at index i in Γ. This implies Γ ⊢[l] .bvar i : A (see Lemmas).

• zero (Γ : Ctx) (A : Expr) (l : ℕ) : Γ ⊢[l] A → Lookup ((A, l) :: Γ) 0 A.lift l
• succ {Γ : Ctx} {A B : Expr} {i l l' : ℕ} : Lookup Γ i A l → Lookup ((B, l') :: Γ) (i + 1) A.lift l

Pretty-printers.

def EqTp.unexpand : Lean.PrettyPrinter.Unexpander

Equations

• One or more equations did not get rendered due to their size.

def EqTm.unexpand : Lean.PrettyPrinter.Unexpander

Equations

• One or more equations did not get rendered due to their size.