Category Theory
Zulip Server
Archive

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.

Stream: theory: type theory

Topic: higher inductive types

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.

Mike Shulman (Aug 18 2021 at 19:36):

Reference: https://arxiv.org/abs/1612.02346

Mike Shulman (Aug 18 2021 at 19:37):

Note that the Cauchy reals and surreals are not just a combination of quotient types with ordinary inductive-inductive types; it matters greatly that the quotienting is part of the inductive definition. In particular, both quotients and ordinary inductive-inductive definitions exist in ZF, but quotient inductive types don't in general.

Mike Shulman (Aug 18 2021 at 19:38):

I don't think I've ever heard this result about cycle-freeness, but it sounds possible.

Mike Shulman (Aug 18 2021 at 19:40):

The example of the circle might suggest that at least a HIT with only 0- and 1-dimensional constructors whose domains are all sets ought to be a 1-type. In higher dimensions the analogous fact becomes wildly false, e.g. the 2-sphere has only 0-, 1-, and 2-dimensional constructors, but is certainly not a 2-type or even an n-type for any finite n. The 1-dimensional case is true classically, and also in every Grothendieck-Lurie $(\infty,1)$-topos, but I believe it's still an open question in constructive HoTT whether, for instance, the suspension of a set is always a 1-type.

Steve Awodey (Aug 19 2021 at 02:49):

Leopold Schlicht said:

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"?

Two further applications are (set) quotients by equivalence relations and Eilenberg-MacLane spaces. Propositional truncation is also "normal" math - it's just saying that a set is non-empty.

Mike Shulman (Aug 19 2021 at 04:01):

EM-spaces aren't exactly non-homotopical math. (-: But the cumulative hierarchy in chapter 10 is another non-homotopical example.

Ulrik Buchholtz (Aug 19 2021 at 06:37):

I would count Rezk completion as non-homotopical math (but I protest the identification “normal math = non-homotopical”).
More generally, using HITs (pushouts will do), we get the type-theoretical replacement principle, which gets us resized set quotients, classifying spaces of groups, Rezk completions, etc.

Mike Shulman (Aug 19 2021 at 14:42):

Rezk completion is an interesting borderline case.

Leopold Schlicht (Aug 21 2021 at 18:42):

Really enlightening discussion, thanks a lot!
Mike Shulman said:

In particular, both quotients and ordinary inductive-inductive definitions exist in ZF, but quotient inductive types don't in general.

Do they exist in ZFC?
Ulrik Buchholtz said:

More generally, using HITs (pushouts will do), we get the type-theoretical replacement principle, which gets us resized set quotients, classifying spaces of groups, Rezk completions, etc.

What is the type-theoretical replacement principle? Does this have something to do with the replacement axiom in set theory?

Mike Shulman (Aug 22 2021 at 00:06):

Yes, "all" HITs exist in ZFC. There's a construction using transfinite recursion in my paper with Peter Lumsdaine, Semantics of higher inductive types.

I say "all" because there isn't really yet a universally-accepted definition of "the class of HITs" -- different people have given different schemas, and we proved that all instances of one schema exist, but that isn't a priori the same as the other schemas, although I expect that similar methods should work for other schemas. In particular our schema doesn't explicitly include higher inductive-inductive types, but I have little doubt that they exist too.

Ulrik Buchholtz (Aug 22 2021 at 08:08):

Leopold Schlicht said:

What is the type-theoretical replacement principle? Does this have something to do with the replacement axiom in set theory?

It says the following, where we're fixing a universe $\mathcal{U}$: Suppose we have a map $f: A \to B$, where $A$ is $\mathcal{U}$-small and $B$ is locally $\mathcal{U}$-small (meaning: its identity types are essentially $\mathcal{U}$-small). Then the image of $f$ is essentially $\mathcal{U}$-small (meaning: equivalent to a type in $\mathcal{U}$).
It holds whenever $\mathcal{U}$ is a univalent universe closed under pushouts, as a consequence of Egbert Rijke's join construction.
A relation to the axiom in set theory is via the following: If $A$ and $B$ are sets with $A$ in $\mathcal{U}$, and we assume propositional resizing so that all propositions are essentially $\mathcal{U}$-small, then it implies that the image of any map $f : A \to B$ is essentially $\mathcal{U}$-small.
That doesn't indicate a formal relationship, though, but it does indicate a certain similarity.

Cody Roux (Aug 22 2021 at 14:55):

This is the type-theoretic formulation? I shudder to think of the category-theoretic one...