The following libraries are pre-loaded:
Acc (accessibility)BoolDecidableDivision (natural number division)Eventually (simulated partial computable objects)FiniteFiniteMapFunctionIntegerIrrelevance (proof irrelevance)Kindlike (types eligible for impredicative quantification)LogicListMarkovMiscNatNatural (natural numbers using “native” arithmetic)OptionPartial (partial computable objects)Permutation (permutations on lists)Quotient (tools for manipulating quotient types)RationalRealRealExponentRealSupremumRealSequenceRelationsSqstableSquish (like squash, but with computational content)StableSymbolTupleWeaksum (an improved interface for union types)Wtype (well-founded types)The following libraries can be loaded from the library directory:
CantorTheorem (the reals are not enumerable)GirardParadox (type is not a type)SmithParadox (there exist inadmissible types)