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 (Dec 06 2021 at 02:49):Ross Street has commented that his work on "cosmoi" has a logical aspect to it. The notation is meant to evoke set theory; he writes PA for the category of presheaves on A (P also stands for powerset) and suggests that the Yoneda embedding is like the singleton embedding A -> PA. The axioms he takes, he says, are inspired by categorifying the substitution properties of equality. However, this is all he says about logic. The rest of his papers on this appear to be pure category theory.
I think this idea is very interesting. In particular Kan extensions of V-valued functors would play the role of quantification. Thus a left Kan extension of a presheaf P along a functor F is an "image" of P along F. An element of lim P is a proof that "for all c, P(c)".
What has been made of this from a logical point of view? Have any type theorists written down a formal theory which can be interpreted in cosmoi? I tried to work it out but it seems subtle. The pun with equality is difficult to formalize because this "equality" is not symmetric in general unless the category is a groupoid. It is maybe more like a reducibility relation than an equivalence relation.
Fawzi Hreiki (Dec 06 2021 at 12:56):Maybe take a look at Lawvere’s first paper on hyperdoctrines where he uses the example of the category of small categories, with the ‘power object’ given by the presheaf category.
Fawzi Hreiki (Dec 06 2021 at 12:57):If you want more advanced stuff, then you can take a look at Mark Weber’s paper on Yoneda structures and 2-toposes, or at Mike Shulman’s nLab page on 2-logic https://ncatlab.org/michaelshulman/show/2-categorical+logic
Fawzi Hreiki (Dec 06 2021 at 13:00):This blog post on the n-cat cafe is a pretty good introduction.
Kenji Maillard (Dec 06 2021 at 13:49):Paul-André Melliès and Noam Zeilberger further developped some of these ideas from Lawvere in An Isbell Duality Theorem for Type Refinement Systems
Mike Shulman (Dec 06 2021 at 20:52):In general, this sort of "directed type theory" is quite subtle. In addition to my unfinished work on the nlab, there's work by Harper and Licata, Nuyts, and North, but I don't think any of it has a general categorical semantics in something like cosmoi yet.