Presentation with

• PER-style equality judgments; and
• Russell-style universes up to N; and
• judgments stratified by universe.

inductive Expr : Type

A Hott₀ expression.

• bvar (i : Nat) : Expr

  De Bruijn index.

• pi (l l' : Nat) (A B : Expr) : Expr

  Dependent product.

• lam (l l' : Nat) (ty body : Expr) : Expr

  Lambda.

• app (l l' : Nat) (B fn arg : Expr) : Expr

  Application at the specified output type.

• univ (l : Nat) : Expr

  (Russell) type universe.

• el (a : Expr) : Expr

  Type from a code.

• code (A : Expr) : Expr

  Code from a type.

instance instReprExpr : Repr Expr

Equations

• instReprExpr = { reprPrec := reprExpr✝ }

@[simp]

theorem Expr.sizeOf_pos (e : Expr) : 0 < sizeOf e