Commutativity of diagrams

[marcbezem]

Recently we became more strict on calling a diagram commutative. We currently have two variants (see Sec. 2.15): commutative by definition, and commutative when all function types are set s(so that commutativity of the diagram is a proposition). There are quite a few cases in which neither of these variants apply. I think we miss good terminology in such cases, e.g., the diagram in Cor. 3.1.3. Unfortunately, this diagram doesn't commute by definition, as conjugation with the reflexivity path is not definitionally equal.

There are a couple of solutions here, including:

1. Introduce a third variant in Ch.2: commutativity up to $\eqto$ (some HoTT texts use "commutativity up to homotopy", but don't single out the propositional case).
2. Blur the distinction, call all such diagrams commutative, that is, go back to the old terminology.

For the moment, before having heard your opinions, my preference is 1. I used this already in 3.1.3, so you can see how it looks. Please give me you opinions.

PS Solution 2 could be made more like 1 by annotating the diagram in the middle by $\jdeq$, $=$ and $\eqto$ in the respective cases. One could speak of $\jdeq$-, $=$- and $\eqto$-commutative, and be allowed to omit the prefix (or not).

[DanGrayson]

I prefer 1 -- and a good term would be "homotopy commutative".

[bidundas]

I generally prefer avoiding the term “homotopy” and I support the dogma that a diagram is a type unless otherwise stated. If, by chance, the type is a proposition a witness needs no name and in that case “commutes” is a synonyme for True.

Bjorn

On 14 Mar 2023, at 02:22, Daniel R. Grayson @.***> wrote:

I prefer 1 -- and a good term would be "homotopy commutative".

— Reply to this email directly, view it on GitHub, or unsubscribe. You are receiving this because you are subscribed to this thread.

[marcbezem]

I agree with Bjørn on both points.

• "homotopy" refers to an advanced mathematical subject that comes after several calculus courses and at least an introduction in topology. We try hard to keep our book on the undergraduate level, as an alternative introduction to group theory. This is at odds with using terminology from more advanced topics. For the same reason we avoid terminology of category theory, even the most elementary.

• "diagram is a type" even an identity type (or equality by definition). Complicated diagrams can even represent several identity types. Consequently, the same conventions should apply to identity types and to diagrams.

[pierrecagne]

I also agree with Bjørn. We try to avoid references to the homotopy language in the rest of the book.

I suggest we do the same as when we refer to displayed unnamed equivalences. By which I mean, it is frequent in the book that we say things like

we can now construct an equivalence of type
\[
   some-type \equivto some-other-type
\]

We can do the same for diagram:

we can now construct an element of type
\[
   diagram
\]

(I think this is pretty much what Bjørn suggests.)

[marcbezem]

I added a few sentences to 2.15:

"In general, a diagram is a visual way to express identity types. For example, if in the above diagram the type $X\to T$ is not a set, then the diagram expresses the identity type $g \circ p \eqto q \circ f$."

and

"Such diagrams are again a visual way to express identity types. For example, the above diagram expresses the identity type $g \circ p \eqto q \circ f$. For a concrete example, see the naturality square in \cref{def:naturality-square}."

All this is a compromise of course, e.g., a span is not a diagram in this sense. Also, in the wild category of types, the diagram for the terminal object T = 1 does not commute under the strict definition of commutativity (which I didn't change): even though X->1 is a set, X->S may not be a set. But it should cover most of the uses of diagrams in the book.

Please take a look, if everybody is happy with this we can close the issue.

[DanGrayson]

It looks good, but a question will arise. In diagrams that consist of multiple squares, do we posit identifications between induced identifications?

[marcbezem]

Yes, that is one of the questions that can arise. Let's explore an example. Consider a,b: X->Y and c,d: Y->Z. Lots of paths X->Z! Assume we pick ca,db: X->Z and have identifications a\eqto b and c\eqto d. Do we posit a specific identification ca\eqto db? Plus what Bjørn said during the zoom (at least how I understood it): is direction of the identification of a with b (and of c with d) clear from the diagram? I think this is too hard for 2.6. Perhaps a margin note indicating these complications is the best we can do at this point?

[bidundas]

This issue is present even in dimension 1 if we write something like a->b->c (which I do think we should allow ourselves). Does a witness just witness a->b and b->c or also a->c - and perhaps even some cells of higher dimensions (people who enjoy ghosts can even contemplate hidden degeneracies involving invisible refls).

I suggest that a diagram is the finest possible type and does not involve “outer diagrams” one can get by merging smaller pieces (ie only the first interpretation in the example above. Even so, it is probably possible to construct awkward examples, but I think this can be solved case-by-case if confusion is possible.

Bjorn

On 20 Mar 2023, at 18:39, Marc Bezem @.***> wrote:



Yes, that is one of the questions that can arise. Let's explore an example. Consider a,b: X->Y and c,d: Y->Z. Lots of paths X->Z! Assume we pick ca,db: X->Z and have identifications a\eqto b and c\eqto d. Do we posit a specific identification ca\eqto db? Plus what Bjørn said during the zoom (at least how I understood it): is direction of the identification of a with b (and of c with d) clear from the diagram? I think this is too hard for 2.6. Perhaps a margin note indicating these complications is the best we can do at this point?

— Reply to this email directly, view it on GitHubhttps://github.com/UniMath/SymmetryBook/issues/183#issuecomment-1476667271, or unsubscribehttps://github.com/notifications/unsubscribe-auth/AKO2SKZF7I7GZ5HUDVMTOVLW5CI3RANCNFSM6AAAAAAVYF52S4. You are receiving this because you commented.Message ID: @.***>

[marcbezem]

A -f-> B -g-> C is currently not a diagram. I once proposed to turn it into a diagram that commutes by definition by adding by default A -gf-> C. This is admittedly ad hoc and will not solve every problem.

We even had A -f-> B -g-> C as an alternative notation for the composition gf for some time, until it was voted down. But I somehow liked it, and feel less alone now (thanks Bjørn :-)

[bidundas]

Sorry if I was unclear. I chose a 1d example to illustrate the point which extends to two and more dimensions. My suggested convention is exactly NOT to add composite cells. (Whether we call it a diagram when it doesn’t have 2-cells … I guess if pressed I’d allow it. For all I know a b and c may themselves be arrow or identity types). Segal would, as you suggest, add composite cells in order to have full functoriality wrtthe various imaginable projections, a thing that is not so pressing when considering a concrete diagram.

Under my convention a->b is a type, a->^fb is a point, two parallel arrows is a sigma type, but if the arrows are marked with predefined names, it is just the type of paths between the named arrows. Likewise, three parallel arrows is the pullback of two types of parallel (named or not) arrows along the type of the middle arrow.

There are ambiguities.

Bjorn

On 20 Mar 2023, at 19:12, Marc Bezem @.***> wrote:



A -f-> B -g-> C is currently not a diagram. I once proposed to turn it into a diagram that commutes by definition by adding by default A -gf-> C. This is admittedly ad hoc and will not solve every problem.

— Reply to this email directly, view it on GitHubhttps://github.com/UniMath/SymmetryBook/issues/183#issuecomment-1476714832, or unsubscribehttps://github.com/notifications/unsubscribe-auth/AKO2SK2PWWIUNIEYBB4N2ETW5CMYZANCNFSM6AAAAAAVYF52S4. You are receiving this because you commented.Message ID: @.***>

[marcbezem]

@bidundas Then I don't understand the suggestion. Is A -f-> B -g-> C just two points? Isn't the finest possible interpretation of, e.g., a square as in 2.15 just four points, since we do not implicitly compose?

[bidundas]

It is one point in the type a->b->c (and so a pair). I think we agree, or at least I think what you wrote at the end of 2.15 is very good.

Bjorn

On 20 Mar 2023, at 20:08, Marc Bezem @.***> wrote:



@bidundashttps://github.com/bidundas Then I don't understand the suggestion. Is A -f-> B -g-> C just two points? Isn't the finest possible interpretation of, e.g., a square as in 2.15 just four points, since we do not implicitly compose?

— Reply to this email directly, view it on GitHubhttps://github.com/UniMath/SymmetryBook/issues/183#issuecomment-1476790940, or unsubscribehttps://github.com/notifications/unsubscribe-auth/AKO2SK6YVNUOND6PSU5WRRTW5CTJ7ANCNFSM6AAAAAAVYF52S4. You are receiving this because you were mentioned.Message ID: @.***>

[marcbezem]

As a result of our discussion I added the following footnote: \footnote{When diagrams get more complicated, the information they convey is not always sufficient to find out which identity type(s) they express. In such cases additional information will be provided.}%

Moreover I went through all diagrams in Chapter 2. Here are the additions/modifications:

• Exc. 2.17.12, added: "visualized by the following diagram\footnote{This diagram actually commutes by definition.}". I could have changed $f\eqto i\circ p$ to $f\jdeq i\circ p$ but didn't, since $\eqto$ is used in the contractible type.
• Def. 2.21.1, below, "diagram" ---> "picture" because of the vertical $\mapsto$'s.
• IoC 2.26.1, above diagram with dashed arrow, added after "there is a contractible type of extensions": $\sum{y:B}((\blank\mapsto y) \eqto{(\trunc\blank_{n+1}^{-1}(z))\to B}(g \circ \fst))$, visualized by ... @UlrikBuchholtz pls check I got this right
• (2.27.1) left as is, "described" is OK, diagram commutes by definition

[UlrikBuchholtz]

• IoC 2.26.1, above diagram with dashed arrow, added after "there is a contractible type of extensions": …

Looks good!

[marcbezem]

@UlrikBuchholtz Please take also a look at the last paragraph + thm of 2.27. I made it self-contained, apart from the proof of Thm. 2.27.4. I added a reference to 3.9 in Footnote 81. However, I think the paragraph + thm is now obsolete because of 3.9 and could be deleted.

[UlrikBuchholtz]

Looks good!