Acc (accessibility)Bar (simulated partial computable objects)BoolDecidableFiniteFiniteMapGirardParadox (type is not a type)IntegerLogicListMiscellaneousNatNatural (natural numbers using “native” arithmetic)OptionPartial (partial computable objects)Permutation (permutations on lists)RelationsSmithParadox (there exist inadmissible types)StableSymbolTupleUnion (elimination forms for union and iexists)Wtype (well-founded types)