homotopy type

[DanGrayson]

I wonder about this comment, where we say that we can be more precise by referring to a homotopy type, but nowhere do we say what a homotopy type is.

[bidundas]

Is this referring to the phenomenon that even in set-based mathematics when we say “the real line” it is context-dependent what topology it carries? If so, something like:

As you probably have seen from other courses, the real line - with the usual metric - is contractible, and so the unique map to a point is an equivalence. In our univalent setup that means that R=1 (the proposition is true). However, there are other legitimate uses in algebra for the field of real numbers as a discrete space, and in that incarnation the real line is a set with uncountably many elements. We shall later (in the chapters on geometry) make plenty use of ….

Bjorn

On 05 May 2021, at 23:25, Daniel R. Grayson @.***> wrote:

I wonder about this comment, where we say that we can be more precise by referring to a homotopy type, but nowhere do we say what a homotopy type is.

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

[DanGrayson]

I should have included footnote 51 in the screen shot:

[DanGrayson]

Oh, and the whole remark is relevant:

[chaikens]

I think it would help to relate what you mean by a homotopy type to the classical, set theory based definition in homotopy theory, which is a homotopy type is an equivalence class of spaces under homotopy equivalence, which is there exist maps f:X->Y, g:Y->X such that fg is homotopic to id_Y and gf is homotopic to id_X.

[DanGrayson]

I think we should remove the notion of "homotopy type" from the book -- it's too hard to pin down what one means by it. And the meaning referred to here is not the standard one, in which every type in our theory is a "homotopy type". We can be content with calling these things simply "types".

[chaikens]

It might then help to give a remark or footnote about this usage and the irrelevance of classical homotopy theory "homotopy type" to your subject. Seth

---

From: Daniel R. Grayson @.***> Sent: Sunday, September 12, 2021 3:35 PM To: UniMath/SymmetryBook Cc: Chaiken, Seth D; Comment Subject: Re: [UniMath/SymmetryBook] homotopy type (#106)

I think we should remove the notion of "homotopy type" from the book -- it's too hard to pin down what one means by it. And the meaning referred to here is not the standard one, in which every type in our theory is a "homotopy type". We can be content with calling these things simply "types".

— You are receiving this because you commented. Reply to this email directly, view it on GitHubhttps://github.com/UniMath/SymmetryBook/issues/106#issuecomment-917696946, or unsubscribehttps://github.com/notifications/unsubscribe-auth/AALVYZVDISZCE4YOBIRPXBLUBT6IZANCNFSM44FZENJA. Triage notifications on the go with GitHub Mobile for iOShttps://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Androidhttps://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.

[DanGrayson]

I think homotopy types are not relevant even in homotopy theory, since they aren't the objects of a category.

[UlrikBuchholtz]

There's a reason for Rem. 2.17.7, namely to avoid certain misunderstandings. In that particular case, it might be better to use Mike's term, shape, instead of homotopy type.

(To add to the confusion, there is a 1-category nearby, namely the homotopy category, which is the truncation of the (∞,1)-category of homotopy types. In HoTT, its type of objects (relative to a universe) is the 1-truncation of the universe. And many things in homotopy theory can indeed be studied via this 1-category, but it has limitations, which is part of what caused the development of the notions of ∞-groupoids and (∞,1)-categories in the first place.)

[chaikens]

Still, it might be a good idea to give a discussion about how your subject differs from the homotopy theory expounded in books like Hatcher's Algebraic Topology. "Homotopy Type Theory" and HoTT are here to stay!

---

From: Ulrik Buchholtz @.***> Sent: Sunday, September 12, 2021 3:57 PM To: UniMath/SymmetryBook Cc: Chaiken, Seth D; Comment Subject: Re: [UniMath/SymmetryBook] homotopy type (#106)

There's a reason for Rem. 2.17.7, namely to avoid certain misunderstandings. In that particular case, it might be better to use Mike's term, shape, instead of homotopy type.

(To add to the confusion, there is a 1-category nearby, namely the homotopy category, which is the truncation of the (∞,1)-category of homotopy types. In HoTT, its type of objects (relative to a universe) is the 1-truncation of the universe.)

— You are receiving this because you commented. Reply to this email directly, view it on GitHubhttps://github.com/UniMath/SymmetryBook/issues/106#issuecomment-917700211, or unsubscribehttps://github.com/notifications/unsubscribe-auth/AALVYZUOOTDSQTZH6I7VF3TUBUAZNANCNFSM44FZENJA. Triage notifications on the go with GitHub Mobile for iOShttps://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Androidhttps://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.

[DanGrayson]

There's probably a better way to clarify matters. What needs to be conveyed is that in topology, the real line is contractible, but for us, it's a (discrete) set. That can be done without introducing the notion of "shape", which we are not prepared to discuss.

Even the word "discrete" (imported from topology) is not a good one, applied to types, even though it is tempting to think of sets as discrete. The actual situation is that every path-component of a set is contractible. Types don't automatically come with a topology.

(I'd still like to think of this as an undergraduate textbook.)

[UlrikBuchholtz]

There's probably a better way to clarify matters. What needs to be conveyed is that in topology, the real line is contractible, but for us, it's a (discrete) set. That can be done without introducing the notion of "shape", which we are not prepared to discuss.

We may not be in a position to give more than a rough idea of the relationship between a topological space (or even a set) and the corresponding homotopy type/shape, but it's hard to convey the difference without at least giving an idea of this relationship.

Even the word "discrete" (imported from topology) is not a good one, applied to types, even though it is tempting to think of sets as discrete. The actual situation is that every path-component of a set is contractible. Types don't automatically come with a topology.

Well, it's a bit more subtle than that. There are models where types have euclidean topological structure, probed-by-compacta topological structure, or smooth structure, etc. Types definable without axioms in a sense carry all these possible structures, and for instance the Dedekind reals acquire their usual topology in first two models alluded to. And it's possible to “probe” these structures internally to various extents. “Discreteness” is quite well-approximated by having decidable equality. Other topological notions can also be captured, as in work by Escardó. (I'm not sure how best, or whether, to convey this subtlety in the book, however.)

(I'd still like to think of this as an undergraduate textbook.)

And I second that.

[chaikens]

Hi, My naive reaction to Hott, even before getting into univalence, as an old dog liking to learn new tricks, was that path induction is a mysterious and magical property. It (unlike other rules for judgement and judgemental equality) didn't seem true except when type families and sections behaved in some restricted and special ways. (I learned that from writings that type families have properties of fibration, namely path lifting.) I think I understand now that path induction, like all other rules, constrains what a mathematical object can be in order for it be a model for type theory (correct?) Note I purposely avoided any language of category theory (like homotopies in model categories), since I'm interested in an undergraduate level understanding. I wonder if it would help to give an informal discussion of some models in terms of ordinary mathematics. Say beginning with sets (which I understand what ML had in mind to deal with by inventing the identity types), then giving one or a few examples where path types are non-trivial; perhaps elaborating on Euclidean space and congruences (digressing on how properties we need follow from the Euclidean metric and congruence as a distance preserving map). Would that foreshadow your book's theme of symmetry?

Was it historically a surprise when useful models of ML type theory with non-trivial identity types were found? Perhaps discussion on that would strengthen interestingness.

I guess my ulterior motive is to see how paths can be between things like proofs, say in algebra, or that a function between discrete structures is a bijection; things done in combinatorics.

Thanks for your patience, and I hope my comments help. Seth

---

From: Ulrik Buchholtz @.***> Sent: Monday, September 13, 2021 3:45 PM To: UniMath/SymmetryBook Cc: Chaiken, Seth D; Comment Subject: Re: [UniMath/SymmetryBook] homotopy type (#106)

There's probably a better way to clarify matters. What needs to be conveyed is that in topology, the real line is contractible, but for us, it's a (discrete) set. That can be done without introducing the notion of "shape", which we are not prepared to discuss.

We may not be in a position to give more than a rough idea of the relationship between a topological space (or even a set) and the corresponding homotopy type/shape, but it's hard to convey the difference without at least giving an idea of this relationship.

Even the word "discrete" (imported from topology) is not a good one, applied to types, even though it is tempting to think of sets as discrete. The actual situation is that every path-component of a set is contractible. Types don't automatically come with a topology.

Well, it's a bit more subtle than that. There are models where types have euclidean topological structure, probed-by-compacta topological structure, or smooth structure, etc. Types definable without axioms in a sense carry all these possible structures, and for instance the Dedekind reals acquire their usual topology in first two models alluded to. And it's possible to “probe” these structures internally to various extents. “Discreteness” is quite well-approximated by having decidable equality. Other topological notions can also be captured, as in work by Escardóhttps://www.cs.bham.ac.uk/~mhe/TypeTopology/. (I'm not sure how best, or whether, to convey this subtlety in the book, however.)

(I'd still like to think of this as an undergraduate textbook.)

And I second that.

— You are receiving this because you commented. Reply to this email directly, view it on GitHubhttps://github.com/UniMath/SymmetryBook/issues/106#issuecomment-918519621, or unsubscribehttps://github.com/notifications/unsubscribe-auth/AALVYZT7DKCRDZMRED3MOB3UBZIFNANCNFSM44FZENJA. Triage notifications on the go with GitHub Mobile for iOShttps://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Androidhttps://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.

[DanGrayson]

We've moved the remark about homotopy types to an appendix subsection, which will be expanded to tie type theory to topology. Not all of our students will know topology.

I think the discussion of "models" will just confuse undergraduates. We intend this to be an algebra course, not a logic course.

The idea is not that paths can be like proofs -- rather, the idea is that any two proofs of a proposition can be joined by a path, whereas any two constructions of a group can be joined by a path only if the groups are isomorphic. It's hard to visualize transitioning gradually from one group to another (isomorphic) group, so think instead of two congruent geometric figures in Euclidean space. There one can easily envision moving gradually from one to the other. And think of an equilateral triangle in the plane -- it is congruent to itself in 6 different ways, depending on how you set up the congruence. That gives 6 paths from it to itself in the type of plane triangles.

The chapter on Euclidean geometry is rudimentary at this point -- eventually all that has to be clarified.

Thank you for your helpful feedback!

[DanGrayson]

Closing, because the remark is now in an appendix, and will be clarified later, in due course.

[chaikens]

Thanks for the discussion! You've clarified my understanding and I agree about closing an issue.

My one closing remark is that undergraduates would and ought to be concerned with what mathematical structures they know, or should be given examples of, for which all the machinery and results they are learning are true, i.e. can be applied to. And (I'd like more of) what situations one should know that HoTT doesn't apply to. We needn't muddy the waters by developing mathematical logic or topology here. But discussing elementary enough examples always helps in algebra. So I used the word "model" in this informal sense, and don't suggest developing logic more than you doing to pursue the book's themes.

Thanks again, and I've found your book enlightening, and look forward to reading more as it's developed.

Seth

---

From: Daniel R. Grayson @.***> Sent: Thursday, September 16, 2021 4:12 PM To: UniMath/SymmetryBook Cc: Chaiken, Seth D; Comment Subject: Re: [UniMath/SymmetryBook] homotopy type (#106)

We've moved the remark about homotopy types to an appendix subsection, which will be expanded to tie type theory to topology. Not all of our students will know topology.

I think the discussion of "models" will just confuse undergraduates. We intend this to be an algebra course, not a logic course.

The idea is not that paths can be like proofs -- rather, the idea is that any two proofs of a proposition can be joined by a path, whereas any two constructions of a group can be joined by a path only if the groups are isomorphic. It's hard to visualize transitioning gradually from one group to another (isomorphic) group, so think instead of two congruent geometric figures in Euclidean space. There one can easily envision moving gradually from one to the other. And think of an equilateral triangle in the plane -- it is congruent to itself in 6 different ways, depending on how you set up the congruence. That gives 6 paths from it to itself in the type of plane triangles.

The chapter on Euclidean geometry is rudimentary at this point -- eventually all that has to be clarified.

Thank you for your helpful feedback!

— You are receiving this because you commented. Reply to this email directly, view it on GitHubhttps://github.com/UniMath/SymmetryBook/issues/106#issuecomment-921211863, or unsubscribehttps://github.com/notifications/unsubscribe-auth/AALVYZTN5UTZ27TWC3E4HIDUCJFS7ANCNFSM44FZENJA. Triage notifications on the go with GitHub Mobile for iOShttps://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Androidhttps://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.