You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Leopold Schlicht (Aug 17 2021 at 17:12):As far as I can see, the HoTT book gives two applications of higher inductive types in normal (i.e., non-homotopical) math: the construction of the Cauchy reals and the construction of the surreal numbers. Both definitions use the principle of "inductive-inductive" definitions as well. I wonder: Is this really an application of higher inductive types? After all, both definitions contain only point and path constructors, but not any homotopy constructors. So would both definitions also work in, say, a type theory with a notion of "quotient type" and inductive-inductive definitions?
Also, aren't Theorem 11.3.9 and Corollary 11.6.5 (stating that these types are sets) trivial in some sense, because both definitions contain only point and path constructors, but not any homotopy constructors?
The introduction to chapter 6 gives an explanation of the phenomenon of an inductive type being a higher groupoid while being defined only using point and path constructors: if the domain of some constructor has higher paths, these will carry over. But if all domains of all constructors are sets, I believe this can't happen. Do Theorem 11.3.9 and Corollary 11.6.5 also fall in some class of higher inductive types that yield sets "for trivial reasons"?
Reid Barton (Aug 17 2021 at 17:15):What's the difference between a "path constructor" and a "homotopy constructor"?
Reid Barton (Aug 17 2021 at 17:27):It seems like the circle-as-inductive-type (section 6.4) is a counterexample to your claim, right?
Leopold Schlicht (Aug 17 2021 at 17:37):I call the things between points "paths" and the things between paths "homotopies" (but not "paths" anymore).
I don't know what claim you are referring to, because I asked a lot of things. :-)
Reid Barton (Aug 17 2021 at 17:39):I mean the last one "But if all domains of all constructors are sets, I believe this can't happen."
James Wood (Aug 17 2021 at 20:45):IIRC, you can recover a similar theorem if you prove that the path constructors are cycle-free. That is, consider a higher inductive type T generated from constructors point : P → T and path : (x y : P) → R x y → point x = point y, where P : Set and R : P → P → Prop. Then, if R is cycle-free in some suitable graph-theoretic sense, T will be a set. The circle fails the latter condition in the simplest way possible – the whole idea of the circle is that the path forms a cycle.
I'd appreciate a reference, if anyone knows one, because it's not immediately clear to me how it works when P has large cardinality and cycle-free paths can be infinitely long.
James Wood (Aug 17 2021 at 20:54):For the broader question, quotient inductive-inductive types have been studied. As far as I can tell, the Cauchy reals are a prime motivating example, along with similar cases where QIITs are enough to get around countable choice.