A type family is a map P:X→𝒰P:X \to \mathcal{U}.
Type families can be thought of as fibrations in classical homotopy theory. The base space is XX, the total space is ∑ (x:X)P(x)\sum_{(x:X)}P(x) and the fiber P(⋆ X)P(\star_X). This gives the fibration:
universe Synthetic homotopy theory
HoTT Book
Revision on September 20, 2018 at 22:13:30 by Richard Williamson?. See the history of this page for a list of all contributions to it.