David Corfield stuff

A map between homotopy types is equivalent to a dependent sum projection $f: \sum_{x: A} B(x) \to A$. If the types $B(x)$ are $n$-types, $f$ forgets $n$-stuff (Buchholtz).

Forgetting properties $-1$-types, it seems like we’re talking about the same thing, this red apple is an apple.

The difference between a subtype, a dependent sum of a dependent type that is necessarily a proposition for each element of the base type, and a dependent type that happens to be a subsingleton for each element of the base.

Perhaps as an example of the three: Married man; Man and warrant of his marriage; and, Man and his spouse. (Assuming we’re in a monogamous society.)

A map from a set to a set quotient is such that homotopy fibres are equivalent to the respective equivalence class. So this if forgetting $0$-stuff, while including a subtype is forgetting $(-1)$-stuff.