hott.types

Various datatypes.

prod
sigma
pi
arrow
eq
fiber
hprop_trunc: in this file we prove that is_trunc n A is a mere proposition. We separate this from trunc to avoid circularity in imports.
equiv
pointed
function: embeddings, (split) surjections, retractions
trunc: truncation levels, n-Types, truncation
W: W-types (not loaded by default)