Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 3 of 3
Is there a formalization of SEAR anywhere, like for example as a Coq/Agda/Lean library or the like?
In 2019 some Joshua Chen wrote on FOM (here):
I’ve started a formalization of Mike Shulman’s SEAR in Isabelle on top of triply-sorted first-order logic, and will be experimenting to see how much mathematics I can formalize in this.
SEAR is written in dependently typed first-order logic, whether or not you include replacement. The dependent types have nothing to do with families of sets, which are expressed in SEAR using relations or bundles just as they are in ETCS, but only with the fact that the type of elements of a set and the type of relations between two sets are dependent on the type of sets. Properties are just first-order formulas.
Replacement/collection is irrelevant for internal completeness of the lattice of relations, which is always provable just as it is in any elementary topos. (Some helpful recent discussion of replacement, and what it means and doesn’t mean, is at Tom’s recent cafe post and the ensuing discussion in the comments.)
I don’t know of any completed formalization of SEAR.
1 to 3 of 3