Post #1905751

2026-04-24 07:12 UTC

@jonmsterling @maxsnew The intuition for a general set is a set whose elements are finitely constructable. Finite limits and initial algebra constructions preserve this property. The tricky thing with topos theory is that it depends on an underlying set theory to index infinite colimits, which is why Vickers shifted from topoi to arithmetic universes while developing this perspective.

Replies (1)

@olynch@mathstodon.xyz 2026-04-24 07:24

@jonmsterling @maxsnew The interesting things about topos theory is that all sheaves are open (can be built out of finite limits and infinite colimits starting from the base), *including* the ones built from negative type formers like function types, etc. However the fact that a certain negative construction and a certain positive construction happen to be isomorphic in a given topos is not preserved by geometric morphisms. It's kind of like how in a fixed programming language, if you have quotient inductive inductive types you can internalize the syntax of that language and then write a type of function abstract syntax trees with equality given by proofs of equality. This is isomorphic to the function type. However, as soon as you add a new primitive operation to your language, the function type automatically picks this operation up, while your carefully encoded abstract syntax trees know nothing about it. And this is why it makes sense to serialize certain data types across languages (inductive types) but you can only serialize closures if you are going to deserialize them into precisely the same language and program that you originally serialized them from. I'm focusing just on the positive fragment of type theory, which is preserved by geometric morphisms, but David Jaz and Mitchell Riley are working on negative constructions which are "stuck" in a certain topos and are not preserved by general substitutions (which are geometric morphisms), figuring out how to handle these stuck constructions is one of the key challenges!

Open ##1905752