The subobject classifier in the topos Sets^(->)

In order to demonstrate operations in on objects of the elementary copresheaf topos $Sets^{\to}$ we should first create a function object. This can be done as of Locus 1.2 using the mapfn function, which converts a clojure.lang.IPersistentMap into a SetFunction. You can also perform the same conversion using the standard to-function method.

(def f
  (mapfn 
    {:a :x, 
     :b :x, 
     :d :y, 
     :e :y, 
     :f :z}))

Once you have defined a function, you can display it using the visualize routine which will give you a diagram like this, demonstrating a surjective function. When we define a subobject classifier in a topos, we also need an object of truth values. The object of truth values in the topos of functions $Sets^{\to}$ is a function that looks like this. The subobject classifier in the topos $Sets^{\to}$ is then a morphism in $Sets^{\to}$, but that means it is also an object in the topos $Sets^{T_2 \times T_2}$ and a presheaf object of a topos in its own right. We get a subfunction from the pair (#{:a :d}, #{:x :y}). The resulting subobject classifier in the topos $Sets^{T_2 \times T_2}$ looks like this: I recently mentioned that $Sets^{\to}$ is a concrete category. This is a new development that I only implemented in Locus 1.2, when I decided that everything should be made into a concrete category in order to implement structure copresheaves and to expose as many morphisms as possible to reasoning in the topos $Sets^{\to}$. This means that the subobject classifier in $Sets^{\to}$ itself has an underlying function that looks like this: This demonstrates that the subobject classifier in $Sets^{\to}$ is like a function on the elements of functions. The elements of functions are inputs labeled by zero and outputs labeled by one, and the maps between them map inputs to inputs and outputs to outputs. We map inputs to $0$, $\frac{1}{2}$ and $1$ depending upon rather they are in the set, their image is in the set, or if their image isn't even in the set at all. So this gives a different notion of truth then we are used to in $Sets$.

When we think of a function $f: A \to B$ we don't typically think of it as a structured set, in fact I am not familiar with any text that describes them as such nor anything that describes $Sets^{\to}$ as a concrete category. This requires a fundamental rethinking of one of the most basic objects of mathematics: functions. We must now consider functions to be like structured sets again.

The beauty of this construction is that when can then take morphisms in $Sets^{\to}$ and consider them to be objects in $Sets^{\to}$ again so we can use the categorical logic of $Sets^{\to}$ on them. In particular, we see that the underlying function of the diamond copresheaf demonstrated above has a function congruence which maps the first part of the input to the first part of the output, demonstrating that morphisms of functions preserve input/output types.

The justification of representing everything as a structured set and every category as a concrete category, is actually primarily so that every morphism can be structured function. This way we can always reason about any morphism in a concrete category using the fundamental topos $Sets^{\to}$ which is our most deepest goal. This requires that we rethink our understanding of presheaves, so that we can consider the different layers of presheaf representations that mathematical objects can be exposed to.

References:
Topoi: The Categorial Analysis of Logic by Robert Goldblatt