+ \def "classification membership of a term"
+ TEta = [t:*Term, a:*Obj] EEx(a, [y:*Obj] E(t, y))
+ : *Term => *Obj -> *Prop
+
+ \def "operation (rule with inhabited domain)"
+ Op = [f:*Obj] Ex([x:*Obj] Conv(OAt(f, x))) : *Obj -> *Prop
+
+ \def "classification inclusion"
+ ESub = [a1:*Obj, a2:*Obj] EAll(a1, [x:*Obj] Eta(x, a2))
+ : *Obj => *Obj -> *Prop
+
+ \def "classification morphism"
+ ETo = [f:*Obj, a:*Obj, b:*Obj] EAll(a, [x:*Obj] TEta(OAt(f, x), b))
+ : *Obj => *Obj => *Obj -> *Prop
+