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