missing axiom from Braided Monoidal Category definition? about agda-categories HOT 27 CLOSED

With @MirceaS's hint I was able to write down my own pen-and-paper proof, which I'll document here in the hope that it'll be helpful. (There may be easier proofs, but one has to start somewhere.)

The key insight I gained by looking at the nLab article @MirceaS cites is that 1⊗_ is equivalent to the identity functor. That means it's enough to prove

1⊗triangle : [ unit ⊗₀ (X ⊗₀ unit) ⇒ unit ⊗₀ X ]⟨
                 id ⊗₁ B                            ⇒⟨ unit ⊗₀ (unit ⊗₀ X) ⟩
                 id ⊗₁ unitorˡ.from
               ≈ id ⊗₁ unitorʳ.from
               ⟩

The actual triangle law can then be recovered by eliminating all the unit-multiplications via naturality of unitorˡ.

In the remainder, I'll use simplified notation: l, r, denote the left and right unitors, a the associator, 1 the unit, and I'll use juxtaposition for ⊗. I'll use primes to denote inverses, i.e. a' is associator.to. I'll write X for id{X} and I'll use = instead of ≈.

The proof goes like this:

1. We'll need two derived laws for monoidal categories:

  kelly  :
      (XY)1 ⇒⟨ a ⟩ X(Y1) ⇒⟨ Xr ⟩ XY
    = (XY)1 ⇒⟨ r ⟩               XY
  kelly'  :
      X(Y1) ⇒⟨ a' ⟩ (XY)1 ⇒⟨ r ⟩ XY
    = X(Y1) ⇒⟨ Xr ⟩              XY

The first one is one of Kelly's laws (coherence₂ from Categories.Category.Monoidal.Properties.Kelly's); the second one is easy to prove from the first (using the fact that a is an iso).

2. With this we can prove the following

1(1X) ⇒⟨ 1l ⟩ 1X
 = (by the triangle law)
1(1X) ⇒⟨ a' ⟩ (11)X ⇒⟨ rX ⟩ 1X
 = (B is and iso)
1(1X) ⇒⟨ a' ⟩ (11)X ⇒⟨ rX ⟩ 1X ⇒⟨ B ⟩ X1 ⇒⟨ B' ⟩ 1X
 = (by naturality of B)
1(1X) ⇒⟨ a' ⟩ (11)X ⇒⟨ B ⟩ X(11) ⇒⟨ Xr ⟩ X1 ⇒⟨ B' ⟩ 1X
 = (by kelly')
1(1X) ⇒⟨ a' ⟩ (11)X ⇒⟨ B ⟩ X(11) ⇒⟨ a' ⟩ (X1)1 ⇒⟨ r ⟩ X1 ⇒⟨ B' ⟩ 1X
 = (by naturality of r)
1(1X) ⇒⟨ a' ⟩ (11)X ⇒⟨ B ⟩ X(11) ⇒⟨ a' ⟩ (X1)1 ⇒⟨ B'1 ⟩ (1X)1 ⇒⟨ r ⟩ 1X
 = (by kelly)
1(1X) ⇒⟨ a' ⟩ (11)X ⇒⟨ B ⟩ X(11) ⇒⟨ a' ⟩ (X1)1 ⇒⟨ B'1 ⟩ (1X)1 ⇒⟨ a ⟩ 1(X1) ⇒⟨ 1r ⟩ 1X
 = (by the second hexagon identity)
1(1X) ⇒⟨ 1B ⟩ 1(X1) ⇒⟨ a' ⟩ (1X)1 ⇒⟨ B1 ⟩ (X1)1 ⇒⟨ B'1 ⟩ (1X)1 ⇒⟨ a ⟩ 1(X1) ⇒⟨ 1r ⟩ 1X
 = (-⊗1 preserves composition)
1(1X) ⇒⟨ 1B ⟩ 1(X1) ⇒⟨ a' ⟩ (1X)1 ⇒⟨ (B'∘B)1 ⟩ (1X)1 ⇒⟨ a ⟩ 1(X1) ⇒⟨ 1r ⟩ 1X
 = (B is an iso )
1(1X) ⇒⟨ 1B ⟩ 1(X1) ⇒⟨ a' ⟩ (1X)1 ⇒⟨ (1X)1 ⟩ (1X)1 ⇒⟨ a ⟩ 1(X1) ⇒⟨ 1r ⟩ 1X
 = (-⊗1 preserves identity)
1(1X) ⇒⟨ 1B ⟩ 1(X1) ⇒⟨ a' ⟩ (1X)1 ⇒⟨ a ⟩ 1(X1) ⇒⟨ 1r ⟩ 1X
 = (a' is an iso)
1(1X) ⇒⟨ 1B ⟩ 1(X1) ⇒⟨ 1r ⟩ 1X

3. With this we can prove the desired law via the equivalence between 1⊗- and the identity functor.

1X ⇒⟨ l ⟩ X
 = (l is an iso)
1X ⇒⟨ l' ⟩ 1(1X) ⇒⟨ l ⟩ 1X ⇒⟨ l ⟩ X
 = (by naturality of l)
1X ⇒⟨ l' ⟩ 1(1X) ⇒⟨ 1l ⟩ 1X ⇒⟨ l ⟩ X
 = (by 2 above)
1X ⇒⟨ l' ⟩ 1(1X) ⇒⟨ 1B ⟩ 1(X1) ⇒⟨ 1r ⟩ 1X ⇒⟨ l ⟩ X
 = (by naturality of l)
1X ⇒⟨ l' ⟩ 1(1X) ⇒⟨ 1B ⟩ 1(X1) ⇒⟨ l ⟩ X1 ⇒⟨ r ⟩ X
 = (by naturality of l)
1X ⇒⟨ l' ⟩ 1(1X) ⇒⟨ l ⟩ X1 ⇒⟨ B ⟩ X1 ⇒⟨ r ⟩ X
 = (l is an iso)
1X ⇒⟨ B ⟩ X1 ⇒⟨ r ⟩ X

from agda-categories.

yeah, you know, I spent two days on building infrastructure to make Kelly's coherence properties look sufficiently trivial.

from agda-categories.

according to https://ncatlab.org/nlab/show/braided+monoidal+category, it is provable. c.f. #16.

from agda-categories.

Wouldn't that mean that a fair bit of Morphism ought to be in Category.Properties then?

from agda-categories.

Isn't the fact that 1⊗_ is equivalent to the identity functor precisely what's being used in our proof of Kelly's coherence, using triangle-prism? I believe we can reuse quite a bit of that code in this proof to get rid of the 1⊗ part.

Yes indeed!

It also suggests that triangle-prism could be strengthened slightly so it doesn't require the morphisms on the top and bottom face of the prism to be isos, only those in the "pillars". (In fact, probably only one of them needs to be an iso.)

from agda-categories.

I guess this can be closed now as it was addressed in #67 and #77 ?

from agda-categories.

BTW:

Indeed, only the pillar where the arrow heads meet has to be an iso.

I implemented this in Categories.Morphism.Reasoning.Iso now (as push-eq) and then extended it so it can be used conveniently when one has a natural isomorphism (see the last part of the proof in #77 for an example).

from agda-categories.

Huh, I might try proving it in the library then if nobody else did that already.

from agda-categories.

that will be fantastic. in case of difficulties, please ask for help here.

from agda-categories.

Indeed, that would be great. I looked at doing it myself, and it was a bit more complex than I had the time right then. The link in issue #16 should be quite useful. The resulting commutative diagram is big, but not too bad to turn into an equational proof. There are quite a few combinators in Morphism.Reasoning that ought to help a lot, especially for gluing together parts of diagrams.

from agda-categories.

I suppose that the proof heavily relies on the involved morphisms being isomorphic. you might want to check https://github.com/agda/agda-categories/blob/master/Categories/Category/Monoidal/Properties.agda for an example of lifting and projecting morphisms to/from isomorphisms.

from agda-categories.

I checked multiple sources, answers and papers but I couldn't actually find a clear step-by-step proof. I tried to prove it myself and I did find that it is equivalent to a number of other identities but I couldn't prove any of them... The Stack Exchange answer has some mistakes in it and I can't really follow it. Do you have any idea where I can find a better source?

from agda-categories.

Could you nevertheless document the sources, answers & papers that you found? I tried to look for other sources, and couldn't find anything obvious.

from agda-categories.

Things that don't help (but may save others time in not going down these dead ends):

• Lean formalization doesn't deal with this
• searching for "braided monoidal category" coherence ("agda" OR "Coq" OR "Isabelle" OR "Lean" OR "Idris") on Google.

from agda-categories.

I can't remember what I found at the time but I just found a proof of an equivalent identity in https://ncatlab.org/nlab/show/monoidal+category that now allows me to prove the original statement (on paper, that is). Formalising it is going to take a while but at least I now know the steps.

from agda-categories.

Impressive! There might be a shorter proof in the picture from this thread on twitter.

from agda-categories.

Isn't that picture about Kelly's laws? Maybe we should tweet back a link to the mechanized version in https://github.com/agda/agda-categories/blob/master/Categories/Category/Monoidal/Properties.agda 😄

from agda-categories.

Haha, I spent the last 2 days trying to formalise coherence₁ before realising that it was already done in Properties.agda. Oh well. Reading through Properties.agda, I think I now got the gist of how to work with lifting in the iso category.
Isn't the fact that 1⊗_ is equivalent to the identity functor precisely what's being used in our proof of Kelly's coherence, using triangle-prism? I believe we can reuse quite a bit of that code in this proof to get rid of the 1⊗ part.
I'll have a go at formalising this tomorrow and I think I should have a PR ready by the end of tomorrow (UK time).

from agda-categories.

Oh, by the way, during my work I also discovered some interesting facts such as the following identities:

  (X1)1 ⇒⟨ r  ⟩ X1
= (X1)1 ⇒⟨ r1 ⟩ X1

  1(1X) ⇒⟨  l ⟩ 1X
= 1(1X) ⇒⟨ 1l ⟩ 1X

Are these known/formalised anywhere in the code?

from agda-categories.

Oh, by the way, during my work I also discovered some interesting facts such as the following identities:

  (X1)1 ⇒⟨ r  ⟩ X1
= (X1)1 ⇒⟨ r1 ⟩ X1

  1(1X) ⇒⟨  l ⟩ 1X
= 1(1X) ⇒⟨ 1l ⟩ 1X

Are these known/formalised anywhere in the code?

not that i am aware of. this library doesn't have lots of properties so if you don't find anything after a quick search, the chances are it is not there.

from agda-categories.

Perhaps they belong under Morphism somewhere?

from agda-categories.

unlikely. it's a property of the right unitor. should be around Monoidal.Properties if there is one.

from agda-categories.

Perhaps they belong under Morphism somewhere?

I feel like a very sensible approach would be to create a module inside Morphism called, say Properties, and have each of Monoidal, Braided, Symmetric etc. extend it as needed with properties related to that type of category (the same way we do it with HomReasoning and my MonoidalReasoning).

from agda-categories.

Wouldn't that mean that a fair bit of Morphism ought to be in Category.Properties then?

which bit you have in mind?

from agda-categories.

All of Morphism.Reasoning. Probably more. Morphism.Cartesian should stay where it is. Parts of the rest.

This is a discussion similar to that in issue #32 about where to put things.

from agda-categories.

All of Morphism.Reasoning. Probably more. Morphism.Cartesian should stay where it is. Parts of the rest.

This is a discussion similar to that in issue #32 about where to put things.

hmm... i agree with it to some degree. not sure which way is the best.

from agda-categories.

Isn't the fact that 1⊗_ is equivalent to the identity functor precisely what's being used in our proof of Kelly's coherence, using triangle-prism? I believe we can reuse quite a bit of that code in this proof to get rid of the 1⊗ part.

Yes indeed!

It also suggests that triangle-prism could be strengthened slightly so it doesn't require the morphisms on the top and bottom face of the prism to be isos, only those in the "pillars". (In fact, probably only one of them needs to be an iso.)

Indeed, only the pillar where the arrow heads meet has to be an iso.
I put up a PR with my work so far which proves the initial coherence minus the -x1 bit. I don't know when I will get around to strengthening the prism or using the current one to finish the proof but if anybody has the time to look into this, that would be nice! :)

from agda-categories.