Context: I'm trying to figure out how much theory one can carry over from sets to setoids. A setoid $A$ here consisting of a "carrier" set $S_A$ and an equivalence relation $\sim_A$ on $S_A$.
For example, a setoid "function" from $A$ to $B$ is simply a function $f: S_A \to S_B$ such that $x \sim_A y \implies f(x) \sim_B f(y)$. This makes for a nice category.
We can say that $A$ is a setoid "subset" ("subsetoid"?) of $B$ iff $S_A \subset S_B$ and $x \sim_A y \implies x \sim_B y$. This makes for a nice partial order (thin category), with a functor to the aforementioned nice category.
Question: Are there sensible corresponding concepts of "intersection" and "union" for setoids? I would expect these to form a distributive lattice along with the subset relation.
Defining a $\cup$ and $\cap$ follows from the basic theory of partitions. Informally, the intersection of setoids is the intersection of the ground sets, equipped with the meet of the relations on the intersecting set. The union of setoids is the union of the ground sets, equipped with the join of the relations on the intersecting part of the union, and the respective relations on the symmetric difference.
Writing a setoid as $(S_A,\sim_A)$, then we can define for $(S_A,\sim_A)$ and $(S_B,\sim_B)$ the setoid meet: $(S_A,\sim_A) \cap (S_B,\sim_B) = (S_{A \cap B}, \sim_{A \cap B})$, where $S_{A \cap B} = S_A \cap S_B$ and:
$$\sim_{A \cap B} = \left(\sim_A|_{A \cap B}\right) \wedge \left(\sim_B|_{A \cap B}\right)$$
where $R|_S$ is the relation $R$ restricted to $S$, and $\wedge$ is the meet of equivalence relations, given by the lattice of partitions of a fixed set.
We can also define the setoid join: $(S_A,\sim_A) \cup (S_B, \sim_B) = (S_{A \cup B}, \sim_{A \cup B})$, where $S_{A \cup B} = S_A \cup S_B$, and:
$$\sim_{A \cup B} = \begin{cases} \sim_A &\text{ on } A \setminus B\\ \sim_B &\text{ on } B \setminus A\\ \left(\sim_A|_{A \cap B}\right) \vee \left(\sim_B|_{A \cap B}\right) &\text{ on } A \cap B\end{cases}$$
where $\vee$ is the join of equivalence relations, given by the lattice of partitions of a fixed set.