Join: prove unitors, triangle law, and hexagon law #1784
Conversation
| Require Export WildCat.Square. | ||
| Require Export WildCat.PointedCat. | ||
| Require Export WildCat.Bifunctor. | ||
| Require Export WildCat.Monoidal. |
There was a problem hiding this comment.
Completely forgot we had this! Looks like there are some incomplete (aborted) results in there still.
| (** ** The hexagon axiom *) | ||
|
|
||
| (** This describes the transformation on [TriJoinRecData] corresponding to precomposition with [functor_join idmap (join_sym C B)], as in the next result. *) | ||
| Definition trijoinrecdata_id_sym {A B C P} (f : TriJoinRecData A B C P) |
There was a problem hiding this comment.
This can be defined ealier in TriJoin right?
There was a problem hiding this comment.
It could go in TriJoin, but I think it fits better in JoinAssoc. functor_join idmap (join_sym _ _) is like the twist equivalence, but in the second and third variables, instead of the first and second. So I think it fits in the file where the twist equivalence is studied. It's also a fairly specific result, so is probably best kept close to where it is used.
|
@jdchristensen Will you try to prove the pentagon next? I had a look and it seems we will probably need a |
@Alizter I'd like to have it, to complete the story, but I'm not sure how to handle the quadruple join. The triple-join induction principle was a lot of work, and while I figured out ways to avoid much of the path algebra, there were still a few cases that needed a 3-cell to be filled. I don't think it would be fun to figure out a 4-cell. I'll think about whether there's a way to push through the pentagon without developing the general theory of quadruple joins... |
The first commit adds faithfulness of the Yoneda embedding, which is used in the next parts. It also adds duals for the 0gpd results, which I hadn't added before.
The next two commits make progress towards showing that the join gives a symmetric monoidal structure. I think all that is missing is the pentagon.