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.
dusko (Mar 28 2023 at 01:51):Morgan Rogers (he/him) said:
dusko Mike explicitly says what the monad does, what are you asking for exactly?
well, the monad which maps sets to their image on the terminal object is indeed idempotent. calling it (-1)-truncation is an excellent idea when we want to confuse the enemy.
if is the base topos generated by 1, as it tends to be, then the (-1)-truncation monad has the number 2 as the category of algebras. how do we model irrelevant types in the number 2?
even for a general topos, the category of algebras of the (-1)-truncation monad is a lattice. still a bit degenerate for a type theory.
i am sure i am missing something and i am not sure that it is worth anyone's effort to enlighten me. but i don't want to pretend that i understand when i don't.
John Baez (Mar 28 2023 at 02:18):I can't tell what if anything you're missing, Dusko, so I'll just throw this out there: do you know about (-1)- groupoids? Sets are 0-groupoids, groupoids are 1- groupoids, and we can go on up from there, but James Dolan noticed that truth values are (-1)-groupoids.
John Baez (Mar 28 2023 at 02:19):Given an n-groupoid and m < n we can m-truncate it and get an m-groupoid.
John Baez (Mar 28 2023 at 02:21):(-1)-truncation is a special case of this: if we (-1)-truncate it we get a truth value saying whether it's occupied.
John Baez (Mar 28 2023 at 02:23):I'm phrasing this all very "classically", in terms of set theory, but these days the cool kids would say it all using homotopy type theory, and talk about m-truncating a type.
dusko (Mar 28 2023 at 03:54):that is obviously a very nice observation. i think makkai also thought of propositions as the level -1...
but capturing observations by introducing new terminology is a questionable communication strategy. if i start calling a cow a horn-horse only because i started using it to pull a cart, the neighbors will let me talk to myself. the truth values have been called propositions for a 1000 years solid, and with modifications for another 1000. it is nice to start a taxonomy from them. but if we tell someone: "hey, category theorists call propositions (-1)-groupoids" --- they will let us talk to ourselves.
or a student joins zulip and wants to learn category theory. exercises: prove that in a cartesian category an object is a subobject of is and only if the diagonal (or a projection) on is an isomorphism. prove that the fixpoints of a functor mapping every to the image of form a sublattice such that every subobject is in the form for some . most students will come back with at least a reasonable workout.
now let us call the subobjects of the (-1)-truncations. most of the students i know will get stuck, think that they are not smart enough for category theory, and go do something else.
dusko (Mar 28 2023 at 04:04):... and if the cool kids don't want to do the basic exercises with products but just to do homotopy type theory --- are they managing to compute some topological invariants that voevodsky would have hoped or to find invariants of some algorithms as the inabitants of the identity type, as martin-loef would have hoped? if they are not, then we have replaced mathematics with coolness. i totally honestly hope that my impression that they are not is based on me being in the corner and not paying attention.
Ryan Wisnesky (Mar 28 2023 at 04:40):sure, here's a paper on using univalence to compute fundamental groups of circles https://www.cs.cmu.edu/~drl/pubs/ls13pi1s1/ls13pi1s1.pdf
John Baez (Mar 28 2023 at 06:00):dusko said:
that is obviously a very nice observation. i think makkai also thought of propositions as the level -1...
That's interesting. He might have had this idea independently, but I think of James Dolan and Toby Bartels as introducing it and Mike Shulman and I as popularizing it in our paper Lectures n-Categories and Cohomology back in 2006. In the section "The power of negative thinking" we wrote:
After James Dolan and JB came up with the periodic table, JB showed it to Chris Isham, who does quantum gravity at Imperial College. I was incredibly happy with it, but he said: “That’s obviously not right — you didn’t start the chart at the right place. First there should be a column with just one interesting row, then a column with two, and then one with three.” I thought he was crazy, but it kept nagging me. It’s sort of weird to start counting at three, after all. But there are no (−1)-categories or (−2)-categories! Are there?
It turns out there are! Eventually Toby Bartels and James Dolan figured out what they are. And they realized that Isham was right.
John Baez (Mar 28 2023 at 06:02):@dusko wrote:
but capturing observations by introducing new terminology is a questionable communication strategy.
No wonder people don't like math. :upside_down:
dusko (Mar 28 2023 at 06:05):oh i don't think makkai would worry about the priority. this was in like 1994. he was walking around talking about the hierarchy of equalities. and equipping them with structures which he i think ended up calling anafunctors, because they came after profunctors and in cell division you have prophasis, anaphasis... it is no wonder that he would come with the same structure, since you are all talking about the same elephant of nature. but everyone is telling a different story.
John Baez (Mar 28 2023 at 06:06):Right.
John Baez (Mar 28 2023 at 06:07):the truth values have been called propositions for a 1000 years solid, and with modifications for another 1000. it is nice to start a taxonomy from them. but if we tell someone: "hey, category theorists call propositions (-1)-groupoids" --- they will let us talk to ourselves.
I actually don't think anyone runs around calling propositions (-1)-groupoids. What's happening is that homotopy type theorists - not category theorists per se - like to talk about truncation. Like on the Homotopy Type Theory blog there's an article Truncations and truncated higher inductive types by Guillaume Brunerie where he writes stuff like this:
Truncations are very useful in homotopy theory, and are also useful for foundations of mathematics, especially for n=-1,0:
The (-1)-truncation is also known as isinhab: given a type A it returns a proposition isinhab A which is true if and only if A is inhabited (by “proposition” and “set” I will always mean “h-proposition” and “h-set”). This has already been considered by Vladimir Voevodsky here, where isinhab A is defined using impredicative quantification and resizing rules, and this is also present in the Coq HoTT library here where isinhab is defined using higher inductive types.
The 0-truncation of a space is the set of its connected components. This allows us, among other things, to build initial algebras by generators and relations and to build quotients of sets by (prop valued) equivalence relations.
The aim of this post is to explain how to define n-truncations for every n using higher inductive types
dusko (Mar 28 2023 at 06:07):i hope someone would go on and prove makkai's stone duality for predicate logic. that is an extremely fundamental result, but written in his language, it was understood by like 4 people. i thought i understood it when he talked about it, but never managed to calculate an actual representation out of it. marek zawadovski i think did.
John Baez (Mar 28 2023 at 06:09):Hmm, I don't know about that.
dusko (Mar 28 2023 at 06:19):John Baez said:
the truth values have been called propositions for a 1000 years solid, and with modifications for another 1000. it is nice to start a taxonomy from them. but if we tell someone: "hey, category theorists call propositions (-1)-groupoids" --- they will let us talk to ourselves.
I actually don't think anyone runs around calling propositions (-1)-groupoids. What's happening is that homotopy type theorists - not category theorists per se - like to talk about truncation. Like on the Homotopy Type Theory blog there's an article Truncations and truncated higher inductive types by Guillaume Brunerie where he writes stuff like this:
Truncations are very useful in homotopy theory, and are also useful for foundations of mathematics, especially for n=-1,0:
The (-1)-truncation is also known as isinhab: given a type A it returns a proposition isinhab A which is true if and only if A is inhabited (by “proposition” and “set” I will always mean “h-proposition” and “h-set”). This has already been considered by Vladimir Voevodsky here, where isinhab A is defined using impredicative quantification and resizing rules, and this is also present in the Coq HoTT library here where isinhab is defined using higher inductive types.
The 0-truncation of a space is the set of its connected components. This allows us, among other things, to build initial algebras by generators and relations and to build quotients of sets by (prop valued) equivalence relations.
The aim of this post is to explain how to define n-truncations for every n using higher inductive types
thank you. i need to think about this.
i was thinking the other day what the kleinian program of understanding geometry that we cannot comprehend (and noether's version...) --- what all that will look like if we manage to teach GPTs to do actual math... they might be able to make us see what we are not normally wired to see (just like paper makes us able to multiply numbers that don't fit into our memory)...
Notification Bot (Mar 28 2023 at 13:06):22 messages were moved here from #theory: category theory > Constant dependent function by Matteo Capucci (he/him).
Matteo Capucci (he/him) (Mar 28 2023 at 13:07):(Sorry for the slicing but it felt the conversation went a bit OT)