Grappling with semisimplicial types

[Tim Campion]

Dear HoTT Cafe denizens,

I've been trying to get my head around what the issue is with defining semisimplicial types in HoTT for awhile now, but I think I'm hampered by not actually having a good feel for what can and can't be done in a proof assistant. I hope this list is an appropriate place to try to air out some of the issues I've been having.

Question 0: In the following, am I missing the main point of what makes semisimplicial types difficult?

Scope:

Actually, I don't really care about semisimplicial types as such, I just want to be able to do higher category theory in HoTT. So let's set the more modest goal of defining (infinity,1)-categories in HoTT. Moreover, I don't understand type theory well enough to hope to make anything strict, so let's aim for a "fully coherent" version of (infinity,1)-categories, even if it means carrying around annoying explicit higher coherence data. And let's not worry about univalence -- I really mean "(inifnity,1)-precategories".

Misgivings about the conventional wisdom:

Now, I've heard it said that if this is our goal, then there's an "obvious approach": we ought to be able to "just" define the associahedra in HoTT; then we can define a category to be a graph equipped with a binary "composition" operation, equipped iteratively with paths filling in all of the associahedra. It would be kind of awful, but doable.

But I worry that the same issues would arise with this approach as with defining semisimplicial types themselves. After all, in the usual theory of A_infinity categories, one still has an underlying strict equality, and one asks for a strict algebroid for the A_infinity operad. So in order to do the analogous thing in HoTT, it seems to me that we would need to rig up our definition of the associahedra in such a way that the A_infinity operad has a multiplication satisfying associativity up to judgmental equality and so forth. This sounds as hard as if not harder than the original problem of defining semisimplicial types which satisfy the semisimplicial identities judgmentally. 

Question 1: Is the "obvious approach" really a non-starter?

Alternate approach:

I have a pet alternate idea, which is to use the "path" monad P, aka the "free category" monad. That is, we fix a type X, and let P be the monad on types over X x X which sends Y to the type x: X, y: Y |-> Sum_{n: N} Sum_{x_1,...,x_n: X} Y(x,x_1) x Y(x_1,x_2) x ... x Y(x_n, y).

Now, the issue with monads is that the coherences a monad should satisfy are exactly the coherences a simplicial type would need to satisfy, which is what we're trying to get our hands on in the first place. But my hope is that these coherences don't need to be spelled out explicitly -- they should all be satisfied judgmentally in the case of the particular monad P.

What we want to do is to define a category with objects X to be an algebra for the monad P, so we need to get a handle on what additional coherences an algebra for a monad should satisfy given that the monad is fully coherent. Let's ignore everything involving units for now. Then I still don't know exactly what these coherences are, but I'm optimistic that one needs only one cell in each dimension and that, crucially, the shape of the filler in each dimension is very simple: it's just a cube of that dimension. So we need a type Y : X x X -> Type, and then y_1: PY -> Y over X x X, and then y_2: y_1 mu = y_1 Py_1 where mu is the multiplication of the monad P, and then y_3 filling a certain 3-cube going from the 2-cube Py_2 to the 2-cube y_2, "and so forth". The main issues I can see are that

     A. One has to be careful to "globularize" one's cube in the most convenient way at each level, and then find a reasonable way to decompose the resulting pasting diagrams as a series of whiskerings and compositions. This sounds delicate, but hopefully doable given the controlled geometry.

     B. One needs to fill in some faces of cubes with coherence cells from the monad P -- for example, the cube filled by y_3 has an associativity square and a mu-naturality square on its boundary. But we've stipulated that coherences of monads are too complicated to understand directly. So it seems to be essential that all of the higher coherences of the monad P really do hold judgmentally so that we're saved the task of parametrizing them all by hand.

Question 2: Does anybody know if I'm correct in my hope that the higher coherences satisfied by an algebra for a monad are relatively straightforward to describe, modulo describing the higher coherences of the monad itself?

Question 3: Is it indeed the case that the path monad P has all the higher coherences you could want up to judgmental equality? (And is my intuition accurate -- if this is true, then we don't have to worry about describing them explicitly?)

Thanks,

Tim Campion

University of Notre Dame

[Ali Caglayan]

I have been thinking about asking a similar question for the last few days. The last time I saw it was discussed was on MO:

 https://mathoverflow.net/questions/145770/how-do-you-define-infinity-1-categories-in-homotopy-type-theory

Now that it has almost been 5 years since Mike posted that answer I think it would be nice if we can get some updates on the general ideas.

[Michael Shulman]

On Sun, Jun 24, 2018 at 3:17 PM, Tim Campion <tcam...@gmail.com> wrote:
> Now, I've heard it said that if this is our goal, then there's an "obvious
> approach": we ought to be able to "just" define the associahedra in HoTT;
> then we can define a category to be a graph equipped with a binary
> "composition" operation, equipped iteratively with paths filling in all of
> the associahedra. It would be kind of awful, but doable.
>
> But I worry that the same issues would arise with this approach as with
> defining semisimplicial types themselves. After all, in the usual theory of
> A_infinity categories, one still has an underlying strict equality, and one
> asks for a strict algebroid for the A_infinity operad. So in order to do the
> analogous thing in HoTT, it seems to me that we would need to rig up our
> definition of the associahedra in such a way that the A_infinity operad has
> a multiplication satisfying associativity up to judgmental equality and so
> forth. This sounds as hard as if not harder than the original problem of
> defining semisimplicial types which satisfy the semisimplicial identities
> judgmentally.

Yes, that seems exactly right to me. I think whoever gave you the
impression that this approach would be more doable was probably
mistaken.

> Question 2: Does anybody know if I'm correct in my hope that the higher
> coherences satisfied by an algebra for a monad are relatively
> straightforward to describe, modulo describing the higher coherences of the
> monad itself?

I'm not sure what you mean by "straightforward". I don't immediately
see a reason to believe that they would be any easier to describe in
finite syntax.

> Question 3: Is it indeed the case that the path monad P has all the higher
> coherences you could want up to judgmental equality? (And is my intuition
> accurate -- if this is true, then we don't have to worry about describing
> them explicitly?)

I don't see any reason to expect it to. Note that those ellipses in
your definition would have to be formalized in type theory using some
kind of type of lists, and concatenation of lists (of arbitrary
length) is not judgmentally associative.

[Tim Campion]

Thanks, Mike!

It's good to know that I wasn't going crazy regarding the associahedra, and also good to know that my understanding of inductive types was off.