inductive Expr (χ : Type u) : Type u

A HoTT0 expression with axioms indexed by χ.

• ax {χ : Type u} (c : χ) (A : Expr χ) : Expr χ

  An axiom (i.e., a closed term constant in the theory) of the given type.

• bvar {χ : Type u} (i : Nat) : Expr χ

  De Bruijn index.

• pi {χ : Type u} (l l' : Nat) (A B : Expr χ) : Expr χ

  Dependent product.

• lam {χ : Type u} (l l' : Nat) (A b : Expr χ) : Expr χ

  Lambda with the specified argument type.

• app {χ : Type u} (l l' : Nat) (B fn arg : Expr χ) : Expr χ

  Application at the specified output type family B.

• sigma {χ : Type u} (l l' : Nat) (A B : Expr χ) : Expr χ

  Dependent sum.

• pair {χ : Type u} (l l' : Nat) (B t u : Expr χ) : Expr χ

  Pair formation.

• fst {χ : Type u} (l l' : Nat) (A B p : Expr χ) : Expr χ

  First component of a pair.

• snd {χ : Type u} (l l' : Nat) (A B p : Expr χ) : Expr χ

  Second component of a pair.

• Id {χ : Type u} (l : Nat) (A t u : Expr χ) : Expr χ

  Identity type.

• refl {χ : Type u} (l : Nat) (t : Expr χ) : Expr χ

  A reflexive identity.

• idRec {χ : Type u} (l l' : Nat) (t M r u h : Expr χ) : Expr χ

  Eliminates an identity.

• univ {χ : Type u} (l : Nat) : Expr χ

  A type universe.

• el {χ : Type u} (a : Expr χ) : Expr χ

  Type from a code.

• code {χ : Type u} (A : Expr χ) : Expr χ

  Code from a type.

instance instInhabitedExpr {a✝ : Type u_1} : Inhabited (Expr a✝)

Equations

• instInhabitedExpr = { default := Expr.bvar default }

instance instReprExpr {χ✝ : Type u_1} [Repr χ✝] : Repr (Expr χ✝)

Equations

• instReprExpr = { reprPrec := reprExpr✝ }

instance instToExprExprOfToLevel {χ✝ : Type u} [Lean.ToExpr χ✝] [Lean.ToLevel] : Lean.ToExpr (Expr χ✝)

Equations

• instToExprExprOfToLevel = { toExpr := toExprExpr✝ inst✝, toTypeExpr := (Lean.Expr.const `Expr [Lean.toLevel]).app (Lean.toTypeExpr χ✝) }

@[simp]

theorem Expr.sizeOf_pos {χ : Type u_1} (e : Expr χ) : 0 < sizeOf e

def Parser.Attr.autosubst_proc : Lean.ParserDescr

Simplification procedure

Equations

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

def Parser.Attr.autosubst : Lean.ParserDescr

A convergent rewriting system for the HoTT0 σ-calculus.

Equations

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