Strong extensionality of 'membership' relation defined on the set of all morphisms of a well-pointed topos

Question

We use the notion of category $C$ with one set of objects $\mathrm{Ob}(C)$ and one set of morphisms $\mathrm{Mor}(C)$, with source function $s:\mathrm{Mor}(C) \to \mathrm{Ob}(C)$ and target function $t:\mathrm{Mor}(C) \to \mathrm{Ob}(C)$.

Recall that a topos is a category $C$ with a terminal object $1$, finite pullbacks, and power objects. A global element in a topos is a morphism $x \in \mathrm{Mor}(C)$ such that the source $s(x) = 1$. A topos is well-pointed if for all sets $A$ and $B$ and parallel morphisms $f \in \mathrm{Mor}(C)$ and $g \in \mathrm{Mor}(C)$ such that $s(f) = s(g) = A$ and $t(f) = t(g) = B$, and for all global elements with target $t(x) = A$, $f \circ x = g \circ x$.

Well pointed topoi represent a categorical model of constructive set theory, where the global elements represent elements of sets. By the universal property of the terminal object, for every object $A$ there is a unique morphism $u_A \in \mathrm{Mor}(C)$ such that $s(u_A) = A$ and $t(u_A) = 1$, which means that the morphism $u_A$ could represent the actual sets.

This means that we could define a binary relation $\in_C$ on $\mathrm{Mor}(C)$ itself which behaves like a membership relation, where given a morphisms $a \in \mathrm{Mor}(C)$ and a morphism $b \in \mathrm{Mor}(C)$, we define

$$a \in_C b := (s(a) = 1) \wedge (t(b) = 1) \wedge (t(a) = s(b))$$

By the properties of the terminal object, the identity morphism $\mathrm{id}_1$ satisfies $\mathrm{id}_1 \in \mathrm{id}_1$, since $s(\mathrm{id}_1) = 1$, $t(\mathrm{id}_1) = 1$, and thus $s(\mathrm{id}_1) = t(\mathrm{id}_1)$. This implies that the relation $\in_C$ is not well-founded.

The condition of the topos being well-pointed means that the relation $\in_C$ is weakly extensional: for all morphisms $x \in \mathrm{Mor}(C)$ and $y \in \mathrm{Mor}(C)$, if for all morphisms $a \in \mathrm{Mor}(C)$, $a \in_C x$ if and only if $a \in_C y$, then $x = y$. However, since $\in_C$ is not well-founded, $\in_C$ being weakly extensional no longer implies that $\in_C$ is strongly extensional.

Recall that given a set $S$ and a binary relation $\prec$, that a bisimulation on $(S, \prec)$ is a binary relation $\sim$ such that for all $x \in S$ and $y \in S$ such that $x \sim y$, the following conditions hold:

• for all $a \in S$ such that $a \prec x$, there exists a $b \in S$ such that $b \prec y$ and $a \sim b$
• for all $b \in S$ such that $b \prec y$, there exists a $a \in S$ such that $a \prec x$ and $a \sim b$

$\prec$ is strongly extensional if every bisimulation is contained in the equality relation on $S$: for all bisimulations $\sim$ and for all elements $x \in S$ and $y \in S$, $a \sim b$ implies that $x = y$.

Is the defined membership relation $\in_C$ a strongly extensional relation on $\mathrm{Mor}(C)$?

Answer 1

By definition of your relation $\in_C$, only for the morphisms into the terminal object $b:A \to 1$ are there morphisms $a:1 \to A$ such that $a \in_C b$, and $a$ by definition has to be a global element. This means that all other morphisms $c:A \to B$ and $d:A \to B$ whose codomains are not the terminal object trivially satisfy the bisimulation condition that for all $e:C \to D$ such that $e \in_C c$ there exists an $f:E \to F$ such that $f \in_C d$ and $e \sim f$ and for all $f:E \to F$ such that $f \in_C d$ there exists an $e:C \to D$ such that $e \in_C c$ and $e \sim f$, as there are no morphisms $e:C \to D$ or $f:E \to F$ such that $e \in_C c$ or $f \in_C d$.

So take the bisimulation $a \sim b$ defined by equality on every hom-set except for the hom-set $(1 \coprod 1) \to (1 \coprod 1)$ on the coproduct of the terminal object, where for all morphisms $a:(1 \coprod 1) \to (1 \coprod 1)$ and $b:(1 \coprod 1) \to (1 \coprod 1)$, $a \sim b$. This is a bisimulation on the set of all morphisms $\mathrm{Mor}(C)$, but it isn't true that $a \sim b$ implies that $a = b$ for all morphisms $a \in \mathrm{Mor}(C)$ and $b \in \mathrm{Mor}(C)$. Thus, $\in_C$ is not strongly extensional.