alternative take: everything is just sets
both can be a foundation for mathematics, and hence, a foundation for everything
what's interesting is how each choice affects what logic even means?
both can be a foundation for mathematics, and hence, a foundation for everything
what's interesting is how each choice affects what logic even means?
How could we go the other way? A set can be "defined" by the predicate that tests membership, but then how do we model the predicates? Some formalism like the lambda calculus?
A category can be defined in terms of its morphisms without mentioning objects and a topos has predicates as morphisms into the subobject classifier.
lambda calculus would provide a computational way to determine the truth value of the predicate, any computable predicate that is.