- \decl "syntactical identity" Id: *Set => *Set -> *Prop
-
- \decl "rule application" App: *Set => *Set => *Set -> *Prop
-
- \decl "classification predicate" Cl: *Set -> *Prop
-
- \decl "classification membership" Eta: *Set => *Set -> *Prop
-
- \decl "object-to-term-coercion" T: *Set -> *Term
-
- \decl "term application" At: *Term => *Term -> *Term
-
- \decl "term-object equivalence" E: *Term => *Set -> *Prop