The boolean base type, for representing the classic boolean values "true" and "false"

Conjunction is defined here using implication and the universal quantifier, as the binary function that returns whether, for any boolean value, the arguments together implying the value necessarily implies the value. |- $/\ = (\p1 p2. !p. (p1 ==> (p2 ==> p)) ==> p)

This axiom states that, for any given function, the lambda abstraction formed by applying the function to the binding variable is equal to the function. |- !(f:'a->'b). (\x. f x) = f

The existential quantifier is defined using just selection, as the function that returns whether any element selected as satisfying the function's predicate argument necessarily satisfies the predicate. Note that if there is no element satisfying the predicate, then not even the result of the selection operation can satisfy the predicate. |- $? = (\(P:'a->bool). P ($@ P))

The universal quantifier is defined using equality and truth, simply as the function that returns whether its predicate argument returns true for every input. |- $! = (\(P:'a->bool). P = (\x. true))

This axiom states the antisymmetry property for implication. |- !p1 p2. (p1 ==> p2) ==> ((p2 ==> p1) ==> (p1 <=> p2))

The one-to-one predicate is defined as the function that returns whether its function argument having the same result when applied to two elements necessarily implies that the two elements are equal. |- ONE_ONE = (\(f:'a->'b). !x1 x2. f x1 = f x2 ==> x1 = x2)

This axiom states a crucial property about the selection operator, namely that any element satisfying a given predicate implies that the selected element for the predicate satisfies the predicate. Note that it says nothing about when there is no element that can satisfy the predicate. |- !(P:'a->bool) x. P x ==> P ($@ P)

It is the instance of the equality reflexive property for the boolean identity function. |- true <=> (\(p:bool). p) = (\p. p)

This predicate is used in the theorem created by the primitive type constant definition command to assert that there is a bijection from the new type to its representation type. It is defined as the function that takes a characteristic function (a predicate for elements of the representation type) and a representation function (mapping elements of the new type to the representation type), and returns whether the representation function is one-to-one and maps onto precisely those elements in the representation type that satisfy the characteristic function. |- TYPE_DEFINITION = (\P (rep:'b->'a). ONE_ONE rep /\ (!x. P x <=> (?y. x = rep y)))