there are various ways in which diagrams of paths are drawn

[EgbertRijke]

There seem to be at least two different ways in which we draw diagrams of paths. One is with arrows (e.g. the diagram illustrating Eckman-Hilton) and in others we use =. Shouldn't all of these be in the same style?

[awodey]

one should not draw diagrams with ===, or ~~~~, etc., arrows are just fine.
the context makes it clear that the arrows are identitiies.
if a diagram has a mixture of identities and others and one needs to indicate which are which,
an arrow can be labelled with an = sign -- just as when indicating that something is an iso or an equivalence.

On May 3, 2013, at 8:56 AM, EgbertRijke notifications@github.com wrote:

There seem to be at least two different ways in which we draw diagrams of paths. One is with arrows (e.g. the diagram illustrating Eckman-Hilton) and in others we use =. Shouldn't all of these be in the same style?

—
Reply to this email directly or view it on GitHub.

[DanGrayson]

A single arrow might be confusing for the reader, since it bears to
resemblance to the equal sign from which it arose. Note that we are
already using double arrows for the identities between identities, as in
the Eckmann-Hilton argument. What about using double arrows for all
identities, the justification being that using ==== in a diagram fails to
show the orientation, and that ====> looks like === with orientation added,
reminding the user it's an identity?

On Fri, May 3, 2013 at 6:03 AM, Steve Awodey notifications@github.comwrote:

one should not draw diagrams with ===, or ~~~~, etc., arrows are just
fine.
the context makes it clear that the arrows are identitiies.
if a diagram has a mixture of identities and others and one needs to
indicate which are which,
an arrow can be labelled with an = sign -- just as when indicating that
something is an iso or an equivalence.

On May 3, 2013, at 8:56 AM, EgbertRijke notifications@github.com wrote:

There seem to be at least two different ways in which we draw diagrams
of paths. One is with arrows (e.g. the diagram illustrating Eckman-Hilton)
and in others we use =. Shouldn't all of these be in the same style?

—
Reply to this email directly or view it on GitHub.

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/192#issuecomment-17392902
.

[awodey]

diagrams drawn with all ==== look awful.

[mikeshulman]

I don't agree that diagrams of equalities look awful, and I do think there is potential for confusion, especially because when the vertices of a diagram are types, an arrow could mean both a function or an equality. We start using commutative diagrams of paths before we start using them for functions, so I can easily see a reader being confused when the latter start popping up if we were using arrows in diagrams for paths. I pushed an experiment to see what it would look like to use === for diagrams of equalities (easy to revert); I think it looks just fine.

[DanGrayson]

It looks fine to me. I suppose the orientation of the identities, not
indicated in the diagram, can be deduced easily from the text.

On Wed, May 8, 2013 at 3:44 PM, Mike Shulman notifications@github.comwrote:

I don't agree that diagrams of equalities look awful, and I do think there
is potential for confusion, especially because when the vertices of a
diagram are types, an arrow could mean both a function or an equality.
We start using commutative diagrams of paths before we start using them for
functions, so I can easily see a reader being confused when the latter
start popping up if we were using arrows in diagrams for paths. I pushed an
experiment to see what it would look like to use === for diagrams of
equalities (easy to revert); I think it looks just fine.

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/192#issuecomment-17632587
.

[mikeshulman]

And the commutativity of a diagram of identities is independent of their
orientation anyway.
On May 9, 2013 8:31 AM, "Daniel R. Grayson" notifications@github.com
wrote:

It looks fine to me. I suppose the orientation of the identities, not
indicated in the diagram, can be deduced easily from the text.

On Wed, May 8, 2013 at 3:44 PM, Mike Shulman notifications@github.comwrote:

I don't agree that diagrams of equalities look awful, and I do think
there
is potential for confusion, especially because when the vertices of a
diagram are types, an arrow could mean both a function or an equality.
We start using commutative diagrams of paths before we start using them
for
functions, so I can easily see a reader being confused when the latter
start popping up if we were using arrows in diagrams for paths. I pushed
an
experiment to see what it would look like to use === for diagrams of
equalities (easy to revert); I think it looks just fine.

—
Reply to this email directly or view it on GitHub<
https://github.com/HoTT/book/issues/192#issuecomment-17632587>
.

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/192#issuecomment-17670728
.

[awodey]

I guess it is a matter of taste; I find such diagrams needlessly cluttered. A normal digram of arrows serves the purpose just as well -- the fact that these arrows are identities is known, so it need not be displayed by special arrows. For example, you wouldn't draw a diagram of arrows in a groupoid as isomorphisms, with double shafts and a huge wavy lines. But I will not argue it further if others like it better this way.

[DanGrayson]

In category theory, identities are arrows (maps). In type theory,
identities and arrows (functions) are different types of things.

On Sat, May 11, 2013 at 11:10 PM, Steve Awodey notifications@github.comwrote:

I guess it is a matter of taste; I find such diagrams needlessly
cluttered. A normal digram of arrows serves the purpose just as well -- the
fact that these arrows are identities is known, so it need not be displayed
by special arrows. For example, you wouldn't draw a diagram of arrows in a
groupoid as isomorphisms, with double shafts and a huge wavy lines. But I
will not argue it further if others like it better this way.

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/192#issuecomment-17772198
.

[andrejbauer]

Ok, but can we at least decrease the number of different ways? Right now we use \ar@{=} and \ar@{-} and \ar.

[mikeshulman]

Where do we use \ar@{-} or \ar to mean paths now?

On Sun, May 12, 2013 at 2:46 PM, Andrej Bauer notifications@github.comwrote:

Ok, but can we at least decrease the number of different ways? Right now
we use \ar@{=} and \ar@{-} and \ar.

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/192#issuecomment-17785992
.

[andrejbauer]

There was a tikzpicture which used that. I converted it to xypic. But then I changed it to \ar@{=}, so at least we now have at most two ways of displaying paths, as ordinary arrows and as prolonged equality signs. I tihnk arrows are used in the Eckmann-Hilton argument, and elsewhere we mostly have equalities.

[mikeshulman]

Where do we still use ordinary arrows?

On Mon, May 13, 2013 at 9:35 AM, Andrej Bauer notifications@github.comwrote:

There was a tikzpicture which used that. I converted it to xypic. But then
I changed it to \ar@{=}, so at least we now have only two ways of
displaying paths, as ordinary arrows and as prolonged equality signs.

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/192#issuecomment-17823713
.

[andrejbauer]

Eckmann-Hilton, I think.

[awodey]

please, no giant equals signs there …

On May 13, 2013, at 3:01 PM, Andrej Bauer notifications@github.com wrote:

Eckmann-Hilton, I think.

—
Reply to this email directly or view it on GitHub.

[andrejbauer]

But they would like a bit like rainbows because they're bent...

[mikeshulman]

Hmm, okay. EH is a problem; I think the rainbows are too much even for me. What if we say there something like "We represent paths by arrows here to match the common usage in higher category theory"? I think we haven't used any commutative diagrams yet at this point, and the situation we're drawing is a bit different, so hopefully it won't be too confusing.

[awodey]

the text calls them "1-paths" and "2-paths" and clearly states that they are depicted in the diagram.
I don't think there is any chance the reader will be confused.

On May 13, 2013, at 5:50 PM, Mike Shulman notifications@github.com wrote:

Hmm, okay. EH is a problem; I think the rainbows are too much even for me. What if we say there something like "We represent paths by arrows here to match the common usage in higher category theory"? I think we haven't used any commutative diagrams yet at this point, and the situation we're drawing is a bit different, so hopefully it won't be too confusing.

—
Reply to this email directly or view it on GitHub.

[mikeshulman]

I added a brief remark in 45e32e1, is that okay?

On Mon, May 13, 2013 at 2:56 PM, Steve Awodey notifications@github.comwrote:

the text calls them "1-paths" and "2-paths" and clearly states that they
are depicted in the diagram.
I don't think there is any chance the reader will be confused.

On May 13, 2013, at 5:50 PM, Mike Shulman notifications@github.com
wrote:

Hmm, okay. EH is a problem; I think the rainbows are too much even for
me. What if we say there something like "We represent paths by arrows here
to match the common usage in higher category theory"? I think we haven't
used any commutative diagrams yet at this point, and the situation we're
drawing is a bit different, so hopefully it won't be too confusing.

—
Reply to this email directly or view it on GitHub.

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/192#issuecomment-17843755
.

[awodey]

very good

On May 13, 2013, at 6:00 PM, Mike Shulman notifications@github.com wrote:

I added a brief remark in 45e32e1, is that okay?

—
Reply to this email directly or view it on GitHub.

[mikeshulman]

Can we close this issue now?