You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Peiyuan Zhu (Oct 16 2022 at 00:40): Peiyuan Zhu (Oct 16 2022 at 00:41):I was reading this note Structuralism, Invariance, and Univalence of Steve Awodey
Peiyuan Zhu (Oct 16 2022 at 00:42):
Peiyuan Zhu (Oct 16 2022 at 00:43):It resonates a lot with this page written by relationalism economist GLS Shackle in his book Decision, Order, and Time in Human Affairs.
Peiyuan Zhu (Oct 16 2022 at 00:52):I'm thinking in Dempster-Shafer theory, a statistical judgement is a probabilistic functor from a category of sensorimotor states to a category of concepts. The sensorimotor states that are analogous to one another are statistical distributions that are homotopy equivalent to one another.
Morgan Rogers (he/him) (Oct 16 2022 at 11:43):@Peiyuan Zhu what's the question?
Peiyuan Zhu (Oct 18 2022 at 07:08):Is this understanding capturing the structuralism idea in homotopy theory?
Peiyuan Zhu (Oct 25 2022 at 13:16):I wonder if the semantics of HoTT as propositions and sets have deeper meanings. In Dempster-Shafer theory propositions are modelled as sets. HoTT people usually tell me HoTT is just providing a group of syntax and semantics are what you're supposed to give, and you can either consider it in case of propositions or sets. But in Dempster-Shafer theory a proposition is represented by a set up to imprecision.
Peiyuan Zhu (Oct 25 2022 at 13:33):
Peiyuan Zhu (Oct 25 2022 at 13:36):"Most of these students, myself included, find it difficult to see how so slight and formal an object as a proposition can, in itself and without reference to the experience by which we come to know it, provide positive but partial support to other propositions."
Notification Bot (Oct 25 2022 at 13:46):10 messages were moved here from #learning: questions > beginner questions by Morgan Rogers (he/him).
Peiyuan Zhu (Oct 25 2022 at 13:47):It sounds like an radical empiricism / empiricism argument.
Peiyuan Zhu (Oct 25 2022 at 13:48):I just recall this paragraph from Zen and the Art of Motorcycle Maintenance P133: "Hume has been saying, in effect, that everything I know about this
motorcycle comes to me through my senses. It has to be. There's no other
way. If I say it's made of metal and other substances, he asks, What's metal?
If I answer that metal's hard and shiny and cold to the touch and deforms
without breaking under blows from a harder material, Hume says those are
all sights and sounds and touch. There's no substance. Tell me what metal is
apart from these sensations. Then, of course, I'm stuck."
Morgan Rogers (he/him) (Oct 25 2022 at 13:49):I think you're going to need to express more of your thinking process in words in order for anyone to be able to contribute to this discussion.
Peiyuan Zhu (Oct 25 2022 at 13:52):Peiyuan Zhu said:
I wonder if the semantics of HoTT as propositions and sets have deeper meanings. In Dempster-Shafer theory propositions are modelled as sets. HoTT people usually tell me HoTT is just providing a group of syntax and semantics are what you're supposed to give, and you can either consider it in case of propositions or sets. But in Dempster-Shafer theory a proposition is represented by a set up to imprecision.
Do you think this question make sense?
Peiyuan Zhu (Oct 25 2022 at 14:02):@Morgan Rogers (he/him)
Tobias Schmude (Oct 25 2022 at 14:06):While I can't say anything about Dempster-Shafer theory, it might be worth noting that in HoTT not every type is a proposition or a set, but generally corresponds to a homotopy type of a space. This is made precise by the simplicial model (Kapulkin-Lumsdaine after Voevodsky) and the proof that identity types endow types with the structure of -groupoids (van den Berg-Garner and Lumsdaine).
Propositions and sets are special cases, defined by contractibility of (higher) identity types. In particular, propositions are sets, without any imprecision!
Peiyuan Zhu (Oct 30 2022 at 23:06):What is the philosophical underpinning of homotopy type? I can see that for sets and propositions, but I cannot find a situation that homotopy type is sensible?
Henry Story (Oct 31 2022 at 01:58):You may want to read the book "Modal HoTT" which is written by David Corfield, a philosopher who also was aparently one of the founders with John Baez of the nlab or the cafe. https://www.schweitzer-online.de/buch/Corfield/Modal-Homotopy-Type-Theory/9780198853404/A52722040/ I think that book would have been a bit more readable with diagrams.
Peiyuan Zhu (Oct 31 2022 at 02:10):I saw this hierarchy before. How can I understand it? image.png
Peiyuan Zhu (Oct 31 2022 at 02:10):Seems relevant, but the explanation is ver little from the book
Henry Story (Oct 31 2022 at 02:11):There was a whole summer course on cubical Agda where they went into all that.
https://www.youtube.com/playlist?list=PLtIZ5qxwSNnzpNqfXzJjlHI9yCAzRzKtx
Peiyuan Zhu (Oct 31 2022 at 02:56):I think they barely talked about philosophy so it's only at the syntax level I believe? But I'm trying to give it some meaning so I can get into it (relate it to real life situation, I mean, intuitionism is about some feelings anyways right?)
Henry Story (Oct 31 2022 at 02:59):Well Cubical Agda is Hott implemented in a proof assistant you can use directly to improve your intuitions. At the end of the course there are some very interesting applications to computing. The book by Corfield is directly looking at how HoTT affects philosophical thinking. Use Cubical Agda to gain intuitions about HoTT and that will help understand the philosophical implications.
Peiyuan Zhu (Oct 31 2022 at 03:13):Ok it's gonna take some time to go through this lecture. I would really hope I can have a solid question in mind tho. Can you give a bit of hint of how homotopy become relevant to intuition? The only place that I can recall it from university math is topology. I never used it myself, but looks interesting. I saw that at the end of the lecture series they started to talk about group without group which seems to be answering the question that I have? David Cortfield cited Ernst Cassier on several occasions, who seems to have contributed to relationalism physics. What's your take on this? How to understand relationalism philosophy in this context?
Peiyuan Zhu (Oct 31 2022 at 03:13):
Peiyuan Zhu (Oct 31 2022 at 03:14):I think this is where David cited this about perception. Do you recommend going through the whole lecture before trying to understand questions like this?
Mike Shulman (Oct 31 2022 at 04:58):Henry Story said:
Well Cubical Agda is Hott implemented in a proof assistant you can use directly to improve your intuitions. At the end of the course there are some very interesting applications to computing. The book by Corfield is directly looking at how HoTT affects philosophical thinking. Use Cubical Agda to gain intuitions about HoTT and that will help understand the philosophical implications.
FWIW, there is nothing specific to cubical type theory here, all of that makes perfect sense in any form of HoTT. I would argue that in some ways, Book HoTT is better for gaining intuitions than cubical type theory, because in cubical type theory you have to worry about this additional weird "interval" thing that is kind of a type and kind of not a type. So I would recommend a proof assistant for Book HoTT, such as the HoTT Coq library or one of the Agda HoTT libraries, at least as much as cubical agda to a newcomer. (Cubical agda also has some warts due to its in-progress nature.)
Mike Shulman (Oct 31 2022 at 05:00):Regarding introductions for philosophers, my paper Homotopy Type Theory: A synthetic approach to higher equalities was written with a philosophical audience in mind.
Peiyuan Zhu (Oct 31 2022 at 05:14):I didn't see any discussion on "events" in your paper there, but it seems to be an important discussion in David Cortfield's book.
Peiyuan Zhu (Oct 31 2022 at 05:15):
Peiyuan Zhu (Oct 31 2022 at 05:31):"What homotopy type theory
does is take observations such as these not merely as an analogy, but as the first steps of a
series of levels."
How to understand this?
Peiyuan Zhu (Oct 31 2022 at 06:58):
Peiyuan Zhu (Oct 31 2022 at 06:58):What does the "cohesion" mentioned here has to do with cohesive topos?
Henry Story (Oct 31 2022 at 07:39):I think Basic Dependent Type Theory is used in programming (something close is used in Scala), and it is very helpful there as well as in mathematics (see the Lean program from Imperial). Corfields argument is that philosphers of the analytic tradition who build on the tradition of Bertrand Russel, author of Principia Mathematica, should take Dependent type theory seriously, and then HoTT as an extension of that, as that is where mathematics has moved. His book also points to limitations in modal logic and future work along those lines.
As a software engineer I am particularly interested in the computational power HoTT as it brings the promise to be able to take proofs on simple models and have them translated nearly automatically to more complex models. Eg. Numers with just the successor function and binary numbers that are much more efficient. The last lectures of the Cubical Hott course look at that. But apparently one cannot yet translate cubical Agda programs to Haskell (or I'd love it if it could be Scala, or if one could just program directly in it)...
Morgan Rogers (he/him) (Oct 31 2022 at 16:29):Peiyuan Zhu said:
I didn't see any discussion on "events" in your paper there, but it seems to be an important discussion in David Cortfield's book.
Why should another writer be expected to use the language that Corfield does? His terminology is derived from his interpretation of the theory, not the other way around, and "events" certainly aren't an elementary/foundational concept in HoTT, unless they refer to something with another name in the theory.
Peiyuan Zhu (Oct 31 2022 at 17:35):Mike Shulman said:
Regarding introductions for philosophers, my paper Homotopy Type Theory: A synthetic approach to higher equalities was written with a philosophical audience in mind.
How to understand the part about seeing different versions of the same reality better? In the paper you mentioned Gauge invariance. Is this a good entry point to this topic?
Peiyuan Zhu (Nov 01 2022 at 00:00):
Peiyuan Zhu (Nov 01 2022 at 00:18):image.png
Is there a way I can understand this development better in details?
Peiyuan Zhu (Nov 02 2022 at 19:57):image.png
How to understand what he calls "hypersets"? Is it self-reference that he talks about? How to understand this topic better? It seems like he's touching some fundamental problems of mathematics. Link to document: https://hal.archives-ouvertes.fr/hal-03779948/document
Jason Erbele (Nov 02 2022 at 20:52):@Peiyuan Zhu, this is not an answer to your question (or your previous one), but more of an observation that will hopefully help you to ask questions that more people are more willing to answer. You will probably get better participation and engagement if your questions are self-contained. Links and excerpts are good for pointing to supplementary things, but if someone has to click on a link or picture to even know what you're talking about, most of the time most people won't bother, even when they could have helped.
To use your previous question as an example, compare:
"Is there a way I can understand this development better in details? [image]"
with:
"In [paper], [author] develops the idea of [idea]. Is there a way I can understand this development better in details? [image]"
In the first case there's nothing to indicate whether I might have anything constructive to add until I click the image. The second case gives context. Now the image is a convenient reference. If I know something about the topic, I'm more likely to click on the image in the second case.
Jason Erbele (Nov 02 2022 at 20:52):Your latest question is a little better – I know you're talking about what someone calls hypersets, but I don't know who "he" is. I can see you left a link to a french website, so should I even bother going there if I don't speak French? If that's a link to the full document, "The full document can be found here: [link]" provides useful context.
Peiyuan Zhu (Nov 02 2022 at 21:02):It's a document written in English and that's the link to the full document
Peiyuan Zhu (Nov 02 2022 at 21:05):I think he's discussing a history of Bourbaki group that went on with only binary relations, but there's more about multinary relations, and I think he's implying that it's not contained in category theory
Peiyuan Zhu (Nov 02 2022 at 21:06):He did give a self-referrential definition of hyperset, but I'm confused about the definition by itself
Peiyuan Zhu (Nov 02 2022 at 21:06):Here's the definition image.png
Peiyuan Zhu (Nov 03 2022 at 15:34):My main question is I don't understand what hypersets are. Does he mean subsets without additional structures inherited from the set itself, like metric, etc? Or does he mean hyperset of Peter Aczel, Barwise, Perry?
Kenji Maillard (Nov 03 2022 at 15:39):No, from your quote the terminology hyperset is just a not-so-usual way to call the powerset of a set (= the set of subsets of a given set).
Peiyuan Zhu (Nov 03 2022 at 16:01):But how to make sense of that recursive definition?
Peiyuan Zhu (Nov 03 2022 at 16:07):Is "hyperset of order" the same as cardinality? What are "canonical injections"?
David Egolf (Nov 03 2022 at 23:24):I'm not totally clear on what that author was saying, but you might find it helpful to write out the powerset of a small set (say ) and then see if any injection from to its powerset stands out as "canonical" to you.
Notification Bot (Nov 07 2022 at 20:24):A message was moved here from #learning: questions > Beginner questions by Peiyuan Zhu.