Homotopy as function over unit square

[mobileink]

P. 59: "Such a homotopy is the image in X of a square that fills in the space between p and q, which can be thought of as a “continuous deformation” between p and q, or a 2-dimensional path between paths."

Should read something like "Such a homotopy is a function over the unit square, whose graph forms a 2-D path between the "end paths" p and q. It can be thought of as a continuous deformation of p to q."

At the suggestion of Andrej Bauer in this thread I include a little background info about myself in order to give you some idea of where to position me relative your target audience. In high school decades ago I was something of a whiz kid in math, went to a summer school and learned enough number theory to get to p-adic numbers and quadratic reciprocity. Most of which I've forgotten. Studied calc freshman year in college using Spivak's excellent text. Drifted away from math. Got a job as a programmer. About 15 years ago started studying programming language design, automata, denotational semantics, etc. Which lead to Haskell, which lead to category theory. Also classical logic. Somewhere along the way, tried to read the official model-theoretic semantics of RDF - painful! - which lead to model theory and more logic. Have read and understood most of "Mathematical Logic" by Ebbinghaus, Flum, and Thomas. Etchemendy's "Concept of Logical Consequence." Lots of papers on logic. Somewhere along the way became enamored of intuitionism, Gentzen, Dummet, Prawitz, Jaraslav Peregrin, etc. Have read a bunch of Martin-Lof's papers. Big fan of the neopragmatists (Putnam, Rorty, etc. esp. R. Brandom and Huw Price). Started seeing references to dependent types, which eventually led me to HoTT; in general I'm more interested in how the type theory works than the mathematics. At this point I'm much more logician/philosopher (pragmatic) than mathematician. But more philologist than either - my real interest is in the early Arabic grammatical tradition (shameless plug: (http://lex.sibawayhi.org), (http://beta.sibawayhi.org)). Not as irrelevant as you might think; someday, maybe, I'll write a paper showing how the conceptual foundations of Al-Khwarizmi's algebra were laid by grammatical thinking. So if you see posts from me trying to elaborate the structure of HoTT concepts in terms of more basic concepts, or nit-picking a bit of usage, you'll know that's the philologist/philosopher speaking. Most of the suggestions I have will come from treating the HoTT book as a text to be studied and explained rather than as something I want to use to do mathematics. Textual exegesis rather than mathematical substance.

Hope that helps,

Gregg

[EgbertRijke]

I think Gregg's mainly having trouble with the word image, because functions and images don't get identified. We could think about replacing just that, and leave the rest as it is. Gregg, did I correctly identify the issue you tried to bring up?

Thanks, Egbert

2015-05-26 15:42 GMT+02:00 Gregg Reynolds notifications@github.com:

P. 59: "Such a homotopy is the image in X of a square that fills in the space between p and q, which can be thought of as a “continuous deformation” between p and q, or a 2-dimensional path between paths."

Should read something like "Such a homotopy is a function over the unit square, whose graph forms a 2-D path between the "end paths" p and q. It can be thought of as a continuous deformation of p to q."

At the suggestion of Andrej Bauer in this thread https://mail.google.com/mail/u/0/?pli=1#label/HoTT/14d7ccfc13b5ca6d I include a little background info about myself in order to give you some idea of where to position me relative your target audience. In high school decades ago I was something of a whiz kid in math, went to a summer school and learned enough number theory to get to p-adic numbers and quadratic reciprocity. Most of which I've forgotten. Studied calc freshman year in college using Spivak's excellent text. Drifted away from math. Got a job as a programmer. About 15 years ago started studying programming language design, automata, denotational semantics, etc. Which lead to Haskell, which lead to category theory. Also classical logic. Somewhere along the way, tried to read the official model-theoretic semantics of RDF - painful! - which lead to model theory and more logic. Have read and understood most of "Mathematical Logic" by Ebbinghaus, Flum, and Thomas. Etchemendy's "Concept of Logical Consequence." Lots of papers on logic. Somewhere along the way became enamored of intuitionism, Gentzen, Dummet, Prawitz, Jaraslav Peregrin, etc. Have read a bunch of Martin-Lof's papers. Big fan of the neopragmatists (Putnam, Rorty, etc. esp. R. Brandom and Huw Price). Started seeing references to dependent types, which eventually led me to HoTT; in general I'm more interested in how the type theory works than the mathematics. At this point I'm much more logician/philosopher (pragmatic) than mathematician. But more philologist than either - my real interest is in the early Arabic grammatical tradition (shameless plug: ( http://lex.sibawayhi.org), (http://beta.sibawayhi.org)). Not as irrelevant as you might think; someday, maybe, I'll write a paper showing how the conceptual foundations of Al-Khwarizmi's algebra were laid by grammatical thinking. So if you see posts from me trying to elaborate the structure of HoTT concepts in terms of more basic concepts, or nit-picking a bit of usage, you'll know that's the philologist/philosopher speaking. Most of the suggestions I have will come from treating the HoTT book as a text to be studied and explained rather than as something I want to use to do mathematics. Textual exegesis rather than mathematical substance.

Hope that helps,

Gregg

— Reply to this email directly or view it on GitHub https://github.com/HoTT/book/issues/789.

[awodey]

Image and graph are completely different things!

Sent from my iPhone

On May 26, 2015, at 11:14 AM, Egbert Rijke notifications@github.com wrote:

I think Gregg's mainly having trouble with the word image, because functions and images don't get identified. We could think about replacing just that, and leave the rest as it is. Gregg, did I correctly identify the issue you tried to bring up?

Thanks, Egbert

2015-05-26 15:42 GMT+02:00 Gregg Reynolds notifications@github.com:

P. 59: "Such a homotopy is the image in X of a square that fills in the space between p and q, which can be thought of as a “continuous deformation” between p and q, or a 2-dimensional path between paths."

Should read something like "Such a homotopy is a function over the unit square, whose graph forms a 2-D path between the "end paths" p and q. It can be thought of as a continuous deformation of p to q."

At the suggestion of Andrej Bauer in this thread https://mail.google.com/mail/u/0/?pli=1#label/HoTT/14d7ccfc13b5ca6d I include a little background info about myself in order to give you some idea of where to position me relative your target audience. In high school decades ago I was something of a whiz kid in math, went to a summer school and learned enough number theory to get to p-adic numbers and quadratic reciprocity. Most of which I've forgotten. Studied calc freshman year in college using Spivak's excellent text. Drifted away from math. Got a job as a programmer. About 15 years ago started studying programming language design, automata, denotational semantics, etc. Which lead to Haskell, which lead to category theory. Also classical logic. Somewhere along the way, tried to read the official model-theoretic semantics of RDF - painful! - which lead to model theory and more logic. Have read and understood most of "Mathematical Logic" by Ebbinghaus, Flum, and Thomas. Etchemendy's "Concept of Logical Consequence." Lots of papers on logic. Somewhere along the way became enamored of intuitionism, Gentzen, Dummet, Prawitz, Jaraslav Peregrin, etc. Have read a bunch of Martin-Lof's papers. Big fan of the neopragmatists (Putnam, Rorty, etc. esp. R. Brandom and Huw Price). Started seeing references to dependent types, which eventually led me to HoTT; in general I'm more interested in how the type theory works than the mathematics. At this point I'm much more logician/philosopher (pragmatic) than mathematician. But more philologist than either - my real interest is in the early Arabic grammatical tradition (shameless plug: ( http://lex.sibawayhi.org), (http://beta.sibawayhi.org)). Not as irrelevant as you might think; someday, maybe, I'll write a paper showing how the conceptual foundations of Al-Khwarizmi's algebra were laid by grammatical thinking. So if you see posts from me trying to elaborate the structure of HoTT concepts in terms of more basic concepts, or nit-picking a bit of usage, you'll know that's the philologist/philosopher speaking. Most of the suggestions I have will come from treating the HoTT book as a text to be studied and explained rather than as something I want to use to do mathematics. Textual exegesis rather than mathematical substance.

Hope that helps,

Gregg

— Reply to this email directly or view it on GitHub https://github.com/HoTT/book/issues/789.

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

[mobileink]

On Tue, May 26, 2015 at 10:14 AM, Egbert Rijke notifications@github.com wrote:

I think Gregg's mainly having trouble with the word image, because functions and images don't get identified. We could think about replacing just that, and leave the rest as it is. Gregg, did I correctly identify the issue you tried to bring up?

No, sorry for not being clearer: the problem is a simple grammatical ambiguity: "square that fills in the space". It's not the square that fills in the space, its the image of the square. You could fix it by adding a comma, I suppose, but to me "function over the unit square" is clearer. Plus, if it is by definition the unit square the text should say so, rather than "a square". Plus, as Colin and Andrej pointed out to me separately, "space between p and q" may not make sense.

[mobileink]

On Tue, May 26, 2015 at 10:17 AM, Steve Awodey notifications@github.com wrote:

Image and graph are completely different things!

Right, but to me the text strongly suggests that space X is two dimensional ("2-dimensional path between paths"). In that case the image in X of the function over the unit square would be a set of order pairs (a graph), no? Anyway I was thinking ink-on-paper graph. Maybe X is not necessarily 2-D, but if not, then thinking of said homotopy as a 2-D path seems unwarranted. I guess that's another ambiguity you might want to address: the way path is defined on the same page places no constraints on the co-domain (other than "set of points"). We could have a continuous function on the unit interval into R3; would that count as a path? Seems reasonable to me, but then it would be odd to call a homotopy between two such paths 2-dimensional.

In any case, I leave the wording to the experts, just wanted to point out an ambiguity.

[mikeshulman]

Why does saying "2-dimensional path between paths" suggest to you that the space X in which this happens is 2-dimensional? An ordinary path between points is 1-dimensional, but it doesn't necessarily live in a 1-dimensional space.

[mobileink]

On May 26, 2015 12:42 PM, "Mike Shulman" notifications@github.com wrote:

Why does saying "2-dimensional path between paths" suggest to you that the space X in which this happens is 2-dimensional? An ordinary path between points is 1-dimensional, but it doesn't necessarily live in a 1-dimensional space?

As the Great Cham said when asked why he defined "pastern" as "horse's knee": "Ignorance, madame, pure ignorance".

But I suspect it's an error lots of naifs will make.

Anyway the upshot (I think) is that such a homotopy need not be 2D. If the paths are in R3, the homotopy could be a wavy ribbon. OK you could say that's a 2D object embedded in R3, but that's a matter of perspective - it's points are triples, which makes it 3D, but - well, you do the math, it's also 2D, if you want to stipulate that 3D things have volume.

I reckon this stuff is trivially obvious to the professional, but its pretty subtle to the rest of us, so it gets back to just how "user friendly" you want to be to the Hoi polloi. To us (speaking ex cathedra ;) 2d anything immediately suggests R2. But I can understand why you wouldn't want to spend a lot of space disabusing us of our flatland biases.

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

[mikeshulman]

Interesting, thanks! A mathematician would never say that a wavy ribbon is itself 3-dimensional: no matter what dimension of space it lives in, the ribbon itself is 2-dimensional. I wonder if there is a small change of wording we can make that would clarify this without becoming too wordy for the mathematician reader.

[mobileink]

On May 26, 2015 2:11 PM, "Mike Shulman" notifications@github.com wrote:

Interesting, thanks! A mathematician would never say that a wavy ribbon is itself 3-dimensional: no matter what dimension of space it lives in, the ribbon itself is 2-dimensional. I wonder if there is a small change of wording we can make that would clarify this without becoming too wordy for the mathematician reader.

The simple way to do this is to provide visualizations. A half-dozen well-designed animations would make all the concepts immediately evident. Pgf/tikz supports pdf animations. A while back I made a start on an easing lib in tex that might be useful. Anybody interested in pursuing this, let me know. I probably won't have time in the near future.

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

[andrejbauer]

Videos are hard to put in a book, for now.

[mikeshulman]

Yes, I'd rather keep to technology that can be shared by readers of print copies. But more static pictures could certainly help.

[mobileink]

On May 26, 2015 4:23 PM, "Mike Shulman" notifications@github.com wrote:

Yes, I'd rather keep to technology that can be shared by readers of print copies. But more static pictures could certainly help.

Animations in a pdf file are not incompatible with nice static graphics in printed copies.

I guess I should mention something I did not put in my little bio: I'm a typesetting geek. I sat on the W3C committee that defined XSL v 1. The task of designing such a language is what drove me to start taking language theory & semantics seriously. Meaning: please do not let your current ideas of what is or is not feasible prevent you from entertaining wildly imaginative ideas about how to present Hott in v2. Anything is possible. Even holographic homotopies. Why not?

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

[mikeshulman]

What I meant by shared is that the same book should be read by everyone.

[mobileink]

On May 26, 2015 4:21 PM, "Andrej Bauer" notifications@github.com wrote:

Videos are hard to put in a book, for now.

Animations are not videos. Please take a few minutes to look at pgf/tikz. It's astounding. Any mathematician will fall in love with it immediately. You've been warned. It may be detrimental to your ordinary duties.

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

[mikeshulman]

Whether or not animations are videos, they are equally hard to print on a piece of paper.

[mobileink]

On May 26, 2015 4:42 PM, "Mike Shulman" notifications@github.com wrote:

What I meant by shared is that the same book should be read by everyone.

Define "same book". If you insist that the experience of reading a text online must be no different than the experince of reading ink on paper the kids will laff at you, and rightly so. I jest, but really, "same book" need not mean same in every way. Why on earth pass up the opportunity to illustrate concepts via animation just because paper cannot do that?

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

[mikeshulman]

The kids can laff all they want. There's nothing wrong with illustrating a concept via animation; I'm just saying that animation should not be part of The HoTT Book, because The HoTT Book is, among other things, printed on paper. I don't want one person to say "I was reading the HoTT Book and I loved the animation on page 180" and someone else to reply "I opened the copy on my shelf to page 180 but nothing moved." Instead the first person should be saying "I loved the animation supplied as supplementary material to go along with page 180 and available at X web address".

[mobileink]

On Tue, May 26, 2015 at 2:11 PM, Mike Shulman notifications@github.com wrote:

Interesting, thanks! A mathematician would never say that a wavy ribbon is itself 3-dimensional: no matter what dimension of space it lives in, the ribbon itself is 2-dimensional. I wonder if there is a small change of wording we can make that would clarify this without becoming too wordy for the mathematician reader.

A homotopy can also be 1D, no? Let f, g be distinct paths from 0 to 1 in R1. Both images are 1D objects in 1D space. A homotopy between them will be the same.

Which suggests that the "dimensionality" of a path/homotopy should be that of its domain, not its image. If so, maybe:

"Such a homotopy can be thought of as drawing a path image whose "endpoints" are paths rather than points: a 'continuous deformation' of the starting path into the ending path. We call such a homotopy 2-dimensional since its domain is a binary product. Note that the the co-domain of a homotopy and its path endpoints may be a space of any dimensionality; for example, its easy to visualize a homotopy between two (1-dimensional) paths embedded in R1, R2, or R3. [INSERT ILLUSTRATIONS] But the homotopy itself is always considered 2-dimensional, since its domain is a 2-tuple." A little on the wordy side, I guess.