71
votes

Accepted

### Why did Voevodsky consider categories "posets in the next dimension", and groupoids the correct generalisation of sets?

First, there is indeed nothing mathematically very deep in this observation, and I agree that the word "breakthrough" might be exaggerated. But on the other hand lots of very deep ideas look trivial ...

41
votes

### Why did Voevodsky consider categories "posets in the next dimension", and groupoids the correct generalisation of sets?

The other answers are quite good and nothing is wrong with them, but lest a wrong impression be given (e.g. by the implicit suggestion that the idea of "categories as sets in the next dimension" in ...

39
votes

### Vladimir Voevodsky's works

Perhaps one of the biggest ideas that VV was pursuing is the Initiality Conjecture for Martin-Löf type theory (with universes). A rough idea is that from the rules for a type theory, one can define a ...

Community wiki

29
votes

### Vladimir Voevodsky's works

Aside from his work on the foundations of mathematics, which others have already elaborated on, earlier in his career Voevodsky also proved the Milnor conjecture in algebraic geometry. The Milnor ...

Community wiki

29
votes

### Defining $SU(n)$ in HoTT

I think Noah's answer is mostly right, but partly misleading, and explaining why will take too much space for a comment, so I'm posting a separate answer.
As Noah says, the main conceptual point is ...

26
votes

Accepted

### Defining $SU(n)$ in HoTT

This isn't easy to do, and the reason it isn't easy is because of the step "$\infty$-groupoids are the same thing as spaces." Of course the homotopy hypothesis tells you that any $\infty$-groupoid ...

25
votes

Accepted

### Deligne's doubt about Voevodsky's Univalent Foundations

It is a bit difficult to understand what he is asking. The already-linked nForum discussion includes some clarification about his example, which at the meeting took us a while to figure out.
More ...

25
votes

Accepted

### Formal definition of homotopy type theory

Here are some resources:
The appendix of the homotopy type theory book gives two formal presentations of homotopy type theory.
Martín Escardó wrote lecture notes Introduction to Univalent Foundations ...

22
votes

Accepted

### Constructive homological algebra in HoTT

As regards HoTT, my own current opinion is that the best way to do "homological algebra" therein is by working directly with spectra.
With only a working mathematician's knowledge of homological ...

21
votes

### Role of univalence in homotopy group calculations

"Isomorphic structures are equal" is a cute slogan, but it sometimes gets in the way because it sounds like it's saying that it forces isomorphic structures to be related by the pre-existing ...

21
votes

Accepted

### Coinduction for all?

This is a question that I've puzzled about myself, and I don't pretend to have The Answer. But here's one thought that I've found illuminating. Let's start by comparing the behavior of induction and ...

19
votes

Accepted

### What kind of category is generated by Cubical type theory?

There are two kinds of answers as to what kind of category a "homotopy type theory" is the internal language of. On the one hand there is a kind of $(\infty,1)$-category that is the semantic object ...

19
votes

### Formal definition of homotopy type theory

Andrej’s answer gives an excellent list of resources. But I think it’s also worth saying a little upfront to ward off common misunderstandings. HoTT is a foundational system — analogous to ZFC set ...

18
votes

Accepted

### The role of univalence in the homotopy interpretation of type theory

Whenever you’re looking at a logical system, there’s a tension between two main ways of studying it:
axioms/theorems in the system show what the world it describes must look like;
models show what ...

17
votes

Accepted

### Why are W-types called "W"?

You write:
Probably "W" means either "wellordered" or "wellfounded". […] But these are notions associated to order theory, whereas W-types don't directly have to do with ...

16
votes

Accepted

### Why the reflection rule trivializes higher paths in Martin-Löf Extensional Type theory?

The point is that the reflection rule makes $p = \mathsf{refl}_x$ a well-formed expression. This turns out to be incredibly dangerous: now we can prove it by induction on equality.
More precisely:
...

16
votes

### Can Homotopy Type Theory or algebraic geometry deal with homotopy fibers in terms of families?

I am answering your "later addon" only, although it seems actually to be a very different question than your original one.
This is perhaps one of the most misunderstood aspects of HoTT and ...

16
votes

Accepted

### 3 questions about basics of Martin-Löf type theory

Universe levels usually trip up newcomers to type theory since there is no straightforward intuition for them. What I found helpful is to think of them as a merely technical device to prevent ...

15
votes

Accepted

### Homotopy type theory: Are the hierarchy of Type_k universes isomorphic?

This question is about type theory in general and is not specific to homotopy type theory. $\newcommand{\Type}{\mathtt{Type}}$
The thing you are missing is that a universe $\Type_k$ contains very ...

15
votes

Accepted

### Role of univalence in homotopy group calculations

Let's start with an easier question: How do we know that loop is not equal to refl in $\pi_1(S^1)$?
By the universal property of $S^1$ this is exactly saying that there exists some type $T$ and some $...

14
votes

### Can Homotopy Type Theory or algebraic geometry deal with homotopy fibers in terms of families?

Here is an answer to your original question in the context of HoTT. An arbitrary map $f:X\to Y$ that isn't a fibration can't be viewed literally as a family of spaces varying continuously over $Y$, ...

13
votes

Accepted

### Are there types with nontrivial paths in all dimensions? (HoTT)

$\prod_{n\in\mathbb{N}} S^n$ certainly has nontrivial structure at all levels (i.e. "is not a homotopy $n$-type for any finite $n$"). In classical homotopy theory, even $S^2$ by itself has nontrivial ...

13
votes

Accepted

### HoTT without Funext, Univalence

“HoTT” isn’t generally currently considered as referring to a single specific formal system — it’s a similar situation to, say, “constructive mathematics”, for which there are various different more ...

13
votes

### Practical example in using (homotopy) type theory

The answers and comments on this question show that there is still a ton of misinformation out there about HoTT.
The short answer (but much more time-consuming for you) is that you should read the ...

13
votes

### Practical Benefits of HTT/univalent foundations for assisted proofs

You didn't specify exactly what "claimed benefits" for non-univalent type theory in general you're referring to, and I happen to believe that even non-univalent type theory does have ...

12
votes

### Why did Voevodsky consider categories "posets in the next dimension", and groupoids the correct generalisation of sets?

Even if this answer can be seen as an expansion of the last two lines of Simon's answer, it does not really come in the same spirit.
From the point of view of enriched category theory, posets are ...

12
votes

Accepted

### Explicit different proofs of the same identity type in MLTT

Martin-Löf type theory contains no such type because it is consistent with uniqueness of identity proofs which states precisely that what you are looking for is not there.
Martin-Löf type theory is ...

12
votes

Accepted

### Defining rational numbers without using quotients or 0-truncations

One version of the theory of continued fractions is as follows. We can define operations $S,T,J\colon\mathbb{Q}^+\to\mathbb{Q}^+$ by $S(x)=x+1$ and $J(x)=1/x$ and $T(x)=JSJ(x)=x/(x+1)$, then we can ...

11
votes

### Stable homotopy type theory?

With respect to the first question, expanding on my comment which pointed out the nLab page dependent linear type theory and the article by Urs Schreiber, 'Quantization via Linear homotopy types', I'd ...

11
votes

Accepted

### Uniqueness Principle for function types

It is not true "by construction". Remember that at this point in the theory a "function" is an abstract undefined thing, not something "defined by its action on inputs" as it is in set theory. The ...

Only top scored, non community-wiki answers of a minimum length are eligible

#### Related Tags

homotopy-type-theory × 133lo.logic × 52

type-theory × 50

ct.category-theory × 25

homotopy-theory × 22

at.algebraic-topology × 18

foundations × 18

higher-category-theory × 16

infinity-topos-theory × 12

reference-request × 9

soft-question × 8

constructive-mathematics × 7

cohomology × 4

computer-science × 4

infinity-categories × 4

ag.algebraic-geometry × 3

real-analysis × 3

topos-theory × 3

mathematical-philosophy × 3

groupoids × 3

set-theory × 2

gn.general-topology × 2

homological-algebra × 2

computability-theory × 2

simplicial-stuff × 2