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.