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.
John Baez (Oct 20 2020 at 16:17):Ultimately it's a very simple thing: a space (or infinity-groupoid, or simplicial set, or homotopy type) where there's a multiplication that's associative up to homotopy, with the homotopy obeying all the rules you could imagine, up to homotopy, etc.
John Baez (Oct 20 2020 at 16:18):And such a thing is best defined inside a similar thing.
Dan Doel (Oct 20 2020 at 16:18):Probably not well. It looks like it'd have the same unknowns as defining an -category.
John Baez (Oct 20 2020 at 16:20):Yes, there's a nice discussion on Michael Harris where Jacob Lurie says he doesn't think homotopy type theory solves this sort of problem (yet).
John Baez (Oct 20 2020 at 16:21):Riehl and Verity's "synthetic theory of -categories" may be a better way to go.
Dan Doel (Oct 20 2020 at 16:22):Basically there's no way of writing down "and ever so on," and no known finitary description, I think.
John Baez (Oct 20 2020 at 16:33):I'm not sure what you mean by "finitary description". You can certainly write down a precise formula of finite length that describes how it goes on forever; every good homotopy theorist or n-category theorist knows at least one way to do this.
Dan Doel (Oct 20 2020 at 16:33):Part of it might be that the sorts of 'descriptions' you can use are artificially limited, and there are ways that can be relaxed, but they're not widely adopted. However, I think there are additional unknowns about what sorts of "higher" stuff should actually be allowed.
Dan Doel (Oct 20 2020 at 16:36):The inductive definitions used in HoTT and other implemented type theories are based on e.g. Haskell, where you have to write down all the constructors and whatnot in a finite source file. There is no way to compute the description of the inductive type. So, unless you can find an alternate characterization of the "and so on" in terms of finitely many (higher) constructors, there's no way to write it down in that framework.
Dan Doel (Oct 20 2020 at 16:38):Or if you can do it in some other way than a direct definition of that sort. Like, there's no way to write down all n-spheres that way, but you can instead define them all as the n-fold suspension or something, by recursion on n.
John Baez (Oct 20 2020 at 16:38):You're taking a more computational view than I do. How is what you're saying fundamentally different from the fact that we can't write a program that prints out all the natural numbers? We have a systematic procedure, but it can never run to completion.
John Baez (Oct 20 2020 at 16:40):I'm not trying to be snarky, I'm trying to get what you're saying.
Dan Doel (Oct 20 2020 at 16:50):I don't see how you can not take a 'computational' approach to what definitions are allowed or not in a particular formal system, which is the 'problem' with defining -categories in HoTT.
Dan Doel (Oct 20 2020 at 16:52):It's not good enough to say that there is a systematic (meta-)procedure for writing down all the coherences necessary to define one, because there is no formal rule for defining a type based on such a (meta-)procedure.
Jacques Carette (Oct 20 2020 at 16:52):At some level, what is going on is that internalizing mathematician's use of "..." in definitions is very hard.
Jacques Carette (Oct 20 2020 at 16:53):Especially when you're in the middle of defining something, and you're at the same time implicitly defining another part using "...". That kind of definitional recursion at the level of definitions gets tricky very quickly.
Dan Doel (Oct 20 2020 at 16:53):It'd be like an ω-rule. I mean, the approach I mentioned is related to not being so limited, and allowing internally definable 'procedures' to introduce types, but that is not how most formal systems implemented today work.
Jacques Carette (Oct 20 2020 at 16:55):For example: the notion of 'homomorphism' is well understood, so well that humans pattern match on structure definitions and write out the obvious notion of homomorphism thus induced. Right now, there are no formal systems (outside of a couple of prototypes that I've written) that internalize this. In large part because you're just not allowed to fold over syntax and then reify the result as a new definition at the top level.
Dan Doel (Oct 20 2020 at 17:02):I guess a really simple example is: data ℕ where Zero ; Suc : ℕ -> ℕ is a valid inductive definition. data ℕ where 0 : ℕ ; 1 : ℕ ; 2 : ℕ ; ... is not a valid inductive definition, even though there is a systematic procedure for outputting it. The problem is that no one knows how to define an -category except in the latter way.
Jacques Carette (Oct 20 2020 at 17:10):Exactly!
Shea Levy (Oct 20 2020 at 17:12):I've often wanted to implement something like the calculus of inductive constructions but where inductive types are first class, in that you can construct them as normal terms, return them from functions, etc... If that doesn't lead to inconsistency, maybe you can just make it so the constructor list is allowed to be infinite and this would be OK? Not sure how you'd eliminate such a type though, unless you just do a wildcard after some point.
Dan Doel (Oct 20 2020 at 17:13):There is work on that kind of thing. This for instance.
Dan Doel (Oct 20 2020 at 17:14):I'm not sure about actual infinite lists of constructors, though.
Dan Doel (Oct 20 2020 at 17:15):That paper is just the beginning, really. I think there's been considerably more done since then.
Shea Levy (Oct 20 2020 at 17:15):Actually I guess you'd want your case statement to be a function from ctor index to case, so you could still do it infintely?
Dan Doel (Oct 20 2020 at 17:18):Anyhow, there are basically two steps, I guess. The first is internalizing the notion of a 'description' of one of these types, so that you can define a description in terms of arbitrary other objects in the theory. The second is adding additional valid descriptions that wouldn't have even made sense before that.
Jacques Carette (Oct 20 2020 at 17:19):If my memory serves me right 'matita' had a variant of CIC that allowed that.
Dan Doel (Oct 20 2020 at 17:21):I.E. you can't have an ω-rule-type until you have internalized things so that you can have an ω-description in the theory. But most implementations aren't even there yet. And also, people have to figure out what ω-rules make sense. :)
Dan Doel (Oct 20 2020 at 17:25):I guess it's not just inductive types, though. For instance, there's a paper on the elimination principle for propositional truncation that shows that you can eliminate into any type via a 'coherently constant' map. However, I don't think anyone knows how to write down 'coherently constant' in HoTT, for similar reasons.
Dan Doel (Oct 20 2020 at 17:27):There is a systematic way of writing down the coherence conditions, but not an obvious internal way.