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: type theory & logic

Topic: Sheafification expressed in the internal language of the top

Andrej Bauer (May 16 2025 at 13:29):

I am looking for an account of how sheafification with respect to a Lawvere-Tierney topology j : Ω → Ω is expressed in the internal language of a topos. In other words, how does one express the ++-construction. My best guess is that A++ = { u : A → Ω | j (singleton u) } where singleton u := (∀ x y, u x ∧ u y ⇒ x = y) ∧ (∃ x . u x), but I'd prefer a written account to having it figure out myself.

Andrej Bauer (May 17 2025 at 17:35):

In case anyone cares, my suggestion is of course too naive. One has to throw in a quotient, or just mimic the +-construction. I am in the process of formalizing this, will post a gist when done.

Jonas Frey (May 18 2025 at 14:46):

Johnstone gives a construction in in terms of elementary toposes in A4.4.4 of the elephant, and I think it translates to
$A++ = \{p : A \to \Omega_j | j(\exists a \in A . p = \{b \in A | j(a=b)\})\}$
in the internal language.

Nicola Gambino (May 19 2025 at 09:02):

A reference is Barbara Veit, "A Proof of the Associated Sheaf Theorem by Means of Categorical Logic", JSL Vol. 46, No. 1 (Mar., 1981), pp. 45-55.

Andrej Bauer (May 23 2025 at 16:14):

Here is the promised Coq formalization of sheafification in logical form. I followed Barbara Veit's paper cited by @Nicola Gambino. A couple of things still remain:

• sheafification is a reflection
• sheafification preserves finite limits

If anyone has the energy to do these two, please let me know so that I can update the gist.