Timeline for The role of univalence in the homotopy interpretation of type theory
Current License: CC BY-SA 3.0
17 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 8, 2017 at 15:54 | comment | added | Mike Shulman | 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. | |
| Sep 8, 2017 at 15:51 | comment | added | Mike Shulman | @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.) | |
| Sep 8, 2017 at 10:41 | comment | added | David Roberts♦ | @Michael sorry, got the wrong idea. I'm not sure, I don't know enough about plain MLTT. | |
| Sep 8, 2017 at 10:16 | comment | added | Michael Bächtold | @DavidRoberts thanks, but I'm still wondering about MLTT and not ZF(C). So is MLTT without univalence also a foundation for mathematics? | |
| Sep 8, 2017 at 10:13 | comment | added | David Roberts♦ | @Michael clearly not, since, modulo size issues, ZF(C) is a foundation after all. The idea is to make the formalisation more 'natural'. If you know how Bourbaki tried to treat his concept of structure in (his version of) set theory, you can see how awkward it can get, and that's without formalisation. | |
| Sep 8, 2017 at 8:53 | comment | added | Michael Bächtold | @DavidRoberts, but suppose we use MLTT and not ZF, is there a theorem at the 2- and 3- category level that we cannot state or prove without univalence? | |
| Sep 8, 2017 at 8:07 | comment | added | Peter LeFanu Lumsdaine | @PhilippeGaucher: there may well be models of ZF(C) where sets are interpreted as spaces in some non-trivial way; if you generalise to constructive set theories like IZF, there certainly are such models. But there can’t be models where “sets are homotopically non-trivial spaces, and equality is path-spaces”, because the first-order logic formulation of all these set theories forces equality in them to be a “mere proposition”. | |
| Sep 8, 2017 at 8:02 | comment | added | Peter LeFanu Lumsdaine | @MikeShulman: §4.8 of the HoTT Book develops how the univalent universe is an object classifier, in a type-theoretic sense that’s clearly somewhat analogous to the ∞-categorical sense of that term. But it’s not making the connection with the ∞-categorical setting precise in any way, which is what I was meaning in the answer. | |
| Sep 8, 2017 at 7:56 | comment | added | David Roberts♦ | @MichaelBächtold the idea is to be able to capture mathematics that is invariant under isomorphism or more generally equivalence and higher equivalence (VV was after all working at the 2- and 3-category level on the rather complicated results that starting giving him concerns regarding verification for correctness). Formal verification systems that are built on ZF, say, don't have this built in. | |
| Sep 8, 2017 at 7:33 | comment | added | Philippe Gaucher | I have a stupid question (it is good enough for a comment I hope): can we prove that there does not exist any model of ZFC interpreting sets as non-trivial spaces (I mean non-discrete) ? | |
| Sep 8, 2017 at 7:30 | comment | added | Michael Bächtold | "because pragmatically one often needs..." Does that mean that univalence is strictly speaking not necessary for formalising what can be found in say UniMath library? It only makes proofs shorter? | |
| Sep 8, 2017 at 3:19 | comment | added | Mike Shulman | Also, FWIW, one sense in which the universe is an object classifier is proven in section 4.8 of the book. | |
| Sep 8, 2017 at 3:18 | comment | added | Mike Shulman | Specifically: if HITs exist and can eliminate into univalent universes, then the HITs are not in general sets; if a univalent universe contains a type with a nontrivial automorphism like bool or nat, then it is not a set; and Kraus and Sattler showed that the nth nested universe is not an n-type. One univalent universe (of propositions only, i.e. a subobject classifier) can exist even if all types are sets. | |
| Sep 7, 2017 at 21:11 | comment | added | Peter LeFanu Lumsdaine | @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. | |
| Sep 7, 2017 at 18:34 | vote | accept | coconut | ||
| Sep 7, 2017 at 18:33 | comment | added | Simon Henry | 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. | |
| Sep 7, 2017 at 18:14 | history | answered | Peter LeFanu Lumsdaine | CC BY-SA 3.0 |