Skip to main content

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
0 votes
0 answers
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 ...
RataMágica's user avatar
0 votes
1 answer
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 ...
fweth's user avatar
  • 3,574
2 votes
1 answer
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 ...
fweth's user avatar
  • 3,574
14 votes
3 answers
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:...
D.R.'s user avatar
  • 8,805
5 votes
1 answer
157 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}(...
IsAdisplayName's user avatar
1 vote
1 answer
145 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. ...
Mark's user avatar
  • 45
1 vote
1 answer
108 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 ...
IsAdisplayName's user avatar
4 votes
1 answer
222 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 ...
user1892304's user avatar
  • 2,828
8 votes
2 answers
463 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. ...
TJM's user avatar
  • 83
3 votes
1 answer
186 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)$$ $$\...
Jordan Mitchell Barrett's user avatar
3 votes
1 answer
212 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}...
Derive Foiler's user avatar
2 votes
1 answer
118 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 ...
JRC's user avatar
  • 526
3 votes
0 answers
80 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 ...
Student's user avatar
  • 1,822
2 votes
1 answer
197 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,...
Lance's user avatar
  • 3,708
2 votes
0 answers
278 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 ...
Lance's user avatar
  • 3,708
2 votes
0 answers
90 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 ...
DrunkCoder's user avatar
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$ ... ...
DrunkCoder's user avatar
2 votes
1 answer
94 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....
Atticus Stonestrom's user avatar
7 votes
1 answer
271 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 ...
Atticus Stonestrom's user avatar
6 votes
1 answer
255 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 ...
Atticus Stonestrom's user avatar
6 votes
1 answer
171 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 ...
Atticus Stonestrom's user avatar
4 votes
0 answers
81 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 ...
Atticus Stonestrom's user avatar
3 votes
1 answer
246 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 "...
Lawrence's user avatar
0 votes
1 answer
119 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 $\...
Patrick Stevens's user avatar
2 votes
0 answers
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 ...
Brandon Brown's user avatar
0 votes
0 answers
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 ...
user514014's user avatar
1 vote
1 answer
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?
user583563's user avatar
2 votes
1 answer
64 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,...
fweth's user avatar
  • 3,574
6 votes
2 answers
846 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 ...
hawkeye's user avatar
  • 1,131
1 vote
1 answer
119 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 ...
Philipp's user avatar
  • 65
4 votes
2 answers
288 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 ...
Philipp's user avatar
  • 65
0 votes
1 answer
226 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.] ...
user642291's user avatar
4 votes
1 answer
302 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 ...
Perry Bleiberg's user avatar
2 votes
1 answer
110 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, ...
Phil-W's user avatar
  • 841
12 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 ...
Nethesis's user avatar
  • 3,986
4 votes
2 answers
437 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 : ...
wert's user avatar
  • 41
2 votes
1 answer
125 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 ...
Kevin Quirin's user avatar
  • 1,395
30 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 ...
Nethesis's user avatar
  • 3,986
7 votes
0 answers
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 ...
Nethesis's user avatar
  • 3,986
11 votes
2 answers
714 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 ...
tharris's user avatar
  • 1,804