# Homotopy Type Theory Synthetic homotopy theory (Rev #12, changes)

Showing changes from revision #11 to #12: Added | Removed | Changed

This page is under construction. - Ali

## Basic notions

• Higher inductive types
• Type families $P : A \to \mathcal{U}$ and fibrations $P(\star_A ) \to \sum_{(a:A)}P(a) \to A$

## Constructions and concepts

### Fibrations

• Hopf construction: H-space on $A$ gives fibration $A \to A \star A \to \Sigma A$

## Useful references

category: homotopy theory

Revision on September 14, 2018 at 05:10:20 by Ali Caglayan. See the history of this page for a list of all contributions to it.