WildCat notation

[patrick-nicodemus]

We currently use the following notation in the WildCat library:

• @ (path concatenation) is in diagrammatic order
• $@ (groupoid composition, vertical composition of 2-cells in a wild 1-category) is in diagrammatic order
• $o (morphism composition) is in traditional order
• h $@L p (whiskering of the 1-cell h with the 2-cell p) is in traditional order
• p $@R h (whiskering of the 1-cell h with the 2-cell p) is in traditional order
• alpha $@@ beta (horizontal composition of 2-cells) is in diagrammatic order

A few points:

• It seems inconsistent that $@@ is in diagrammatic order while $@L, $@R and $o are in traditional order, because whiskering is a special case of horizontal composition (with the identity)
• It's a bit confusing that vertical composition of 2-cells in a wild 1-category is usually given in diagrammatic order (using $@) while horizontal composition of 1-cells and whiskering are in traditional order. Perhaps it would be good to introduce more notation, say for horizontal composition of 2-cells in a wild category in diagrammatic order, so that proofs can use diagrammatic notation consistently.
• I am currently working on this bicategory branch and I need good notation for horizontal and vertical composition of 2-cells. One option is to adhere to the syntax above as closely as possible. On the other hand, @ is concatenation in the path groupoid, $@ is composition in an arbitrary 0-groupoid, and $@L, $@R and $@@ are only defined for cells in groupoids. Therefore one could argue that using the @ symbol in contexts where the cells are not invertible is confusing, because the programmer expects that it generalizes path groupoids and 0-groupoids, i.e., the cells are invertible.

I propose alpha $| beta for the vertical composition of alpha with beta in diagrammatic order in a bicategory, so alpha $| beta = alpha $@ beta for the 2-cells of a 1-category. I'm not sure what a good symbol is for horizontal composition of 2-cells and whiskering. I kind of like the semicolon for diagrammatic horizontal composition, because it evokes program composition: f; g; h.

[jdchristensen]

I might be in favour of expanding existing notations to non-groupoid situations rather than duplicating notations. One reason is that there are a lot of places where we use the groupoidal notations and therefore require typeclasses asserting that the appropriate graphs are groupoids, when in fact that doesn't get used at all except to allow the notation.

For example, I noticed a little while ago that we currently have

  Definition IsInitial {A : Type} `{Is1Cat A} (x : A)
    := forall (y : A), {f : x $-> y & forall g, f $== g}.

which requires A to be a 1-category. But the definition makes sense even if A is not a 1-category, and there was a situation in which the type class search here went astray when in fact it wasn't needed at all. One option would be to use $-> for the (possibly non-invertible) 2-cells, writing:

  Definition IsInitial {A : Type} `{Is2Graph A} (x : A)
    := forall (y : A), {f : x $-> y & forall g, f $-> g}.

Or, if we decided that $== could be used for any higher cells, then we could have

  Definition IsInitial {A : Type} `{Is2Graph A} (x : A)
    := forall (y : A), {f : x $-> y & forall g, f $== g}.

In this case, $== just becomes a synonym for $-> except that it would denote a 2-cell or higher.

(Of course, if you decide to make definitions like this without assuming invertibility, there can be different, inequivalent choices. But I'm not sure that's an issue. We just pick one way that is convenient.)

[patrick-nicodemus]

One could also consider something along the lines of

Definition IsInitial {A : Type} `{Is2Graph A} (x : A) := 
  forall (y : A), (x $-> y) /\ (forall (f g : x $-> y), f $=> g)

I think there would be some utility in a general notion of "wild contractibility" -

• a 0-graph (A, R : A -> A -> Type) is contractible if A is inhabited and forall (x y : A), R x y
• an n+1-graph (A, R : A -> A -> n-Graph) is contractible if A is inhabited and for all x y : A, R x y is a contractible n-graph

Then IsInitial x would mean that Hom x y is a contractible 1-graph for all y.

As a notational preference I would rather $== always denote an equivalence relation, and perhaps $=> could be a generic notation for a cell of level 2 or higher (a higher cell in any n-graph for n >=2? or would we expect the higher cells to form at least a 01Cat)

I am fine with $@ being weakened to (diagrammatic) composition in any 01cat.

[jdchristensen]

@patrick-nicodemus I like your idea of wild contractibility. I wonder if a functor is a wild-equivalence iff all of its wild-category fibers are contractible?

If we keep $== for equivalence relations and add $=> for possibly non-invertible 2-cells, then in all situations where we currently use $== we'd need to evaluate whether the invertibility is really being used there. And the conservative default would be to just use $=>. ("conservative" in the sense of not requiring additional type classes that aren't needed.) But then, why have $== at all? So I'm not sure about having two notations for n-cells for n >= 2. We could decide to switch to $=> everywhere, but then the parallel with == is lost. Or we could just use $-> in all cases, but then the hint to the reader is lost.

Lately some of our renamings have caused problems for out-of-tree work and also created conflicts for unmerged PRs. Based on that experience, my suggestion would be to make changes that have minimal impact throughout the library. That would support the idea of simply letting the $== notation be used even if the cells aren't invertible. And this is pretty reasonable: until you need to do an operation on a cell, you shouldn't care about what properties it has.

[patrick-nicodemus]

I understand the need to not be overly disruptive to out of tree work.

But then, why have $== at all?

I'm sure there are examples of 0-groupoids in this library which are not the 0-groupoid of 1-cells in a 1-cat or (2,1)-cat. For example there is the core isomorphism groupoid of a 1-cat. And if you know it is invertible (e.g. morphisms in Ext(A,B)) then $== is clearer than $=>. I am sure there are also important theorems about categories which are not true for 1-bicategories, and so you wouldn't be able to drop the typeclass restriction for $==for those proofs.

To me, $== makes sense in its current meaning of a morphism in a 0-gpd. $=> would be an arbitrary 2 cell or n>=2. So the meanings would be more overlapping than duplicating. Refactoring things like IsInitial would then be slow things to do gradually, it's natural that this would be distruptive to out of tree work because it's a meaningful change (weakening a hypothesis)

It's important to agree on some notation because future work on 2-categories will depend on it, so I won't dig my heels in, but I do think using $== for a non equivalence relation is not a good convention (if it's agreed to be temporary that would be okay)

[jdchristensen]

That's a good point that $== applies in any 0-groupoid, not just to higher cells that happen to be in a 0-groupoid, so it's probably best not to expand its meaning.

We could just use $-> for generic higher cells. It's not clear if we really need to distinguish n=1 from n>=2 with a separate notation. On paper, I might do so, and also distinguish 3-cells with a third horizontal line, etc, but I'm not sure it's worth it here since there isn't an obvious way to continue the pattern. Hmm, one idea would be $-> for 1-cells, $--> for 2-cells, $---> for 3-cells, etc... (Of course, those are all lower bounds. One could use $--> for 3-cells if one wanted, since they are 2-cells in a Hom category. So this would still be a heuristic.)

Then we should actually define $= for the 1-cells in a 0-groupoid, $== for invertible 2-cells, etc. This would match how paths are = and homotopies are ==.

So the notation would cleanly separating out the invertibility from the dimension of the cell.

This actually looks pretty reasonable to me. What do people think?

[patrick-nicodemus]

I think that's logical and makes sense. I think that 2-cells are common enough that 4 characters is a little bulky and will increase the size of common theorem statements.

I agree that there's no obvious way to continue the pattern but this strikes me as mostly unproblematic. In a bicategory all 3-cells are invertible so I would tend to prefer $== or $===, so it's unnecessary to solve the problem of a good notation for noninvertible 3-cells. A good notation for modifications of pseudo functors is desirable but non-invertible 4-cells will likely be considered so infrequently that an ad hoc local notation in the files that use them is fine. Even in the case of modifications it's still not a pressing problem to come up with a good notation for all 3-cells if one can choose a good notification for modifications specifically and call it a day.

if $=, $== and $=== seems clearer to you then I'm definitely okay with that, but I prefer using $-> for 1 cells, and $=> for 2 cells. Perhaps $==> for 3-cells, then, or just ==> if there is no conflict with the Categories library. (Dropping the dollar sign would be a bit inconsistent but having dollar signs absolutely everywhere isn't really the most aesthetically pleasing thing either)

[patrick-nicodemus]

Actually we are getting a bit off topic here because the original question was specifically about composition operators

[jdchristensen]

Actually we are getting a bit off topic here because the original question was specifically about composition operators

Right, but the questions are related, and we should come up with a plan that is consistent. You mentioned that some operations are only defined for cells in groupoids, and my response was:

I might be in favour of expanding existing notations to non-groupoid situations rather than duplicating notations

Does it make sense to have composition notations that work for non-invertible cells just as well as for invertible cells?

[jdchristensen]

For example, what if we allow $@ to be used for composition of not-necessarily-invertible 1-cells (and therefore, of arbitrary n-cells) in diagrammatic order? So g $@ f would be another notation for f $o g.

I don't think we should introduce a special version that only works for n >= 2, and don't see a need to distinguish composition of invertible cells from non-invertible cells.

About $@L and $@R, h $@L p currently has type h $o f $== h $o g, so it makes sense that it uses traditional order. However, if we used the first idea in this message, we could write the type as f $@ h $== g $@ h, and so diagrammatic order would make sense. And I guess we could add $oL and $oR for traditional order?

So the pattern would be that o is used for traditional order and @ for diagrammatic order.

Unfortunately, the proposed change to $@L and $@R would affect a lot of code, since they are used fairly often... It would be a simple search and replace with the new $oL and $oR, but would still cause conflicts.

[patrick-nicodemus]

For example, what if we allow $@ to be used for composition of not-necessarily-invertible 1-cells (and therefore, of arbitrary n-cells) in diagrammatic order? So g $@ f would be another notation for f $o g.

Yes, I agreed with this earlier in the comment where I suggest "wild contractibility".

I like the idea of $oL as well. I don't want to be too gung ho about breaking code but I do think the existing notation is confusing, $@@ and $@L meaning different things trips me up.

[jdchristensen]

Ok, can you suggest a concrete set of changes to make?

[patrick-nicodemus]

Okay. How about:

• $@ is diagrammatic composition in any 01-cat, $o is traditional composition in any 01-cat (consistent with existing notation, but generalizes $@ from 0-groupoids to 01-cats)
• h $@L p and p $@R h are changed from traditional order to diagrammatic order (breaking change)
• new notations $oL and $oR are added to represent whiskering in traditional order
• $@@ is generalized to horizontal composition of 2-cells in diagrammatic order (currently it represents horizontal composition of 2-cells in 1-cats)
• $= the binary relation in a 0-gpd or higher, $== for 2-cells in a 2-graph where for all 0-cells a,b, Hom a b is a 0-gpd (such as a 1-cat), $=== for 3-cells in a 3-graph where all 3-cells are invertible, i.e. Hom (A:=Hom a b) f g is a 0-gpd (such as a (2,1)-cat)
• $-> for the binary relation in a graph or higher, $=> for the binary relation in a 2-graph or higher, $==> for the binary relation in a 3-graph or higher
• No new notations for vertical composition of 2-cells,= or higher, one can use $@ or $o as preferred

[jdchristensen]

Thanks, that's a good basis for discussion. I have two comments:

1. I'm still skeptical of the idea of using a separate notation for invertible cells vs non-invertible cells. We generally only assume typeclass instances that are needed for any particular statement, so in a development about 1-categories, some results will need to use that the 2-cells are invertible, and some will not, and as a result the notation will flip back and forth between $=> and $==, which will be odd. And in particular situations, goals may be expressed using $== (because the overall result needs invertible cells), but you'll want to apply a lemma that holds for non-invertible cells, so that lemma will be expressed using $=>. This might cause unification problems for rocq, but even if not, it will cause human-comprehension problems. Cells are cells, so why not have a single notation for them?

2. If we do decide to distinguish invertible and non-invertible cells, I think the two notations should be more parallel, so the non-invertible ones should be $->, $-->, $--->.

3. If we don't distinguish invertibility of cells, I can see two options. One is that we decide on a single sequence that we use consistently. For example, $->, $=>, $==> or $->, $==, $=== or $->, $-->, $--->. Another option is that we have some synonyms for backwards compatibility. We could generalize $== to any cells in any dimensions (the same as $->), but use the one that feels right for a given situation. We could also introduce $--> and $---> to specify cells of larger dimensions. Or maybe $== could be reserved for any >= 2-cell. (Then, in a 0-groupoid, we'd have to switch to $->, or introduce a synonym $= for $->.)

Point 3 will require more discussion, but whether that discussion is needed depends on the decision about point 1. I'd like to hear what @Alizter has to say.

[jdchristensen]

I'm curious what @Alizter thinks about these questions.

[patrick-nicodemus]

Regarding point 1, I would prefer an arrow-like notation for all cells than an equality-like notation for all cells.