Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [univalent-foundations]

The tag has no usage guidance.

1
vote
0answers
51 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
136 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
99 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
40 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,...
5
votes
2answers
77 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
51 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
145 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
103 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.] ...
3
votes
1answer
171 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
vote
1answer
82 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, ...
6
votes
1answer
527 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
251 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
102 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 ...
20
votes
1answer
1k 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
343 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
417 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 ...