(32) ∑: (X:set)((X) prop) prop.
Die Syntax des höheren Niveaus ist ∑(A, B), wo A:set und B:(A) prop eingesetzt werden. Wenn ein Element von ∑(A, B) durch das Operator “pair” geformt wird, sind ein Element a: A und ein Beweis von B(a) gebraucht.
(33) pair: (X:set)(Y: (X)prop)(x:X)(Y(x))∑(X,Y).
Die Projektionen (p und q), die ein Element von A und einen Beweis von B(p(c)) durch einen Beweis c:∑(A, B) erzeugen, werden in (34) eingeführt. Allerdings sind sie nicht kanonisch.
(34)
p: (X:set)(Y: (X) prop)(z:∑(X,Y))X;
q: (X:set)(Y: (X) prop)(z:∑(X,Y))Y(p(X,Y,z)).
Π ist die gleiche Type wie ∑. Aber die monomorphische λ-Abstraktion und das ap-Operator werden eingeführt, um die monomorphische Regelungen aus der Zuweisung der Kategorien abzuleiten. Die Regelungen entsprechen den polymorphischen Typentheorien, die Matin-Löf darstellte. Diese Operatoren wie ∑, Π, pair, λ, p, q und ap werden im Lexikon der deutschen Grammatik enthalten.
(35)
Π: (X:set)((X) prop) prop;
λ: (X:set)(Y: (X) prop)((x:X)Y) Π(X:Y);
ap: (X:set)(Y: (X)prop)(Π(X:Y))(x:X) Y(x).
花村嘉英（2005）「計算文学入門－Thomas Mannのイロニーはファジィ推論といえるのか？」より