As described in Definitions , some defined operators are treated for the most part as if they were primitives, since their definitions could be distracting to the casual browser. Here is a list of most of those operators.

t T == t = t	[member]
Y(f) == (x.f(x(x)))(x.f(x(x)))	[ycomb]
x f y == f(x,y)	[infix_ap]
T == T	[guard]
Prop == Type	[prop]
True == 0	[true]
False == Void	[false]
P & Q == PQ	[and]
A & B == AB	[cand]
P Q == P+Q	[or]
P Q == PQ	[implies]
x:A. B(x) == x:AB(x)	[exists]
x:A. B(x) == x:AB(x)	[all]
Unit == 0	[unit]
== *	[it]
== Unit+Unit	[bool]
true == inl()	[btrue]
false == inr()	[bfalse]
if b t else f fi == InjCase(b ; t; f)	[ifthenelse]

About: