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 (Jan 05 2022 at 20:59):Hello
Peiyuan Zhu (Jan 05 2022 at 21:00):Is this group the only community that can discuss this topic? I was wondering if there's a more HoTT related group, because category theory seems to be the focus of this group
Dylan Braithwaite (Jan 05 2022 at 21:03):There's a HoTT Zulip as well: http://hott.zulipchat.com
Peiyuan Zhu (Jan 05 2022 at 21:15):Thanks so much
Peiyuan Zhu (Jan 10 2022 at 23:59):Reading the chapter Modalities as Monads (P109): “One key finding, however, is that it is not this variation as such that matters, but rather the properties possessed by adjoint operators arising from such variation.”
Peiyuan Zhu (Jan 11 2022 at 00:04):"When symbolized as entailments, p ⊢ ♢p and ♢♢p ⊢ ♢p, a category theorist will immediately be put in mind of a key construction known as a monad. A similar analysis of necessity
indicates the dual concept, a comonad."
Peiyuan Zhu (Jan 11 2022 at 02:39):"Indeed, there is no reason that being a certain kind of dog should correspond to being owned by a certain kind of person."
Peiyuan Zhu (Jan 11 2022 at 02:39):
Peiyuan Zhu (Jan 11 2022 at 02:43):How are properties represented in HoTT? Are they types? What does a 'transportation' of property mean? It seems like at a deeper level this paragraph is saying algebraic ontology doesn't work naturally, but still one desires to construct an algebraic correspondence between the two properties.
Peiyuan Zhu (Jan 11 2022 at 02:59):I looked at the HoTT book, transportation on a type family whose judgemental equality is defined. The proof starts by defining a product type that maps to universal type, which produces the function d inductively as the transport function. How to read ? It seems like what it is doing is to inductively define an identity that maps between properties, am I correct?
image.png
image.png
image.png
Peiyuan Zhu (Jan 11 2022 at 03:34):Not sure about a lot of things on this page. What does "*" mean? And how does it compose with the quantifiers over worlds? What does quotient mean? (I understand it as a poset)
image.png
Peiyuan Zhu (Jan 11 2022 at 03:42):I think above are all motivations of Modal HoTT
Peiyuan Zhu (Jan 11 2022 at 04:12):A blog post that explains Modal Type, going to give it another stab later on: https://medium.com/@bblfish/modal-hott-on-the-web-2f4f7996b41f