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.
37
questions
13
votes
3
answers
302
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:...
- 7,599
5
votes
1
answer
138
views
What's wrong with this "proof" involving' $n$-connectedness in HoTT?
okay, this is silly, but I can't for the life of me figure out what's wrong with the following "proof":
Claim: if $B$ is an $(n-1)$-type, then $(n\text{-conn}(A) \to B) \simeq (\text{isCntr}(...
- 1,766
1
vote
1
answer
131
views
Proving that W-algebra homomorphisms are contractible
I don't understand the conclusion of the proof of Theorem 5.4.7 of the Homotopy Type Theory text and would like a more detailed explanation of how it works. Here's my attempt at divining an answer.
...
- 45
1
vote
1
answer
92
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 ...
- 1,766
3
votes
1
answer
136
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,748
7
votes
1
answer
359
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
3
votes
1
answer
120
views
Confusion about quasi-inverses and equivalences in HoTT
I'm reading the HoTT book, section 2.4, where for $f : A \to B$, they define
$$\mathsf{qinv}(f) = \sum_{g:B\to A} \big( (f \circ g \sim \mathrm{id}) \times (g \circ f \sim \mathrm{id}) \big)$$
$$\...
- 1,816
2
votes
1
answer
139
views
Law of the Excluded Middle for Mere Propositions
In the Homotopy Type Theory book, they define the (non-contradictory) law of the excluded middle as
$$\operatorname{LEM}:\prod_{A:\mathcal U}\big(\operatorname{isProp}(A)\to(A+\lnot A)\big).\tag{3.4.1}...
- 689
2
votes
1
answer
98
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
3
votes
0
answers
73
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,770
1
vote
1
answer
153
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,492
2
votes
0
answers
150
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,492
2
votes
0
answers
78
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 ...
- 353
0
votes
1
answer
64
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$
... ...
- 353
2
votes
1
answer
89
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....
- 11.1k
7
votes
1
answer
256
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 ...
- 11.1k
6
votes
1
answer
230
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 ...
- 11.1k
6
votes
1
answer
134
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 ...
- 11.1k
4
votes
0
answers
74
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 ...
- 11.1k
3
votes
1
answer
222
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
0
votes
1
answer
109
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 $\...
- 35.4k
2
votes
0
answers
75
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 ...
- 645
0
votes
0
answers
336
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
1
answer
159
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?
- 11
2
votes
1
answer
61
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,...
- 3,102
6
votes
2
answers
583
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,121
1
vote
1
answer
110
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
4
votes
2
answers
247
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
0
votes
1
answer
205
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.]
...
- 13
4
votes
1
answer
239
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,225
2
votes
1
answer
108
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, ...
- 777
10
votes
1
answer
1k
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,812
4
votes
2
answers
399
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
2
votes
1
answer
124
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,375
28
votes
1
answer
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,812
7
votes
0
answers
452
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,812
10
votes
2
answers
651
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 ...
- 1,794