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

Showing changes from revision #9 to #10: Added | Removed | Changed

* table of contents

Open problems

See open problems

Basic notions

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

Constructions and concepts


Homological Algebra



Useful references

category: homotopy theory

Revision on September 5, 2018 at 09:57:51 by Ali Caglayan. See the history of this page for a list of all contributions to it.