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.
Keith Elliott Peterson (Oct 22 2021 at 05:54):Are there structural set-theoretic 'halfway houses' that allow one to speak of sets of sets like one can in material set theories or are structural set theories always limited to a family of sets construction?
Mike Shulman (Oct 22 2021 at 13:06):Well, one could debate about the meaning of "structural set theory", but the way I generally use the term, no. I would say that in a structural set theory the elements of a set are always "intrinsically featureless" and only given meaning (to be regarded, for instance, as representatives of some other set) by external structure relating that set to some other set(s). However, in type theory one can have some of both worlds.
Mike Shulman (Oct 22 2021 at 13:06):(BTW, I also used to use "halfway house" to mean "point in the middle", but then I learned that actually it's something else.)
Martti Karvonen (Oct 22 2021 at 16:55):Mike Shulman said:
(BTW, I also used to use "halfway house" to mean "point in the middle", but then I learned that actually it's something else.)
(Looking at meaning 3, it seems to me that "point in the middle" is also an established meaning of the phrase)
Keith Elliott Peterson (Oct 24 2021 at 23:22):Y'all are looking too deeply into the metaphor.
Does MLTT come with its own form of diagrammatic reasoning, just as in ZF we have collections of dots/subcollections or the collections of dots with arrows between dots view of ETCS/SEAR?
Mike Shulman (Oct 25 2021 at 07:00):I'm not sure that I would call those diagrammatic reasoning. But whatever they are, one could imagine drawing pictures of types and their elements. An element of a function type is a function and can be drawn as arrows between dots or however you like, an element of a powertype is a subset and can be drawn with subcollections of dots, etc.
Keith Elliott Peterson (Oct 26 2021 at 07:19):Okay, good. I wrote a program that drew functions sets as literal sets of functions, with the functions drawn as their cographs. It is nice to see it was meaningful.