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.
Xuanrui Qi (May 24 2021 at 16:26):Does anyone know of examples of using CT techniques, particularly categorical semantics and topos theoretic techniques, to prove equiconsistency of two theories? I'm thinking of something along the lines of _Sheaves in Geometry and Logic_, VI 10, where Mac Lane and Moerdijk prove the equivalence of topos-theoretic and set-theoretic foundations. But I wonder if anyone has used this approach to prove equiconsistency results between (some flavor of) type theory and (some flavor of) set theory.
Reid Barton (May 24 2021 at 16:44):Not sure if this is exactly what you're looking for, but I found this blog post by Mike Shulman on proving metatheoretic properties of type theories (including consistency relative to set theory) using Artin gluing quite helpful.
Xuanrui Qi (May 24 2021 at 16:47):Thanks! This one looks interesting