@hackage LargeCardinalHierarchy0.0.0

Copyright (c) 2010 Stephen E. A. Britton. All rights reserved.

The LargeCardinalHierarchy module defines a recursively enumerable, countably infinite subclass of the logically (consistent) maximal transfinite set-theoretic universe ZFC+Con(LargeCardinals) (Zermelo-Frankel Set Theory + Axiom of Choice + All known large cardinals consistent with ZFC) via data constructors for each large cardinal within the hierarchy and functions over them. The algebraic data type Card is a Haskell implementation of the set theoretic proper class of all cardinals, Card. Card has value constructors for a countably infinite (aleph-null sized) subset of every cardinal type of all known large cardinals consistent with ZFC (Zermelo-Frankel Set Theory + Axiom of Choice) or, equivalently, ZF+GCH (Zermelo-Frankel Set Theory + Generalized Continuum Hypothesis).