[WIP] Monoidal Category Tactic

[TOTBWF]

Patch Description

This PR implements the start of a monoidal category solver, based roughly off of the ideas found in [1].
Specifically, we compute a normal form for each of the objects via reassoc, and then show that any composition of coherence morphisms is actually just the identity morphism between the normalized objects.

Notes

I'm almost over the finish line on this one, just have to show that normalization preserves equality for associators, and prove a couple of rather stubborn lemmas. Of note is strict-⊗, which is not being well behaved. The proof ought to follow by some simple rewrites like strict-∘, but Agda does not seem happy about that.

References

1. http://www.cse.chalmers.se/~peterd/papers/Coherence_Monoidal.pdf

[sstucki]

This is very cool!

I'd love to help out but I'm super busy this and next week. What I can offer in the meantime is some observations:

1. I'm not surprised that you have unresolved metas in exactly the places you do because you have not yet used any of the coherence laws (triangle, pentagon) that make it possible to prove coherence for monoidal categories. I suspect these will be crucial in the missing steps/proofs though I'm not 100% certain since the subset of the free monoidal category you're using is somewhat degenerate (you don't have any "non-trivial" morphisms).
2. Why use slurp? It's nice that you can proof the extra unit isn't necessary, but who cares? A normal form with the extra unit is as good as one without, no? I suspect the slurps could get in the way in some of the proofs.
3. Is the use of rewrite necessary? I'm surprised it worked, I thought rewrite was not --safe.
4. I was surprised that you added syntax for objects (Word) and for morphisms (Expr) but not for equations on morphisms. If you had those, your syntax would be the free monoidal category over a discrete category (with the objects of 𝒞). I was expecting you to prove preserves-≈ in that category (i.e. w.r.t. to the "synthetic" equality) rather than in the embedding of that category into 𝒞. Maybe that would simplify some proofs by removing the extra [_↓] in the types. Maybe not. But worth considering if you remain stuck.
5. I would actually have gone a step further and added yet another syntax for normal forms — the free strict monoidal category over the objects of 𝒞 — but you don't seem to need it. I suspect if one added support for non-trivial morphisms (i.e. anything other than combinations of associators and unitors) this might become necessary because the normal forms are then more complicated. But I'm just speculating.
6. Nitpick: I find the name "coherence morphism" a bit misleading. I think it should be "coherent morphism" because these morphisms don't ensure coherence, they are coherent (it's the coherence laws that ensure their coherence). Anyway, that's a detail.

Update: forget about 2. I realize now the slurps aren't used to define normal forms. They are helpers to define other things.

[TOTBWF]

Yeah, I roughly see where I need to use the associators and unitors. The reason I am using this degenerate version is that during reflection, I plan on splitting the morphisms into the ones that just do coherence things, and non trivial ones. If we included the non trivial ones in our subcategory, then the key theorem coherence : Expr A B → (X : Word) → reassoc A X ≡ reassoc B X woudn't be true!

As for rewrite, it's a special version of with abstraction that does some extra stuff for us (See https://agda.readthedocs.io/en/v2.6.1.3/language/with-abstraction.html#rewrite). There is another very unsafe feature with the same name, but that uses pragmas.

I originally tried working with synthetic equality actually, but it didn't seem to be buying me a whole lot. Perhaps it could help with versions of the problematic strict-⊗ lemma.

Adding a syntax for normal forms is a great idea, I hadn't considered it! The whole proof is sort of a bizzare version of a coherence theorem anyways, so it makes sense that an explicit version of a stricit moniodal category could be useful. Will give this a go :)

WRT to naming, good point. I suppose just writing unitors/associators is clearer.

[sstucki]

I managed to make some progress by using an explicit representation of normal forms. It allowed me to solve the case for the tensor product _⊗₁′_ in preserves-≈ and re-prove the other cases you had. I don't know how best to share this (is there a way to collaborate on PRs?) so I pushed it into a branch in my fork of the library:
https://github.com/sstucki/agda-categories/blob/27dc6adf0332a243747f83014b98fc3e7ee7786d/src/Categories/Tactic/Monoidal.agda

Hope this is helpful.

[JacquesCarette]

I think it is possible to add commits to this PR, at least for people who have push access to the repo (which I believe you do @sstucki ). Though it might make sense to push to you another branch that is started from this one, to let @TOTBWF do the merge, if he so chooses.

[TOTBWF]

@sstucki This is great! I think we might have ourselves a solver pretty soon :). WRT commiting to the branch, this is the most annoying thing about git IMO. I'll grab those commits off your branch and integrate them into mine. Moving forward, you should probably have your branch track mine so that the histories are the same (makes merges easier)

[TOTBWF]

Looks like using explicit equalities might be the right move after all. This lemma would be waaaaaay easier if we could pattern match on equality proofs.

invert-resp-≈ : ∀ (f g : Expr A B) → f ≈↓ g → invert f ≈↓ invert g

Maybe it's worth defining Free Monoidal Categores in a separate PR. That seems useful enough in it's own right! The same could be said for the strict variants as well.

[sstucki]

Can't you use the fact that f and inverse f form an iso? Lift f ≈↓ g to an equality on isos, the project out the component on the inverses.

In fact, there's a lemma in IsoEquiv that proves what you want:

agda-categories/src/Categories/Morphism/IsoEquiv.agda

Lines 22 to 23 in 5e4de42

	to-unique : ∀ {f₁ f₂ : A ⇒ B} {g₁ g₂} →
	Iso f₁ g₁ → Iso f₂ g₂ → f₁ ≈ f₂ → g₁ ≈ g₂

[sstucki]

Moving forward, you should probably have your branch track mine so that the histories are the same (makes merges easier)

Good idea, I'll do that!

[TOTBWF]

Ok, more progress. ⌊⌋-α is done, and all that remains of the associator case is a gnarly reassociation. What are everyones thoughts on using the category tactic to implement this tactic? They both will be importing reflection code at the end of the day, so the dependency tree doesn't get any deeper.

[JacquesCarette]

Because of the stated reason, using the category tactic here seems reasonable.

[sstucki]

What are everyones thoughts on using the category tactic to implement this tactic? They both will be importing reflection code at the end of the day, so the dependency tree doesn't get any deeper.

Actually, a lot of the code in this module is independently useful. It's a weak version of the coherence theorem for (discrete) monoidal categories. It just so happens that this proof is constructive so we can use it as an algorithm to "solve" equations in such categories. I think there's a point exposing that part of the module and making it independent of tactics code.

If the issue is just the "gnarly reassociation" for the associator case, then we can either prove it by hand (shouldn't be all that bad) or use the category tactic to generate a proof and substitute it in. Apparently the command for this is C-c C-m but I have never tried using it.

[TOTBWF]

The proofs are finally done! Now all that remains is writing the reflection code, and figuring out what needs to get factored out.

@sstucki After checking through the relevant sections of CWM, I think this is actually the proof that Maclane has. Specifically, that coherence theorem states that "every diagram built out of unitors, associators, and multiplication commutes"[1], which is exactly what this proves.

References

[1] Categories for the Working Mathematician VII.2

[JacquesCarette]

I would be tempted to call this [[_]]W. But this is just a weak suggestion.

[JacquesCarette]

And then here [[_\d]] (or maybe put the downarrow outside?). Again, weak suggestion.

[JacquesCarette]

My feeling is that using the semantic equality here is downright clever, and should stay.

[JacquesCarette]

Perhaps make the next two proofs private, and export just invert-iso?

[JacquesCarette]

Add a comment to the effect that "the normal form for a (free) Monoid is a list"?

[JacquesCarette]

I would be tempted, to avoid subst-juggling, to try

  idⁿ : ∀ {N M} → N == M → NfExpr N M

There's also some alternate way that @sstucki wrote to do this, but I can't recall where it is...

[sstucki]

@JacquesCarette I think you're thinking of hid which itself uses subst-juggling, so not sure it's helpful here.

But I was thinking: the use of subst in this module could maybe be avoided if the normal forms of the unitors and associators were defined by recursion on the domains following the same structure as the unit/associativity laws for lists themselves. That might also simplify the proofs of the corresponding "monoidality" laws which are proven by recursion and need helper lemmas to deal with the subst stuff. Anyway, just an idea, I don't know whether it would actually work out.

[JacquesCarette]

Right, hid. If all subst-juggling can be isolated to one place, that counts as a win.

[TOTBWF]

Ok, I've done some more thinking on this, and I have a idea for how we can normalize non-discrete things. If we update our Expr to:

  data Expr : Word → Word → Set (o ⊔ ℓ) where
    id′  : Expr A A
    _∘′_ : Expr B C → Expr A B → Expr A C
    _⊗₁′_ : Expr A C → Expr B D → Expr (A ⊗₀′ B) (C ⊗₀′ D)
    α′   : Expr ((A ⊗₀′ B) ⊗₀′ C) (A ⊗₀′ (B ⊗₀′ C))
    α⁻¹′ : Expr (A ⊗₀′ (B ⊗₀′ C)) ((A ⊗₀′ B) ⊗₀′ C)
    ƛ′   : Expr (unit′ ⊗₀′ A) A
    ƛ⁻¹′ : Expr A (unit′ ⊗₀′ A)
    ρ′   : Expr (A ⊗₀′ unit′) A
    ρ⁻¹′ : Expr A (A ⊗₀′ unit′)
    [_↑] : X ⇒ Y → Expr (X ′) (Y ′)

and our normal forms to something like:

  data NfExpr : NfWord → NfWord → Set (o ⊔ ℓ) where
    emptyⁿ : NfExpr [] []
    consⁿ  : ∀ {X Y} {N M} → X ⇒ Y → NfExpr N M → NfExpr (X ∷ N) (Y ∷ M)

Then things seem to work out. Most of the proofs seem to fall out pretty naturally by induction, though I haven't reworked the monster that is preserves-≈.

One annoying thing is that we lose out on invert, but we can flip most of the structural morphisms we need by hand. This seems like a totally acceptable price to pay for a better tactic though!

[JacquesCarette]

Everything else in Expr represents an iso, so why not for

   [_↑] : X ⇒ Y → Expr (X ′) (Y ′)

as well? You should make the lift be on an iso too. You really do want that for NfExpr too, no? Then you'll get invert back too.

[sstucki]

This is definitely a big step forward, but it doesn't go all the way. The issue is that the domain and codomain of [_↑] should really be words because you'd want to be able to represent things like id ⊗ f ∘ g ⊗ id where f : B ⊗ C ⇒ X and g : Y ⇒ A ⊗ B, i.e. where fand g are "shifted" w.r.t. each other. I suspect this would complicate normal forms a lot though. But I might be wrong. You've already come much further than I thought would be possible!

In any case, the tactic would already be enormously helpful even in the form you propose, because one could solve string diagrams "layer by layer" with a few manual proofs to merge and split these layers, when necessary.

[sstucki]

You should make the lift be on an iso too.

Actual string diagrams that contain arrows other than the monoidal maps (unit, assoc, etc.) need not be invertible. So there's no reason to think you'd only be embedding isos, is there?

[TOTBWF]

We can still represent those morphisms with this encoding actually!

  example : ∀ {V W X Y Z} (f : W ⊗₀ X ⇒ Y) → (g : Z ⇒ V ⊗₀ W) → Expr ((Z ′) ⊗₀′ ((W ⊗₀ X) ′)) (((V ⊗₀ W) ′) ⊗₀′ (Y ′))
  example f g = id′ ⊗₁′ [ f ↑] ∘′ [ g ↑]  ⊗₁′ id′

The trick here is that we are "quoting" the objects W ⊗₀ X and V ⊗₀ W

EDIT:
Ok it does have problems when you have things like [ f ↑] ∘′ α′, as the the [ f ↑] has everything quoted, and the α′ has nothing quoted.

[JacquesCarette]

The Expr without [_↑] could only represent isos. That's why invert could exist.

[sstucki]

The trick here is that we are "quoting" the objects W ⊗₀ X and V ⊗₀ W

I don't understand how the composition can type check when different parts of the domain and codomain are quoted.

EDIT: Oh, I see. My example was imprecisely formulated. I meant for the domain of f and the codomain of g overlap on B (or W in your example).

[TOTBWF]

Yeah, that example worked out fine by coincidence. You run into trouble when you want to start composing onto associators/unitors. You were definitely right when you stated that the domain/codomain of the quoted morphisms ought to be reified words.

[sstucki]

Yea, what I had in mind was

   Y     C
   |     |
[  g  ]  |
 |   |   |
 |  [  f  ]
 |     |
 A     X

[TOTBWF]

Ok, I have a possible solution:

During reflection, we insert quoting/unquoting morphisms when needed:

    quot   : Expr A ((reify A) ′)
    unquot : Expr ((reify A) ′) A

These can read-back into id morphisms. We should also probably add something to the normal form to support these as well

[sstucki]

I think the fundamental problem is certain diagrams just cannot be 'linearized' into a single list of morphisms. They need some form of tiling with multiple levels. Here's another version of the example I gave above with an explicit associator:

   Y     C
   |     |
[  g  ]  |  
 |   |   |
[  assoc  ]
 |   |   |
 |  [  f  ]
 |     |
 A     X

I cannot see how you'd turn that into a single layer. But maybe there's a way to turn it into a multi-layer normal form somehow.

[JacquesCarette]

Would there be something to learn from @gelisam 's premonoidal solver?

[gelisam]

The monoidal version of the problem is harder than the premonoidal version, so it is I who has the most to learn from this conversation :)

In particular, while I do have a definition for a free premonoidal category in that repo, I have not yet made a solver out of it.

What distinguishes a premonoidal category from a monoidal category is that the law (f *** id) >>> (id *** g) = f *** g = (id *** g) >>> (f *** id)

  |     |         |     |         |     |
[ f ]   |         |     |         |   [ g ]
  |     |    =  [ f ] [ g ]  =    |     |
  |   [ g ]       |     |       [ f ]   |
  |     |         |     |         |     |

is required to hold in a monoidal category but not in a premonoidal category (in fact there is no (***) in a premonoidal category, only the special cases first f = f *** id and second f = id *** f).

When looking for a definition for a free X, e.g. the free monoidal category, I start from a representation for the AST and I apply all the laws to reduce all the degrees of freedom. Above, we can see that the f and the g are free to slide past each other; by applying the corresponding law, I eliminate that freedom and force all the free-sliding blocks all the way to one side, say, the bottom. The end result is that the canonical representation looks like a tetris pile: blocks stacked on top of each other, with some overhangs.

  |        |            |        |
  |   [    f    ]       |        |
  |     |     |         |        |
[ g ]   |     |         |        |
  |     |   [ h ]       |        |
  |     |     |    =    |        |
  |   [    i    ]       |        |
  |     |     |         |        |
[    j    ]   |         |   [    f    ]
     |        |         |     |   [ h ]
     |      [ k ]     [ g ] [    i    ]
     |        |       [    j   ]  [ k ]

The canonical representation for the premonoidal case is much easier: the representation on the left is already canonical. It's just a list of atoms, each shifted so that it only affects a sublist of the strings at that height of the string diagram.

[gelisam]

Taking a closer look at this branch, it looks to me like you don't support atoms at all, only the structural bits such as the associators, unit-introduction, and unit elimination? That explains why your only normal form is the identity! Well, that certainly makes the problem a lot simpler.

And yet, from what I can see in the rest of this thread, it has already been quite a challenge! I guess I was wrong to think that the main challenge when writing this kind of solver was to figure out what the canonical representations look like, and that the rest (converting to and from the canonical representation, proving that an expression is equal to its canonical representation, writing a macro reflecting the type into an expression) would be routine.

[gelisam]

Maybe it's worth defining Free Monoidal Categories in a separate PR.

Where is your definition of a Free Monoidal Category? I'd be curious to see how yours compares to my tetris pile approach. I don't see it in this nor any recent PR.

[sstucki]

Taking a closer look at this branch, it looks to me like you don't support atoms at all, only the structural bits such as the associators, unit-introduction, and unit elimination?

Indeed, atoms are not part of the implementation in the PR, hence the discussion starting after this comment by @TOTBWF (who claims he has a version with limited support for atoms somewhere 😉).

And yet, from what I can see in the rest of this thread, it has already been quite a challenge!

The challenge was really to implement the laws and to show that (embeddings of) the normal forms are equal to the original morphisms. The main difficulty there, as far as I can tell, stems from the coherence laws for the associators and unitors. As far as I can tell, this is somewhat orthogonal to the question of defining (good) normal forms. But @TOTBWF did all the work, so I might be wrong 😄.

Where is your definition of a Free Monoidal Category? I'd be curious to see how yours compares to my tetris pile approach. I don't see it in this nor any recent PR.

In this PR, we only support a degenerate form of monoidal category (the discrete ones) which are lacking atoms, as you point out. The free discrete monoidal category is just the one built out of Words, Exprs and the _≈↓_ equality. I think something like your tetris pile should also work for monoidal categories, but I'm not sure how best to define that normal form as a datatype. Especially since one then needs to show that all the usual operations (composition, product, associators, etc.) are "admissible" for this representation (i.e. can be "implemented") and satisfy all the laws. Did you come up with a satisfactory representation for your project?

[TOTBWF]

I've done a lot of stewing on this over the past 2 weeks, and I keep running into walls whenever I try to add non-structural morphisms. I think that this approach of trying to boil everything down to identity morphisms then reading them back is just not the right approach to handling atomic morphisms, and we may need to take a radically different approach if we want to support those. That's not to say the existing code isn't useful (it is a proof of a coherence theorem after all, and that is somewhat exciting), but I can't see any obvious way of bolting on non-structure morphisms that doesn't cause everything to come falling down.

Perhaps instead of trying to do the strictification and solving at the same time, we could adopt a sort of "phased" approach, where we pluck out all of the structure morphisms, resolve them to a canonical form, then try to solve the remaining morphisms in this strict context.

[JacquesCarette]

So is this completely stalled then?

[TOTBWF]

I've been pretty busy as of late (started a new job and moved countries) so I haven't had the time to think about this too hard 🙁. Hopefully I'll have some time to devote to this soon!

[JacquesCarette]

Those are rather good reasons for not having time! Hope it all went smoothly.

[laMudri]

What's the current thinking on this? It looks as if coherence doesn't get us a solver for equalities in the usual sense, because coherence only talks about the free monoidal category on a set of objects, rather than on any data that could contain morphisms.

I wonder how much we can get out of coherence. I suppose the most obvious thing is that, if we had a coherence tactic, we would never have to name a coherence principle during a proof. I think there genuinely are at least some cases where we naturally have two cliques of structural morphisms, and we know they're equal because of coherence.

Something else we should be able to get is a tactic for composition up to structurality. For example, if we have f : X → A ⊗ (B ⊗ C) and g : (A ⊗ B) ⊗ C → Y, we should be able to have a g ∘ᴹ f : X → Y. Naturality should give us that g ∘ᴹ ((h ⊗ (i ⊗ j)) ∘ f) ≈ (g ∘ ((h ⊗ i) ⊗ j) ∘ᴹ f. And we should be able to introduce arbitrary structural morphisms “within” the composition, like g ∘ᴹ f ≈ g ∘ᴹ (λ ⊗ id) ∘ᴹ f.

For a lot of other things we do in monoidal categories, maybe the tool we need is a solver for morphisms involving various functors and natural transformations. Incorporating functors into a solver is traditionally hard to do because of size issues, but this should not be a problem when most of the functors derive from ⊗, as these are all level-preserving. I don't remember seeing a solver for natural transformations, but it seems at least plausible that one should be possible to make.

[JacquesCarette]

So this might end up being new research, rather than something that can "just be done". Or at least, that's my current impression. I don't personally have any cycles I could devote to this right now (and not for some months), but if it's still open when my time frees up [and it will - sabbatical next year!], I'll dive in.

[JacquesCarette]

I take it that this is still stalled (and there was no progress on something similar over in 1lab?)

[gelisam]

We're currently discussing this in the Monoidal Café discord. We found a flaw in my Tetris pile idea from earlier in this thread: it doesn't support scalars (morphisms from unit to unit), which commute with each other but not with identity morphisms. Word on the street is that @pigworker has found a complicated normal form for monoidal categories he calls "staircases", but it's not ready to be published yet.

[JacquesCarette]

I can't find the Monoidal Café discord - could I get an invite?

[zanzix]

I was summoned here by @gelisam. Here is an invite to the Monoidal Cafe, feel welcome to join!
https://discord.gg/kswesAKQ