# Questions tagged [univalent-foundations]

Univalent foundations are an approach to the foundations of mathematics in which mathematical structures are built out of objects called types.

40 questions
Filter by
Sorted by
Tagged with
92 views

### What are the axioms of homotopy type theory?

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 ...
• 314
67 views

### If $\Gamma\vdash b:\mathsf{Glue}[\phi\mapsto(T,f)]A$, then $\Gamma,\phi\vdash b:T$

Can someone help me from where in those rules I can deduce what is printed below, i.e. that if $\Gamma\vdash b:\mathsf{Glue}[\phi\mapsto(T,f)]A$, then $\Gamma,\phi\vdash b:T$? All the gluing types ...
• 3,574
97 views

### How To Choose What Counts As Isomorphic

Just a naive question about univalent foundations. As far as I understand, we want to define our mathematical types like sets, groups, categories, etc. such that structurally identical objects are ...
• 3,574
664 views

### Help! I don't believe in the identity elimination rule for Martin-Löf type theory/HoTT!

I was watching this video this video "$\infty$-Category Theory for Undergraduates" by Emily Riehl, and was onboard with everything except the path induction principle for identity types (27:...
• 8,805
157 views

• 36.4k
79 views

### Prospects of teaching/learning elementary math with computed-checked type theory

I've read as much as I can understand about type theory and homotopy type theory (HoTT) and it seems like these are very promising directions for re-foundationalizing mathematics in a way where ...
361 views

### Calculus in Homotopy Type Theory

My understanding is that homotopy type theory is intended as a new mathematical foundations, as is notably being written up at https://github.com/UniMath/UniMath. I am wondering whether there has been ...
• 442
1 vote
166 views

### Is HOTT, a new attempt at foundation of mathematics, free from incompleteness theorem or is it still suffering? [closed]

Do mathematicians who study Homotopy Type Theory think that it can be completely free from Godel-Rosser theorem?
64 views

• 1,395
2k views

### What is wrong with ZFC?

Why are there seemingly so many who want to use ETCS, or HoTT, or similar as a foundation of mathematics? I'm aware that HoTT has a good few good aspects, but that doesn't entirely explain the strong ...
• 3,986
471 views

### What is the likely future of Univalent Foundations?

Univalent foundations has been hyped up as the foundation for mathematics for the future in articles such as this one. Now I've given HoTT a brief look, and at least seen that it appears on the face ...
• 3,986