Category Theory
Zulip Server
Archive

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.

Stream: theory: category theory

Topic: Regular Hyperdoctrines and Regular Categories

Max New (Jun 17 2023 at 16:42):

I just read Carsten Butz's nice article Regular Categories and Regular Logic and I noticed that the construction of the classifying regular category for a regular category had a very syntactic character.

Basically, he took the syntax of regular logic, which is the free [[regular hyperdoctrine]] and he performed a kind of syntactic completion where he constructed a new logic where the objects were essentially pairs of a list of objects and a proposition over them, and the morphisms were the total functional relations in the regular hyperdoctrine.

The fact that this works suggests to me the following conjecture and I wonder if it's known to be true.

Conjecture: A regular hyperdoctrine is the hyperdoctrine of subobjects of a regular category if and only if:

1. Its objects are closed under "subobject comprehension", i.e., for every object $A$ and predicate $\phi \in L(A)$ there is an object $\{ A | \phi \}$ with universal property $\Gamma \to \{ A | \phi \} \cong \{ f : \Gamma \to A | \top \leq f^*\phi\}$. In the syntax this looks like a "subset type" or "refinement type" in PL terminology.
2. It satisfies the principle of unique choice. I.e., in the internal language from any total functional relation $R$ you can construct a function $f$ whose graph is $R$.

Ivan Di Liberti (Jun 17 2023 at 16:49):

See the discussion at the beginning of page 33 here: https://arxiv.org/abs/2304.07539.

Max New (Jun 17 2023 at 18:30):

Right so this says that the regular categories for a reflective sub 2-category of the regular hyperdoctrines, where the reflection is given by the construction I mentioned. I'm proposing an alternative, explicit characterization of that sub 2-category as regular hyperdoctrines that have some essentially unique structure