Documentation

apply is a binary higher-order function that takes a function f and a list of type x values, [x], and returns a new list of values derived from the application of f to each of the x values within [x].

zero is the unique nullary function within the LargeCardinalHierarchy module that returns the additive identity element (and multiplicative absorbing element within the class of all cardinals), cardinal 0, via the Card constructor.

one is the unique nullary function within the LargeCardinalHierarchy module that returns the multiplicative identity element within the class of all cardinals, cardinal 1, via the Card constructor.

absolute is a type synonym (nullary function) for AbsoluteInfinity; the supremum of the class of all cardinals, Card.

zeros is a nullary function that returns a countably-infinite (aleph-null sized) sequence (a stream) of cardinal zeros.

ones is a nullary function that returns a countably-infinite (aleph-null sized) sequence (a stream) of cardinal ones.

alefz is a unary function that takes an Int n and returns an n-element list of the first n aleph numbers enumerating from aleph-null.

tavs is a nullary function that returns a countably-infinite (aleph-null sized) sequence (a stream) of TAVs; TAV being the symbol for the absolutely infinite supremum of the class of all cardinals, Card.

absolutes is a nullary function that returns a countably-infinite (aleph-null sized) sequence (a stream) of AbsoluteInfinitys; AbsoluteInfinity being the cardinality the class of all cardinals, Card.

absoluteInfinities is a type synonym (nullary function) for absolutes.

'(#)' is binary function from (Card, Card) to Card. '(#)' takes two cardinal numbers and returns their binary sum. Category-theoretically speaking, '(#)' is a coproduct in the class of all cardinals, Card.

'(#.)' is a unary (or, multiary) function from [Card] to Card. '(#.)' takes a list of cardinal numbers and returns their multiary sum. Category-theoretically speaking, '(#.)' is a coproduct in the class of all cardinals, Card.

'(*.)' is a binary function from (Card, Card) to Card. '(*.)' takes two cardinal numbers and returns their binary product.

x is a unary (or, multiary) function from [Card] to Card. x takes a list of cardinal numbers and returns their multiary product.

'(^.)' is a binary function from (Card,Card) to Card. '(^.)' take two cardinal numbers and returns the power of the zeroth cardinal number exponentiated to the first cardinal number.

cp is a binary function from [a] & [b] to [(a, b)]. cp takes two lists of elements and returns the list of all ordered pairs of elements between the two lists. cp is the Cartesian product operator.

cartesianProduct is a binary function from [a] & [b] to [(a, b)]. cartesianProduct takes two lists of elements and returns the list of all ordered pairs of elements between the two lists cartesianProduct is the Cartesian product operator.

powerList is a unary function from [a] -> [[a]]. powerList takes a list of elements and returns the list of all sublists of that list. powerList is a canonical example of Haskell's facilitation in expressing functions elegantly.

ascend is a unary function from Integer to [Card]. ascend takes a natural number n and returns a list of aleph cardinals from aleph 0 to aleph n.

descend is a unary function from Integer to [Card]. descend takes a natural number n and returns a list of aleph cardinals from aleph n to aleph 0.

level is a ternary function from (Int, Card, Integer) to Card. level takes an Int n, a Card value constructor cons, and an Integer m and returns a Card equal to cons $ cons $ cons $ ... $ Card m.

ascent is a quaternary function from (Int, Card, Integer, Integer) to [Card]. ascent takes an Int x, a Card value constructor cons, and two Integers y and z and returns a list of level x type cons Card values from y to z, where y <= z. ascent is a generalization of ascend over all data constructors in Card.

descent is a quaternary function from (Int, Card, Integer, Integer) to [Card]. descent takes an Int x, a Card value constructor cons, and two Integers y and z and returns a list of level x type cons Card values from y to z, where y >= z. descent is a generalization of descend over all data constructors in Card.

c is a unary function that takes an Integer n and returns a finite cardinal number, Card n.

alef is a unary function that takes an Integer n and returns a tranfinite aleph number subscripted by cardinal n, Aleph n.

aleph is a binary function from (Int, Integer) to Card. aleph takes an Int m and an Integer n and returns an m level Aleph whose deepest subscript is n.

beth is a binary function from (Int, Integer) to Card. beth takes an Int m and an Integer n and returns an m level Aleph whose deepest subscript is n.

wInac is a binary function from (Int, Integer) to Card. wInac takes an Int m and an Integer n and returns an m level WeaklyInaccessible whose deepest subscript is n.

weaklyInaccessible is a function synonym for wInac.

sInac is a binary function from (Int, Integer) to Card. sInac takes an Int m and an Integer n and returns an m level StronglyInaccessible whose deepest subscript is n.

stronglyInaccessible is a function synonym for sInac.

theta is a binary function from (Int, Integer) to Card. theta takes an Int m and an Integer n and returns an m level StronglyInaccessible cardinal whose deepest subscript is n. theta is a function synonym for sInac.

aInac is a binary function from (Int, Integer) to Card. aInac takes an Int m and an Integer n and returns an m level AlphaInaccessible whose deepest subscript is n.

alphaInaccessible is a binary function from (Int, Integer) to Card. alphaInaccessible takes an Int m and an Integer n and returns an m level AlphaInaccessible whose deepest subscript is n. alphaInaccessible is a function synonym for aInac.

hInac is a binary function from (Int, Integer) to Card. hInac takes an Int m and an Integer n and returns an m level HyperInaccessible whose deepest subscript is n.

hyperInaccessible is a binary function from (Int, Integer) to Card. hyperInaccessible takes an Int m and an Integer n and returns an m level HyperInaccessible whose deepest subscript is n. hyperInaccessible is a function synonym for hInac.

nu is a binary function from (Int, Integer) to Card. nu takes an Int m and an Integer n and returns an m level HyperInaccessible whose deepest subscript is n. nu is a function synonym for hInac.

h2Inac is a binary function from (Int, Integer) to Card. h2Inac takes an Int m and an Integer n and returns an m level Hyper2Inaccessible whose deepest subscript is n.

hyper2Inaccessible is a binary function from (Int, Integer) to Card. hyper2Inaccessible takes an Int m and an Integer n and returns an m level Hyper2Inaccessible whose deepest subscript is n. hyper2Inaccessible is a function synonym for h2Inac.

mu is a binary function from (Int, Integer) to Card. mu takes an Int m and an Integer n and returns an m level Hyper2Inaccessible whose deepest subscript is n. mu is a function synonym for h2Inac.

wMahlo is a binary function from (Int, Integer) to Card. wMahlo takes an Int m and an Integer n and returns an m level WeaklyMahlo whose deepest subscript is n.

weaklyMahlo is a binary function from (Int, Integer) to Card. weaklyMahlo takes an Int m and an Integer n and returns an m level WeaklyMahlo whose deepest subscript is n. weaklyMahlo is a function synonym for wMahlo.

sMahlo is a binary function from (Int, Integer) to Card. sMahlo takes an Int m and an Integer n and returns an m level StronglyMahlo whose deepest subscript is n.

stronglyMahlo is a binary function from (Int, Integer) to Card. stronglyMahlo takes an Int m and an Integer n and returns an m level StronglyMahlo whose deepest subscript is n. stronglyMahlo is a function synonym for sMahlo.

rho is a binary function from (Int, Integer) to Card. rho takes an Int m and an Integer n and returns an m level StronglyMahlo cardinal whose deepest subscript is n.

aMahlo is a binary function from (Int, Integer) to Card. aMahlo takes an Int m and an Integer n and returns an m level AlphaMahlo whose deepest subscript is n.

alphaMahlo is a binary function from (Int, Integer) to Card. alphaMahlo takes an Int m and an Integer n and returns an m level AlphaMahlo whose deepest subscript is n. alphaMahlo is a function synonym for aMahlo.

hMahlo is a binary function from (Int, Integer) to Card. hMahlo takes an Int m and an Integer n and returns an m level HyperMahlo whose deepest subscript is n.

hyperMahlo is a binary function from (Int, Integer) to Card. hyperMahlo takes an Int m and an Integer n and returns an m level HyperMahlo whose deepest subscript is n.

Binary function from (Int, Integer) to Card reflect takes an Int m and an Integer n and returns an m level reflecting cardinal whose deepest subscript is n

Binary function from (Int, Int, Int, Integer) to Card pii takes an Int x, an Int y, an Int m, and an Integer n and returns the m level pi-(x, y)-indescribable cardinal whose deepest subscript is n

Binary function from (Int, Integer) to Card ether takes an Int m and an Integer n and returns an m level ethereal cardinal whose deepest subscript is n

Binary function from (Int, Integer) to Card subtle takes an Int m and an Integer n and returns an m level subtle cardinal whose deepest subscript is n

Binary function from (Int, Integer) to Card kappa takes an Int m and an Integer n and returns an m level measurable cardinal whose deepest subscript is n

Binary function from (Int, Integer) to Card lambda takes an Int m and an Integer n and returns an m level rank-into-rank cardinal whose deepest subscript is n

Binary function from Int x Card to Card order takes an Int m and a Card card and returns the countably infinite list of level m card(s) indexed over the natural numbers [0..]. That is, order returns [(card m 0), (card m 1), (card m 2), (card m 3), . . .]

order increases linearly over its second argument keeping its first argument constant. order indexes in a zero order manner over the natural numbers. order m card = [(card m 0), (card m 1), (card m 2), (card m 3), . . .]

fixedpoints increases hierarchly over its first argument keeping its second argument constant. fixedpoints indexes in a higher order manner over its own arguments. fixedpoints m card = [(card 1 m), (card 2 m), (card 3 m), (card 4 m), . . .]

Binary function from Int x Card to Card zeroOrder takes an Int m and a Card card and returns the countably infinite list of level m card(s) indexed over the natural numbers [0..]. That is, zeroOrder returns [(card m 0), (card m 1), (card m 2), (card m 3), . . .]

zeroOrder increases linearly over its second argument keeping its first argument constant. zeroOrder indexes in a zero order manner over the natural numbers. zeroOrder m card = [(card m 0), (card m 1), (card m 2), (card m 3), . . .]

zeroOrder 1 Aleph = [Aleph(0), Aleph(1), Aleph(2), Aleph(3), . . .]

higherOrder increases hierarchly over its first argument keeping its second argument constant. higherOrder indexes in a higher order manner over its own arguments. higherOrder m card = [(card 1 m), (card 2 m), (card 3 m), (card 4 m), . . .]

higherOrder 1 Aleph = [(1), Aleph(1), Aleph(Aleph(1)), Aleph(Aleph(Aleph(1))), . . .]

Binary function from Int x Card to Card orderClass takes an Int m and a Card card and returns the countably infinite list of level m card(s) indexed over the natural numbers [0..]. That is, orderClass returns [(card m 0), (card m 1), (card m 2), (card m 3), . . .] orderClass is identical to order

Unary function from Card to Card club takes a Card value constructor card and returns the countably infinite list of type card Card fixed points indexed over the natural numbers [0..]. That is, club returns [(card 1 0), (card 2 0), (card 3 0), . . .] club is an implementation of the normal function f: Ordinals -> Ordinals that defines a closed and unbounded (club) class of ordinal fixed points according to the Fixed point lemma for normal functions

Binary function from Int x Card to Card fixedpoints takes an Int m and a Card value constructor card and returns the countably infinite list of type card Card fixed points indexed over the natural number m. That is, fixedpoints returns [(card 1 m), (card 2 m), (card 3 m), . . .] fixedpoints is an implementation of the normal function f: Ordinals -> Ordinals that defines a closed and unbounded (club) class of ordinal fixed points according to the Fixed point lemma for normal functions

fixedpoints increases hierarchly over its first argument keeping its second argument constant. fixedpoints indexes in a higher order manner over its own arguments. fixedpoints m card = [(card 1 m), (card 2 m), (card 3 m), (card 4 m), . . .]

order increases linearly over its second argument keeping its first argument constant. order indexes in a zero order manner over the natural numbers. order m card = [(card m 0), (card m 1), (card m 2), (card m 3), . . .]

Binary function from Int x Card to Card higherOrder takes an Int m and a Card value constructor card and returns the countably infinite list of type card Card fixed points indexed over the natural number m. That is, higherOrder returns [(card 1 m), (card 2 m), (card 3 m), . . .] higherOrder is an implementation of the normal function f: Ordinals -> Ordinals that defines a closed and unbounded (club) class of ordinal fixed points according to the Fixed point lemma for normal functions

higherOrder increases hierarchly over its first argument keeping its second argument constant. higherOrder indexes in a higher order manner over its own arguments. higherOrder m card = [(card 1 m), (card 2 m), (card 3 m), (card 4 m), . . .]

higherOrder 1 Aleph = [(1), Aleph(1), Aleph(Aleph(1)), Aleph(Aleph(Aleph(1))), . . .]

zeroOrder increases linearly over its second argument keeping its first argument constant. zeroOrder indexes in a zero order manner over the natural numbers. zeroOrder m card = [(card m 0), (card m 1), (card m 2), (card m 3), . . .]

zeroOrder 1 Aleph = [Aleph(0), Aleph(1), Aleph(2), Aleph(3), . . .]

Quaternary function from Int x Card x Int x Int to [Card] fromTo takes an Int ord, a Card value constructor cons, an Int m, and an Int n and returns the list of type cons Card(s) of order ord indexed from m to n. That is, fromTo returns [(cons ord m), . . . , (cons ord n)] fromTo ord cons m n = descent ord cons m n