Rel, bicategory of relations, allegory
left and right euclidean;
extensional, well-founded relations.
In a finitely complete category , a setoid object is an object with an internal pseudo-equivalence relation on . This means that it consists of a an object , an object , and morphisms and , equipped with the following morphisms:
internal reflexivity: which is a section both of and of , i.e., ;
internal symmetry: which interchanges and , i.e., and ;
internal transitivity: which factors the left/right projection map through , i.e., the following diagram commutes
where and are the projections defined by the pullback diagram
Created on September 22, 2022 at 16:08:22. See the history of this page for a list of all contributions to it.