11
$\begingroup$

In Martin-Löf type theory with identity eliminator

$$ J : \prod_{B:\prod_{x,y:A}(x=y)\to\mathcal{U}}\left( \prod_{x:A}B(x,x,\mathrm{refl}_x)\to \prod_{x,y:A}\prod_{p:x=y}B(x,y,p) \right) $$

satisfying $J(B,b,x,x,\mathrm{refl}_x)=b(x)$ we can have terms $p:x=x$ that are not equal to $\mathrm{refl}_x$.

We can then interpret the $x:A$ as points of a space, and the terms of $x=y$ as the paths joining $x$ and $y$. The loops $p:x=x$ that are not $\mathrm{refl}_x$ are interpreted as non-contractible loops. Terms of type $p=_{x=y}q$ are homotopies between paths, etc.

Now, I have seen that the univalence axiom is of great importance in homotopy type theory, but I don't see how it enters in this discussion. The question is: does univalence have consequences in the homotopy interpretation of type theory?

If the answer is yes, what role does it play?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
18
$\begingroup$

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 the world it describes can look like.

The interpretation of types as spaces shows that the types of plain Martin-Löf type theory can look like homotopically non-trivial spaces (unlike e.g. the sets of ZF(C), which are always homotopically discrete).

However, in plain Martin-Löf type theory, you can’t prove that there must exist homotopically non-trivial types. It’s consistent that every type “is a set”, in the sense of being homotopically discrete. This follows from the fact that you can also model types as plain old sets, in ZF(C) or any similar theory.

Univalence implies that there must exist homotopically non-trivial types. Specifically, once you add both univalence and higher inductive types, then (as shown in the HoTT book, and various papers on synthetic homotopy theory) you can reproduce many standard constructions of spaces from classical homotopy theory, and show that they behave how you’d expect them to in many ways: e.g. that the fundamental group of the circle is $\mathbb{Z}$, just to name the simplest non-trivial such fact.

So from the point of view of the homotopy interpretation of type theory, the rôle of univalence is ensuring that enough homotopically non-trivial types exist for the world to look like a reasonable homotopy-theoretic world. One approach to making this precise is to say that univalence should force the universe (or a hierarchy of universes, or something) to be an object classifier (or classiying family, or something) in the sense of Lurie’s ∞-topos theory — though this idea hasn’t been made precise yet.

This isn’t the only rôle of univalence: it’s not Voevodsky’s original motivation, for example. That was roughly, as I understand it, to allow more powerful and natural reasoning about how constructions respect equivalence, because pragmatically one often needs to use such reasoning when formalising mathematics in type theory. But it’s the essential rôle that univalence plays from the point of view of the homotopy-theoretic interpretation.

Improve this answer
$\endgroup$
15
  • 2
    $\begingroup$ I would add that the univalence for a single universe alone is not enough to get a real homotopy theoretic feel: One can imagine a model where general type are groupoids, but small types are sets ($h$-sets) and the Universe is the groupoids of sets and isomorphisms between them. This will satisfies univalence but have almost no homotopy theoretic contents. This is really (as you pointed out) the interaction between higher inductive type and univalence which forces to have interesting homotopy theoretic content. Having a full hierarchy of universe all univalent also do the trick. $\endgroup$
    – Simon Henry
    Sep 7, 2017 at 18:33
  • $\begingroup$ @SimonHenry: Yes, absolutely — “a univalent universe” means almost nothing until you specify what type-constructions you’re assuming the universe is closed under, and this is something people are often very vague about (as I was here). To get a homotopically rich universe, you want closure under at least M-L’s original constructors, plus some HIT’s — e.g. pushouts is enough to go along way. Or, as you say, a hierarchy — i.e. univalent universes that contain other univalent universes. $\endgroup$
    – Peter LeFanu Lumsdaine
    Sep 7, 2017 at 21:11
  • 1
    $\begingroup$ @DavidRoberts thanks, but I'm still wondering about MLTT and not ZF(C). So is MLTT without univalence also a foundation for mathematics? $\endgroup$
    – Michael Bächtold
    Sep 8, 2017 at 10:16
  • 2
    $\begingroup$ @MichaelBächtold plain MLTT can be used as a foundation for mathematics, but it's a bit annoying because, among other things, it lacks propositional truncation, function extensionality, and propositional extensionality. Thus, often people using it as a foundation are forced to build mathematics out of "setoids" rather than types. For set-level mathematics, this is tedious and annoying but mostly works; but when you start doing higher-categorical mathematics, it gets problematic, and you start feeling forced towards a more HoTT-like approach. (I hope this is a fair characterization.) $\endgroup$
    – Mike Shulman
    Sep 8, 2017 at 15:51
  • 2
    $\begingroup$ There are certainly theorems in HoTT about categories (and 2-categories and 3-categories) that we can't prove without univalence; see for instance chapter 9 of the book. $\endgroup$
    – Mike Shulman
    Sep 8, 2017 at 15:54

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.