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 ...
Simon Henry's user avatar
  • 39.9k
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 ...
Mike Shulman's user avatar
  • 64.7k
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 ...
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 ...
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 ...
Mike Shulman's user avatar
  • 64.7k
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 ...
Noah Snyder's user avatar
  • 27.8k
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 ...
Mike Shulman's user avatar
  • 64.7k
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 ...
Andrej Bauer's user avatar
  • 47.5k
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 ...
Mike Shulman's user avatar
  • 64.7k
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 ...
Mike Shulman's user avatar
  • 64.7k
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 ...
Mike Shulman's user avatar
  • 64.7k
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 ...
Mike Shulman's user avatar
  • 64.7k
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 ...
Peter LeFanu Lumsdaine's user avatar
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 ...
Peter LeFanu Lumsdaine's user avatar
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 ...
Peter LeFanu Lumsdaine's user avatar
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: ...
Zhen Lin's user avatar
  • 14.9k
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 ...
Mike Shulman's user avatar
  • 64.7k
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 ...
Maximilian Doré's user avatar
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 ...
Andrej Bauer's user avatar
  • 47.5k
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 $...
Noah Snyder's user avatar
  • 27.8k
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$, ...
Mike Shulman's user avatar
  • 64.7k
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 ...
Mike Shulman's user avatar
  • 64.7k
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 ...
Peter LeFanu Lumsdaine's user avatar
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 ...
Mike Shulman's user avatar
  • 64.7k
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 ...
Mike Shulman's user avatar
  • 64.7k
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 ...
Ivan Di Liberti's user avatar
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 ...
Andrej Bauer's user avatar
  • 47.5k
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 ...
Neil Strickland's user avatar
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 ...
David Corfield's user avatar
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 ...
Mike Shulman's user avatar
  • 64.7k

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