Coherence theorem for monoidal categories #112
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…sts and one for the coherence theorem itself
stschaef
approved these changes
Oct 22, 2024
hejohns
pushed a commit
to hejohns/multi-poly-cats
that referenced
this pull request
Oct 26, 2024
* displayed monoidal categories * free monoidal category on a type of objects with its universal property * strong and lax monoidal functors * Displayed Arrow category and Iso category and their reflection principles * helper for making displayed monoidal cats with prop homs * a more convenient version of isSetHom\^D * product of monoidal cats, prove Graph is a 2-sided fib (also define 2-sided fib) * Monoidal structure on displayed cat of Isos of Monoidal Cat * arrow cat is 2-sided fib, iso cat is 2-sided isofib * reindexing displayed monoidal cat along strong monoidal functor * prove displayed Iso cat is isofibration, product of strong monoidal functors * IsoFiber displayed category, whose GlobalSections are sections up to Iso * Lists as monoidal category, weak universal property * displayed monoidal total category * prove hasPropHoms is closed under IsoRetraction * dual of a monoidal category
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
I've gotten this pretty far, but there are a couple of monoidal category diagram chases left:
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.Coherence.agdato constructrecforList, 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.Making this PR because I might not have more time to work on this this weekEdit: finished now, figured out a way to avoid needing the composition of strong monoidal functors by using the displayed total category instead.