Actually, let us define an operation, called bracket, that takes a relation \\(R\\), and two elements in a set, and gives \\(\mathrm{true}\\) when \\(R\\) holds for the elements \\(x\\) and \\(x'\\) and \\(\mathrm{false}\\) otherwise,

\\[

[x R x'] =\begin{cases}\mathrm{true} & \mathrm{if} \ x R x' \\\ \mathrm{false} & \mathrm{otherwise} \end{cases}

\\]

then,

\\[

\cap_X(x,x') := [x \leq x'].

\\]

Interesting fact about brackets is that when we identify \\(\mathbf{Bool}\\) with \\((\varnothing \subseteq \mathbf{1})\\), with \\(\mathbf{false} \cong \varnothing\\) and \\(\mathbf{true} \cong \mathbf{1}\\) then taking the cartesion product with them allows us to have an object appear only when our relation holds (up to isomorphism),

\\[

[x R x'] \times A \\\\

\implies A \text{ when } [x R x'] = \mathrm{true} \\\\

\implies \varnothing\text{ when } [x R x'] = \mathrm{false}

\\]

since the cartesion product of any \\(A\\) with \\(\varnothing\\) is isomorphic to \\(\varnothing\\), and the cartesion product of any \\(A\\) with \\(\mathbf{1}\\) is isomorphic to \\(A\\).

In fact, thinking about it,

\\[

(\cup\_{x,x} \times id_{x'}) \circ (id_x \times \cap_{x,x')} ) \\\\

= ([x \geq x]\times id_{x'}) \circ (id_x \times [x \leq x'] ) \\\\

= ([x = x]\times id_x') \circ (id_x \times [x \leq x'] )

\\]

is equivalent to an upper-set, if we are allowed to vary \\(x'\\). Which is sort of what I wanted to show above.

\\[

[x R x'] =\begin{cases}\mathrm{true} & \mathrm{if} \ x R x' \\\ \mathrm{false} & \mathrm{otherwise} \end{cases}

\\]

then,

\\[

\cap_X(x,x') := [x \leq x'].

\\]

Interesting fact about brackets is that when we identify \\(\mathbf{Bool}\\) with \\((\varnothing \subseteq \mathbf{1})\\), with \\(\mathbf{false} \cong \varnothing\\) and \\(\mathbf{true} \cong \mathbf{1}\\) then taking the cartesion product with them allows us to have an object appear only when our relation holds (up to isomorphism),

\\[

[x R x'] \times A \\\\

\implies A \text{ when } [x R x'] = \mathrm{true} \\\\

\implies \varnothing\text{ when } [x R x'] = \mathrm{false}

\\]

since the cartesion product of any \\(A\\) with \\(\varnothing\\) is isomorphic to \\(\varnothing\\), and the cartesion product of any \\(A\\) with \\(\mathbf{1}\\) is isomorphic to \\(A\\).

In fact, thinking about it,

\\[

(\cup\_{x,x} \times id_{x'}) \circ (id_x \times \cap_{x,x')} ) \\\\

= ([x \geq x]\times id_{x'}) \circ (id_x \times [x \leq x'] ) \\\\

= ([x = x]\times id_x') \circ (id_x \times [x \leq x'] )

\\]

is equivalent to an upper-set, if we are allowed to vary \\(x'\\). Which is sort of what I wanted to show above.