better definition of monoidal 1-category

[Alizter]

We refactor the definition of a monoidal 1-category to be more inline with the rest of the wildcat library. This should also make it easier to actually use in the library. A simple example would be binary products in a pointed category.

[Alizter]

Hmm I seemed to have missed that we actually use the LeftUnitor and RightUnitor classes. I will see what the best way forward will be.

[Alizter]

I've further improved Monoidal.v so that it declares and uses some common diagrams that appear in the definition defined as typeclasses. I've also adapted the rest of the library.

I added a few more instances for bifunctors however I am unsure it is a good idea.

@gio256 Could you also take a look and tell me what you think? Notably there is a proof in AbHom.v that had to be tweaked as typeclass search seemed to loop. I couldn't however work out why it was looping.

My hope with these classes is that we can reuse them in the definition of TwoOneCat.v. A test case would be that a (2,1)-cat structure on a contractible type is monoidal.

@jdchristensen I had to tweak some of the proofs for the associativity of the join and it might need further improvements.

One thing that has changed is the direction of the associator. We used to have A x (B x C) -> (A x B) x C however I think that (A x B) x C -> A x (B x C) is a better choice. If we think of n-ary tensors as a list, then lists should associate to the right a :: b :: c :: [] etc. This will make working with monoidal categories slicker in the long-run. We can think of the associator as a rewrite rule "normalizing" the n-ary tensors. It might be that we need to tweak a few of the proofs in the Join formalization to better suite this however.

Another thing that would probably simplify some of the work here is some theory of natural transformations in two variables to complement our theory of bifunctors. I believe that these don't require an extra coherence like in the 1-functoriality case. Another simplification would be a treatment of ternary functors (and nat trans) which would simplify some of the funny instances we had to define.

[jdchristensen]

I think it's good to have classes for various identities. About the direction of associativity:

One thing that has changed is the direction of the associator. We used to have A x (B x C) -> (A x B) x C however I think that (A x B) x C -> A x (B x C) is a better choice. If we think of n-ary tensors as a list, then lists should associate to the right a :: b :: c :: [] etc. This will make working with monoidal categories slicker in the long-run.

I don't think it matters which way the associator goes, but I don't buy this argument that the direction you used is better. I think what is most important is that we try to be consistent. So if you want this direction here, then I suggest that join_assoc be proved in the other direction, so we don't need the inversions that were introduced in join_associator and the complexity they add to the proof of the triangle law. Or you could reverse the direction of the typeclass.

I looked through the library and found that these all agree: join_assoc, Associativity from Classes (used for addition, multiplication, the operations in any group or ring, etc.), the associativity of addition in Spaces/Nat/Arithmetic.v, and the associativity of products of types. The other other convention is used for associativity of sums of types and the associativity of compositions of morphisms in a category and in a wild category. Since Associativity from Classes is used a lot, it might be best to conform to that as much as possible. But I'm ok with staying with your convention if join_assoc can easily be flipped as well, without making it more complicated. (I'm hoping to prove the pentagon at some point, and for that it'll be important to minimize the complexity.)

[Alizter]

Very well, I will flip the direction back. I should also note that it has been quite common in the literature to choose the convention I gave, but not universally so.

[Alizter]

Actually I read your comment a bit fast yesterday. I think I would like to continue with this direction for the associator. This is the direction we pick for cat_assoc as you said. I'll have a go at better adapting some of the proofs in the Join formalization to work in the opposite direction.

[Alizter]

I think another improvement we can make to this definition is to keep the tensor operation and unit as an argument rather than part of the structure. We do this already in mathclasses and it makes it easier to reason about. If being monoidal was a property then I think keeping it in the record would make more sense, but it is not. We have various examples of monoidal categories with different tensor products and I think it would benefit us greatly to be sure exactly which one we are using.

For instance, Type has Join and prod, pType has pprod and Smash, etc.

[Alizter]

I've added two more commits now. The first commit applies some review suggestions. The second commit reverses the direction of the associator to be inline with the one in JoinAssoc; redefines the naturality as an uncurried form to the one found in JoinAssoc; and also adds a way to build uncurried natural transformations.

I had a go at reversing the associator in JoinAssoc but after some hours rewriting proofs I found myself asking "what's the point?", so I reversed it instead now.