What are the axioms of homotopy type theory?

87 Views Asked by At

The primitive notions of Zermelo-Fraenkel set theory are those of set and membership, i.e. we don't define what we mean by 'set' neither what we mean by '$\in$', rather, the axioms define what we mean by these concepts. Using the concepts of set and membership as well as the axioms of Zermelo-Fraenkel, we can define the cartesian product of two set $A$ and $B$ which we denote by $A\times B$, and using the concept of cartesian product we can define the concept of function.

I've heard that there is an alternative to set theory for a foundation of mathematics, this is known as 'Homotopy Type Theory', it's said that the primitive concepts of this theory is that of "homotopy type", so, a set is an homotopy type of certain level, similarly a truth-value and a category. The last seems very interesting for me. We can list the axioms of set theory which only involve 'set' and 'membership', so, if homotopy type is the only primitive notion of Homotopy type theory, then what is the list of axioms of homotopy type theory which only involves types?