search

HoTT / Coq-HoTT

A Coq library for Homotopy Type Theory
http://homotopytypetheory.org/
Other
1.23k stars 185 forks source link

Project: coherence for monoidal categories #1896

Open Alizter opened 3 months ago

Alizter commented 3 months ago

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:

Inductive FMC (X : Type) :=
| unit : FMC X
| tensor : FMC X -> FMC X -> FMC X
| associator x y z : tensor (tensor x y) z = tensor x (tensor y z)
| left_unitor x : tensor unit x = x
| right_unitor x : tensor x unit = x
| triangle x y
  : associator x unit y @ ap (tensor x) (left_unitor y)
    = ap (fun x => tensor x y) (right_unitor x).
| pentagon w x y z
  : associator (tensor w x) y z @ associator w x (tensor y z)
    = ap (fun f => tensor f z) (associator w x y)
      @ associator w (tensor x y) z
      @ ap (tensor w) (associator x y z).

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 type X. 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 https://github.com/HoTT/Coq-HoTT/pull/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 to list X. It can be defined in an obvious way where nested trees created by unit and tensor can be associated to a list of elements of X.

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 to N. 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 to idmap to show that any two monoidal functors from FMC(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 from FMC(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.

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

jdchristensen commented 3 months ago

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 X -> FMC X.

I also think that the paths introduced in the HIT will be a problem. A functor from that HIT will have to take tensor (tensor x y) z and tensor x (tensor y z) to equal objects of the target category, but in general they will only be isomorphic, unless the target category is univalent. So I think what we really want is to formally adjoin isomorphisms, not paths. Not sure how to do this. (The same comment applies to the other equalities.)

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 to N

I don't think this is the correct universal property. Currently FMC X is the free monoidal category on the type X, so the universal property should give some kind of equivalence between all type maps X -> N and all monoidal functors SMC X -> N. If we instead have X be a category, then the construction of FMC X will be more involved, and the LHS of the equivalence would have (non-monoidal) functors X -> N.

Alizter commented 3 months ago

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.

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.

In your HIT, I think you forgot a point constructor X -> FMC X.

Yes, I did forget it, thanks.

I also think that the paths introduced in the HIT will be a problem. A functor from that HIT will have to take tensor (tensor x y) z and tensor x (tensor y z) to equal objects of the target category, but in general they will only be isomorphic, unless the target category is univalent. So I think what we really want is to formally adjoin isomorphisms, not paths. Not sure how to do this. (The same comment applies to the other equalities.)

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.

I don't think this is the correct universal property. Currently FMC X is the free monoidal category on the type X, so the universal property should give some kind of equivalence between all type maps X -> N and all monoidal functors SMC X -> N. If we instead have X be a category, then the construction of FMC X will be more involved, and the LHS of the equivalence would have (non-monoidal) functors X -> N.

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.

mikeshulman commented 3 months ago

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.

jdchristensen commented 3 months ago

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.