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.
Patrick Nicodemus (Jan 29 2023 at 20:17):There are lots of papers on formalizing category theory in ZFC or NBG set theory, or ZFC+ some number of universes.
There are also lots of papers on formalizing category theory in Coq, Lean or other dependent type theories.
I am interested in what has been done theoretically regarding the possibility of carrying out the development of category theory in HOL, perhaps + extra axioms. HOL is a weaker logic than the calculus of constructions and dependent types are very natural for encoding category theory, so this is arguably an uphill battle, but I think the question is still interesting because automation in HOL leads automation in dependent type theory by a considerable margin at the moment. Reasoning in category theory is often very simple (equational reasoning is often all that is necessary for proving a diagram commutes) and so one would like to be able to take advantage of automation.
Patrick Nicodemus (Jan 29 2023 at 20:18):There are papers in the Isabelle/HOL archive of formal proofs. i have been reading the papers by Eugene Stark. it is very interesting but honestly his conception of a "category of sets" is utterly foreign to me, I am very taken aback. I am wondering if there has been much other theoretical work on this topic
Ryan Wisnesky (Jan 30 2023 at 02:35):Which paper has the unexpected definition of the category of sets? The "Types" mailing list is probably a good place to ask this question. https://lists.seas.upenn.edu/mailman/listinfo/types-list
Max New (Jan 30 2023 at 22:19):Maybe not exactly what you are asking for, but this describes a development of some category theory in Isabelle/HOL: https://link.springer.com/chapter/10.1007/3-540-44755-5_11
John Baez (Jan 30 2023 at 23:39):Now I'm curious about what an utterly foreign concept of "a category of sets" could look like!
Patrick Nicodemus (Jan 31 2023 at 01:14):https://www.isa-afp.org/browser_info/current/AFP/Category3/outline.pdf
Chapters 9 and 10
For any category S, the set of all terminal objects in S are thought of as "elements", I do not know if these behave like urelements or if they can have nontrivial internal structure.
Fix a distinguished terminal object 1.
Then we define, for each object X, a map from Hom(1, X) into the set of terminal objects of S, which sends each map a : 1 -> X to the "element" that it picks out. The idea is for a nice enough "category of sets" S, every object can be uniquely recovered from its underlying "set of elements" - the set of terminal objects under this correspondence
Jason Erbele (Jan 31 2023 at 05:38):That's a pretty nifty definition of a category of sets. Using Hom(1, X) in Set to pick out the elements of X is not unusual, so it looks promising just at a glance. Would it be too much to expect that if T is a terminal object in S, the map from Hom(1, T) to the terminal objects of S would pick out T? I don't suppose this is necessary, but it probably could be done for convenience. Ah. Looks like this is addressed on pp. 62–63 on the pdf you linked, with roughly the conclusion I expected:
The locale assumption stable-img forces t ∈ set t in case t is a terminal object. This is very convenient, as it results in the characterization of terminal objects as identities t for which set t = {t}. However, it is not absolutely necessary to have this.
My first thought on how to make this definition appear more foreign (besides turning it into computer code, but given what stream this conversation is in, maybe that's me) is to take S to be a category with a unique terminal object (not just unique up to isomorphism), like . Glossing along as best I can on the linked pdf, it seems like that would be the context for a set theory where there is only one element and thus only one non-empty set. This situation also gets a mention (on p. 75) in the pdf as "the case of a degenerate universe with only a single element."
The pdf at least indirectly mentions another "perverse" sort of situation that can happen that I didn't think of:
We call a set category replete if there is an object corresponding to every subset of the universe.
So a set category that is not replete would have sets that don't have objects of S to represent them.
Patrick Nicodemus (Feb 01 2023 at 02:09):Jason Erbele said:
We call a set category replete if there is an object corresponding to every subset of the universe.
So a set category that is not replete would have sets that don't have objects of S to represent them.
For my intuition, this seems to be the less perverse case, if we think of the collection of all terminal objects as forming the elements of which all sets are composed, then it seems reasonable that many collections may be "proper classes", i.e. not small sets. If the objects represent small sets then I would think not all collections can be represented as objects.
So for a replete category presumably it does not have an internal notion of powerset /power-object in general, else what would represent the power-object of the object containing all terminal objects?
Of course not all constructions of set theory are necessary to do basic elementwise reasoning, so this is fine.
Patrick Nicodemus (Feb 01 2023 at 02:15):He constructs these categories of sets in an ad-hoc local way, corresponding to the problem that needs to be solved. So given two categories C and D and functors F : C -> D and G : D-> C he constructs a category of sets in some sense generated by |C| \coprod |D| so that he can formulate what it means for F and G to be adjoint. I have not read this portion yet so I don't know how he does this freely generating a category of sets from a given set.
Patrick Nicodemus (Feb 01 2023 at 02:19):When I said it was foreign I mostly meant the extensionality principle of interpreting one object as directly representing a collection of other objects, it's not a categorical definition imo. Also fine but feels strange.