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.
Patrick Nicodemus (Mar 01 2024 at 14:31):Topos theory admits a semantics for a formal logic commonly referred to as "intuitionistic higher-order logic". For a formal presentation one can take, for example, Bell's "local set theory", or the mitchell-benabou so-called "internal language" of the topos.
I am not aware of any formal treatments of the internal language of topos theory where one explicitly speaks of type _variables_ rather than type constants, and allows one to quantify over types to define functors. Do such treatments exist?
I would speculate that the Hindley-Milner predicative polymorphism type system would admit an interpretation where polymorphic types are associated to endofunctors on the topos.
James Deikun (Mar 01 2024 at 16:36):The [[stack semantics]] of a topos is all about quantifying over types.