-
Notifications
You must be signed in to change notification settings - Fork 189
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Project: coherence for monoidal categories #1896
Comments
Interesting idea. Do we expect to have applications? In my non-univalent work with monoidal categories, all diagrams that arose could be factored into the basic commuting regions in a pretty obvious way, so I never needed to appeal to the general theorem. Comments: In your HIT, I think you forgot a point constructor I also think that the paths introduced in the HIT will be a problem. A functor from that HIT will have to take
I don't think this is the correct universal property. Currently |
Yes, I have found the same to be true. I did wonder however if we can get a proof assistant to do this for us which is where I came across this idea.
Yes, I did forget it, thanks.
That's a very good point. I suppose then this would only work on categories where the Rezk completion is an equivalence. That would mean that pType and Type would be covered. I think we could probably come up with some pathological counter examples in general, but my view was towards the obvious univalent examples. I guess we can't expect to have a coherence theorem for non-univalent monoidal categories since these aren't quite categories from a semantic point of view.
Yes, that needs correcting. I guess overall this might not turn out to be very useful in practice. Mainly due to the reason that univalence is nice, but is not great at giving easy to work with examples. I guess it can be thought of as a meta-theoretic statement that the definition of monoidal categories that we have is correct in some sense. It would be interesting to know if parts of the argument can be loosened to encompass more general wild categories, but that's probably not a good use of time. |
I think coherence for non-univalent monoidal categories should work just like coherence for ordinary monoidal categories in set theory. Just add isomorphisms instead of equalities, as Dan said. You can't do this wrapped up in a single HIT, but you should be able to use inductive types to define a free (pre/wild) category generated by certain operations. |
I agree with Mike. The coherence really just amounts to cutting a diagram into primitive regions matching the axioms, so it shouldn't rely on univalence. |
In this issue I will sketch out a multistep project that we can carry out over time. It consists of multiple little pieces but it should be relatively straightforward to do. I will occasionally contribute to the completion, but I encourage others to have a go if they are interested.
Introduction
One of the remarkable things about monoidal categories are that the axioms are enough to say that any diagram involving only tensors, unitors and associators commutes. This is an easy thing to claim but in practice it involves coming up with an algorithm that will fill our homotopy. I've worked with monoidal categories in the past on paper and I don't think I ever fully appreciated the work that goes into proving this. What I will sketch here is a way for us to prove it and use it practically.
Free monoidal categories
In order to formalise the notion of a diagram consisting only of tensors, unitors and associators we need a notion of "free monoidal category" luckily, this becomes something easily stateable in HoTT. A free monoidal category is essentially an higher inductive type that looks like the following:
Now this HIT is quite complicated but it should be possible to construct straight out of GraphQuotients. For the time being I think it would be best just to define this as a private inductive type since this is really an orthogonal metatheoretic consideration.
This HIT can be easily checked to be a monoidal category and will be useful later.
"Normalised" free monoidal categories
Another kind of monoidal category we will consider is that where the morphisms are normalised. By this I mean that the associators have been applied so that they are bracketed in only one way. Remarkably, we don't actually need a HIT to construct such an object as
list X
has all the structure we need.Forgetting monoidal categories for the moment and focusing only on monoids,
list X
can be thought of as the free monoid on a typeX
. The product comes from list concatenation and it can be easily verified to satisfy the monoid axioms baring truncation.The same situation applies for monoidal categories, here we will remove the truncatedness and claim that
list X
can be given the structure of a monoidal category with tensor product given by list concatenation++
.The monoidal axioms for list can easily be checked. See #1895 for the pentagon identity. Therefore we need to show that
list X
is a monoidal category.Normalisation
Normalisation is a monoidal functor
nrm
from the free monoidal category on X tolist X
. It can be defined in an obvious way where nested trees created byunit
andtensor
can be associated to a list of elements ofX
.Furthermore, the normalisation functor has a uniqueness property which can be stated as: there is a natural equivalence
NatEquiv nrm idmap
.Maps from the free monoidal category to a monoidal category
Next we need to show that the free monoidal category really is free in that it is initial in the bicategory of monoidal categories. In other words, if
f : M -> N
is a monoidal functor between monoidal categories, then it can always be factored as a map into the free monoidal category followed by the universal map from the monoidal category toN
. There are some details here to be sorted out later with regards to the generating set, but the idea is basically the same as the one we have for free groups.Once we have that, then we can use the natural equivalence from
nrm
toidmap
to show that any two monoidal functors fromFMC(X) -> M
are naturally isomorphic. This gives our desired coherence.Making things practical
Now it's all very well to have such a theorem, but it is useless without being able to use it in practice. In order to do that we will need to create some tactics that can quote a given functorial term in a monoidal category
M
and produce an equivalent functor fromFMC(X) -> M
. Once this is characterised, the theorem can be applied to give the desired filler in a diagram.Conclusion
This project consists of some simple independent steps that I will list out specifically here so that over time we can chip away at them. The end result will be some nice machinery that let's us show various diagrams in monoidal categories are commutative in a mechanical way.
X
as the HIT described above.list X
is a wild monoidal category with++
as the operation.nrm
and show that it is a functor.nrm
is naturally equivalent toidmap
. (This is the bulk of the proof).X
to a monoidal categoryM
(which is monoidal in a specific sense (X
is monoidal with@
)), then this map factors through the free monoidal category.Luckily, none of this is new and has all been done before. Once this project is completed we should be able to play a similar game for braided or symmetric monoidal categories. This will be quite useful for abelian groups and smash products.
References
The text was updated successfully, but these errors were encountered: