/sci/ - Science & Math

>>11289222
>But then can we proceed to do anything interesting here?
I haven't taken a closer look at you axiom IV yet, but before we go on, it might be worth pointing out that the crucial axiom of a Topos is, in fact, the universal characterization of characteristic functions (the other being sums, products, exponentiation):

If your theory has an object that behaves like the a singleton set (all arrows of type into it are the same)
and if your theory has a notion of injections/embeddings (j.f=j.g implies f=g)
then a notion of subobject, if it exist,
is given by a truth object Ω (and no, in general this doesn't have to be a two-element set, like {0, 1})
and, for each embeddings j:U->X from "smaller" objects U into "bigger" objects X,
a "characteristic function" chi such that only j makes

chi.j = take_True

The categories which have this thing are generalizations of logics, set theories and topologies.

https://en.wikipedia.org/wiki/Subobject_classifier
https://en.wikipedia.org/wiki/Topos#Elementary_topoi_(topoi_in_logic)