Types in Martin-Lӧf Type Theory:
- unit
- bool
- num (natural numbers written in binary form)
- nat (subfolder)
- int (subfolder)
- prod
- sigma
- sum
- pi
- arrow
- arrow_2: alternative development of properties of arrows
- W: W-types (not loaded by default)
- lift
- list
- fin: finite types
The number systems (num, nat, int, ...) are for a large part ported from the standard libary.
Types in HoTT:
- eq: show that functions related to the identity type are equivalences
- pointed: pointed types, pointed maps, pointed homotopies, pointed equivalences and pointed truncated types
- fiber
- equiv
- trunc: truncation levels, n-types, truncation
- pullback
- univ
- type_functor
- pointed2: equalities between pointed homotopies, squares of poitned maps and pointed homotopies, and pointed maps in or out of
ppmap A B