nLab setoid object




In a finitely complete category CC, a setoid object is an object XX with an internal pseudo-equivalence relation on XX. This means that it consists of a an object XX, an object RR, and morphisms p 1:RXp_1:R \to X and p 2:RXp_2:R \to X, equipped with the following morphisms:

  • internal reflexivity: r:XRr \colon X \to R which is a section both of p 1p_1 and of p 2p_2, i.e., p 1r=p 2r=1 Xp_1 r = p_2 r = 1_X;

  • internal symmetry: s:RRs \colon R \to R which interchanges p 1p_1 and p 2p_2, i.e., p 1s=p 2p_1\circ s = p_2 and p 2s=p 1p_2\circ s = p_1;

  • internal transitivity: t:R× XRRt: R \times_X R \to R which factors the left/right projection map R× XRX×XR \times_X R \to X \times X through RR, i.e., the following diagram commutes

    R t R× XR (p 1q 1,p 2q 2) X×X\array{ && R \\ & {}^{\mathllap{t}}\nearrow & \downarrow \\ R \times_X R & \stackrel{(p_1 q_1,p_2 q_2)}\rightarrow & X \times X }

    where q 1q_1 and q 2q_2 are the projections defined by the pullback diagram

    R× XR q 2 R q 1 p 1 R p 2 X\array{ R \times_X R & \stackrel{q_2}\rightarrow & R \\ \downarrow^{\mathrlap{q_1}} && \downarrow^{\mathrlap{p_1}} \\ R & \stackrel{p_2}\rightarrow & X }

See also

Created on September 22, 2022 at 12:08:22. See the history of this page for a list of all contributions to it.