lean2/hott/types/types.md

hott.types

Types (not necessarily HoTT-related):

• unit
• bool
• nat (subfolder)
• int (subfolder)
• prod
• sigma
• sum
• pi
• arrow
• W: W-types (not loaded by default)

HoTT types

• eq: show that functions related to the identity type are equivalences
• pointed
• fiber
• equiv
• trunc: truncation levels, n-Types, truncation