David Corfield

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

Forgetting properties 1-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 00-stuff, while including a subtype is forgetting (1)(-1)-stuff.

Last revised on April 23, 2021 at 05:13:27. See the history of this page for a list of all contributions to it.