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.

Filter by
Sorted by
Tagged with
2
votes
0answers
48 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
vote
1answer
41 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,...
1
vote
0answers
32 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 ...
1
vote
0answers
53 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 ...
0
votes
1answer
49 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$ ... ...
2
votes
1answer
60 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....
7
votes
1answer
135 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 ...
6
votes
1answer
154 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 ...
2
votes
1answer
62 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 ...
4
votes
0answers
61 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 ...
3
votes
1answer
140 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 "...
1
vote
1answer
74 views

Streicher's K axiom but for List

Some of the intuition behind relaxing Streicher's K axiom ("the only inhabitant of the identity type is reflexivity") is: "yes, there is only one uniformly definable element of the identity type $\...
2
votes
0answers
65 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 ...
0
votes
0answers
223 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 ...
1
vote
1answer
144 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?
2
votes
1answer
47 views

Definition Of Equivalence

I'm reading this paper on the univalence axiom and I'm stuck with the following definitions: Maybe my thinking is still too much grounded in set theory, but let's say $f$ is the identity on $\{0,...
6
votes
2answers
139 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
vote
1answer
68 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 ...
4
votes
2answers
189 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 ...
-1
votes
1answer
128 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.] ...
4
votes
1answer
195 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 ...
2
votes
1answer
92 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, ...
7
votes
1answer
668 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 ...
4
votes
2answers
302 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 : ...
2
votes
1answer
113 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 ...
22
votes
1answer
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 ...
7
votes
0answers
405 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 ...
7
votes
2answers
468 views

Two questions on homotopy type theory

In reading the HoTT book, I have found that it is easy to become bogged down in detail and hard to tell the general 'big picture' of what is going on. I hope to get some general answer to the ...