# 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.

34 questions
Filter by
Sorted by
Tagged with
1 vote
70 views

### HoTT Book: Proof of Lemma 4.1.1 and exerices 2.17, using univalence

I have a question about a certain method of proof used in the HoTT book. This question might just boil down to how univalence is used in practice. The method of proof I have in mind can be seen in one ...
56 views

### Isomorphism vs. equivalence of types and homotopy vs. equality of functions

I am trying to build an understanding of the Univalence Axiom in HoTT and I am slightly confused about some definitions. If I was asked after reading of Chapter 1 of the HoTT book to formulate a ...
• 2,688
232 views

### Object Classifier implies Univalence in Type Theory?

There is a correspondence between univalence in Type Theory and object classifiers in $\infty$-toposes. This, for example, is suggested in the article Univalent Foundations for Mathematics on nlab. ...
• 73
107 views

72 views

### What is "univalent" about univalent logic and foundations?

This is a perhaps naive question about terminology. I know that "a bundle is said to be univalent if every other bundle is a pullback of it in at most one way (up to homotopy)" ref. But this ...
• 725
67 views

### Translating developments over different foundations

More and more often, different foundations of mathematics emerging. In some cases, they even rebuild classical theorems (e.g. number theory, Cartan geometry [1].. etc) on top of it. Some foundations ...
• 1,666
121 views

### What is the relation between (and status of) the Univalent Foundations and Homotopy Type Theory?

It appears as though UniMath and HoTT on GitHub are both active up til and including today. The Wikipedia pages have both linking to each other. Without being steeped in both areas, how do they relate,...
• 3,156
74 views

### What does "univalent" mean?

I have heard of the Univalent Axiom in the search for a foundation of mathematics, "Univalent Foundations". The univalent axiom says: The name univalence (due to Voevodsky) comes from the ...
• 3,156
1 vote
60 views

### Path induction for homotopies between functions

Consider a version of HoTT where every type former specifies the "shape" of its identity type definitionally (e.g. an equality of pairs is a pair of equalities, equality of types is ...
• 313
62 views

### What are the consequences of alternative type-theoretic definition of homotopy equivalence?

The standard definition of homotopy equivalence in HoTT is a quadruple of: $f: A \rightarrow B$ $g: B \rightarrow A$ $p: \operatorname{id} A = g \circ f$ $q: \operatorname{id} B = f \circ g$ ... ...
• 313
77 views

### Type theory for $\infty$-categories: retracts of shapes?

Here's another question about the formalities of Riehl and Shulman's A type theory for synthetic $\infty$-categories, and in particular about the role that "shapes" play in this type theory. In Prop 5....
• 9,841
225 views

### Type theory for $\infty$-categories: how do we inhabit $\text{hom}$ types?

I've started reading Riehl and Shulman's A type theory for synthetic $\infty$-categories, which looks like it develops some beautiful theory, but I want to make sure I'm not misunderstanding some of ...
• 9,841
206 views

### "Size Issues" and Cantor's Paradox in HoTT

Section 3.5 of the homotopy type theory book describes the type $\text{Set}_{\mathcal{U}_{i}}\equiv\sum_{(A:\mathcal{U}_i)}\text{isSet}(A)$, which can be thought as the "type of all sets in the ...
• 9,841
96 views

### Path-Lifting in HoTT

Lemma 2.3.2 of the HoTT book defines a kind of path-lifting for "fibrations" (ie type families): The proof is left as an exercise, but I'm struggling to understand what the last propositional ...
• 9,841
70 views

### Typos in HoTT appendix A.1.2?

I've started reading the HoTT book and am trying to understand its formal treatment of Martin-Löf type theory. Something small in the "first presentation" of the appendix has tripped me up; see the ...
• 9,841
187 views

### Why can't you formulate Voevodsky's 2-theories in set theory if its the foundation of maths?

I was reading up on the motivations of Voevodsky's homotopy type theory and was puzzled when i read that his main motivation was for his work in infinity groupoids. He was working on what he calls "...
• 31
93 views

• 2,740
345 views

### Can all mathematical operations be encoded with a Turing Complete language?

In High School Computing I was taught the Structured Program Theorem - that you could implement any mathematical operation using: Sequence Selection Iteration After completing a Computer Science ...
• 1,091
1 vote
98 views

### Type former as primitive constants

in the first appendix of the HoTT book the type formers (or connectives) are defined to be primitive constants, e.g. $\sum_{x:A}B$ is defined as $c_{\sum}(A,\lambda x.B)$. I was wondering what the ...
• 65
216 views

### Define $\neg\neg A$ to be truncation using LEM

I am currently reading the HoTT book and came across exercise 3.14: Show that assuming $\mathrm{LEM}$, the double negation $\neg \neg A$ has the same universal property as the propositional ...
• 65
176 views

### "Realizing" Globular Sets in Homotopy Type Theory

[Apologies in advance if I don't have the right terminology down for some things -- I'm a bit of a novice, hopefully not at the stage where I know enough to be dangerous, but not enough to be useful.] ...
209 views

### Question about the Univalence axiom.

In my study of Type Theory, the univalence axiom has been introduced as the statement that "Isomorphic structures are equal." I haven't learned how to define any algebraic, combinatorial, or ...
• 1,165
102 views

### Associativity of cartesian product in Univalent Foundations

In classical set theory, pairs $(x,y)$ are encoded usually in such a way that (for sets $A,B,C$) $(A\times B)\times C \neq A\times (B\times C)$. From my (small) knowledge of Univalent foundations, ...
• 757
867 views

### Will Homotopy Type Theory ever be as accessible as traditional Set Theory?

At the moment, Homotopy Type Theory is barely accessible to undergraduates, and only the most advanced or most gifted could have a decent chance of grasping it at a workable level without mountains of ...
• 3,612
357 views

### Definition of "set" in HoTT

In the homotopy type theory book (https://hott.github.io/book/nightly/hott-online-1007-ga1d0d9d.pdf) "set" is defined as follows (see chapter 3): Definition 3.1.1. A type A is a set if for all x, y : ...
• 41
122 views

### Finding a type such that $X + 1 \not\simeq X$ and $X+2\simeq X$

Yesterday, I read the following question : Finding a space such that $X\cong X+2$ and $X\not\cong X+1$, and found the result very astounding. Does it still hold in homotopy type theory? As a type ...
• 1,365
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,612
436 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,612