BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Liberating synthetic quasi-coherence from syntax - David Jaz Myers
  (Topos Institute)
DTSTART:20251107T140000Z
DTEND:20251107T150000Z
UID:TALK240262@talks.cam.ac.uk
CONTACT:Ioannis Markakis
DESCRIPTION:In usual foundations like ZFC\, we perform all of our mathemat
 ical constructions out of bare sets. The axiom of choice ensures these set
 s are "extremally disconnected" --- Cantor dust. We make the mathematical 
 objects built out of this dust to hang together with various binders and g
 lue\, but we must then constantly check that all further constructions res
 pect this gunk. Worse\, the underlying dustiness of bare sets leads to end
 less monster-barring in an attempt to preserve the intuitive dualities rel
 ating spaces and the algebras of intensive (functional) and extensive (dis
 tributional) quantities varying over them.\n\nIn synthetic mathematics\, w
 e instead work in the internal logic of a topos\, baking in the variation 
 of our notions with respect to an appropriately chosen class of test objec
 ts. The theory of these test objects is positive (roughly\, inductive). Bu
 t when the test objects are internalized as the universal model of their t
 heory\, they pick up beautiful negative properties which characterize thei
 r fundamental dualities.\n\nIn this talk\, I’ll conjecturally reformulat
 e Ingo Blechschmidt’s “synthetic quasi-coherence” axiom — or more 
 precisely his “general nullstellensatz” which identifies these extra n
 egative properties — as a lifting property inspired by Ivan Di Liberti
 ’s work on coherent toposes and ultrastructures. This lifting property s
 hows that synthetic quasi-coherence can be derived from a sort of “direc
 ted path induction” for toposes\, suggesting the possibility of an inter
 nal logic for all toposes in which the axioms for any sort of synthetic ma
 thematics would compute. (Based on joint work with Mitchell Riley)
LOCATION:SS03\, Computer Laboratory
END:VEVENT
END:VCALENDAR