search

maxsnew / cubical-categorical-logic

Extensions to the cubical stdlib category theory for categorical logic/type theory
MIT License
25 stars 5 forks source link

Coherence theorem for monoidal categories #112

Closed maxsnew closed 1 month ago

maxsnew commented 1 month ago

I've gotten this pretty far, but there are a couple of monoidal category diagram chases left:

  1. Need to prove that the composition of lax/strong monoidal functors is lax/strong. I have the construction of the nat isos but not the coherences. Once that's done we can show any strong monoidal functor into the free monoidal category has a section up to nat iso.
  2. Need to prove a couple more diagrams Coherence.agda to construct rec for List, which will give us such a strong monoidal functor into the free monoidal category. One is a dual of a large proof I've already done. The other one not so sure about.
  3. Then show that if a cat is a retract up to iso of another that its homs are a retract, and so inherit hLevels, which then shows that if the generators are an hSet that the free monoidal category is thin.

Making this PR because I might not have more time to work on this this week

Edit: finished now, figured out a way to avoid needing the composition of strong monoidal functors by using the displayed total category instead.

maxsnew commented 1 month ago

@stschaef @hejohns you want to do a review here?