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
1 vote
1 answer
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 ...
user avatar
2 votes
1 answer
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 ...
user avatar
  • 2,688
7 votes
1 answer
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. ...
user avatar
  • 73
3 votes
1 answer
107 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)$$ $$\...
user avatar
1 vote
1 answer
89 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}...
user avatar
2 votes
1 answer
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 ...
user avatar
  • 725
3 votes
0 answers
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 ...
user avatar
  • 1,666
0 votes
1 answer
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,...
user avatar
  • 3,156
2 votes
0 answers
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 ...
user avatar
  • 3,156
1 vote
0 answers
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 ...
user avatar
0 votes
1 answer
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$ ... ...
user avatar
2 votes
1 answer
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....
user avatar
7 votes
1 answer
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 ...
user avatar
6 votes
1 answer
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 ...
user avatar
4 votes
1 answer
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 ...
user avatar
4 votes
0 answers
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 ...
user avatar
3 votes
1 answer
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 "...
user avatar
0 votes
1 answer
93 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 $\...
user avatar
2 votes
0 answers
73 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 ...
user avatar
0 votes
0 answers
281 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 ...
user avatar
1 vote
1 answer
154 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?
user avatar
2 votes
1 answer
51 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,...
user avatar
  • 2,740
6 votes
2 answers
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 ...
user avatar
  • 1,091
1 vote
1 answer
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 ...
user avatar
  • 65
4 votes
2 answers
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 ...
user avatar
  • 65
0 votes
1 answer
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.] ...
user avatar
4 votes
1 answer
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 ...
user avatar
  • 1,165
2 votes
1 answer
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, ...
user avatar
  • 757
8 votes
1 answer
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 ...
user avatar
  • 3,612
4 votes
2 answers
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 : ...
user avatar
  • 41
2 votes
1 answer
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 ...
user avatar
  • 1,365
24 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 ...
user avatar
  • 3,612
7 votes
0 answers
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 ...
user avatar
  • 3,612
10 votes
2 answers
582 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 ...
user avatar
  • 1,774