Contents

Idea

Apseudo-equivalence relation is like anequivalence relation, but where we allow more than one element in the relation; i.e. the underlyingdirected graph of the relation is adirected pseudograph. In the same way thatmagmoids are the raw structure used to buildsemicategories andcategories, sets with pseudo-equivalence relations are the raw structure used to builddagger categories andgroupoids (i.e. a groupoid without associativity, unital laws, and inverse laws).

Sets equipped with pseudo-equivalence relations are sometimes calledsetoids (i.e. inWilander (2012), §4;Palmgren & Wilander (2014), §2, §6;Emmenegger & Palmgren (2020), §6;Cipriano (2020), Def. 1.1.1), but the term “setoid” is also used in mathematics to refer only to the sets withequivalence relations. In this article, the term “setoid” is used in the former sense of “sets equipped with pseudo-equivalence relations”.

Definition

With a family of sets

Using graph theoretic terminology, apseudo-equivalence relation on a set$V$ ofvertices is a family of sets$E(a,b)$ ofedges for each vertex$a\in V$ and$b\in V$, which comes with the following additional structure

• for each vertex$a\in V$ an element

  $$\mathrm{refl}(a)\in E(a,a)$$

• for each vertex$a\in V$ and$b\in V$ a family of functions

  $$\mathrm{sym}(a,b):E(a,b)\to E(b,a)$$

• for each vertex$a\in V$,$b\in V$, and$cinV$, a family of functions

  $$\mathrm{trans}(a,b,c):(E(a,b)\times E(b,c))\to E(a,c)$$

With a set

Apseuodo-equivalence relation on aset$V$ is a set$E$ and functions$s:E\to V$,$t:E\to V$ (a loopdirected pseudograph), with with functions$\mathrm{refl}:V\to E$,$\mathrm{sym}:E\to E$, and

such that

• for every$a\in V$,$s(\mathrm{refl}(a)){=}_{E}a$
• for every$a\in V$,$t(\mathrm{refl}(a)){=}_{E}a$
• for every$f\in E$,$s(f){=}_{V}t(\mathrm{sym}(f))$
• for every$f\in E$,$t(f){=}_{V}s(\mathrm{sym}(f))$
• for every$f\in E$ and$g\in E$ such that$t(f){=}_{V}s(g)$,$s(\mathrm{trans}(f,g)){=}_{E}s(f)$
• for every$f\in E$ and$g\in E$ such that$t(f){=}_{V}s(g)$,$t(\mathrm{trans}(f,g)){=}_{E}t(g)$

Extensional functions, dagger functors, and isomorphisms

We define anextensional function$f:A\to B$ between two sets$A$ and$B$ with pseudo-equivalence relations$(E_A,{\mathrm{refl}}_A,{\mathrm{sym}}_A,{\mathrm{trans}}_A)$ and$(E_B,{\mathrm{refl}}_B,{\mathrm{sym}}_B,{\mathrm{trans}}_B)$ to be a function$f_V:A\to B$ and a family of functions$f_E(a,b):E_A(a,b)\to E_B(f_V(a),f_V(b))$

Composition of extensional functions is defined as composition of the vertex function and of each edge function.

An extensional function between two sets with pseudo-equivalence relations isfull if every edge function$f_E(a,b):E_A(a,b)\to E_B(f_V(a),f_V(b))$ is asurjection, and an extensional function isfaithful if every edge function is aninjection. An extensional function isinjective-on-objects? if the vertex function$f_V:V_A\to V_B$ is aninjection,surjective-on-objects if the vertex function is asurjection, andbijective-on-objects if the vertex function is abijection.

An extensional function is adagger functor if additionally it preserves the functions$\mathrm{refl}$,$\mathrm{sym}$,$\mathrm{trans}$

Anisomorphism of setoids is afull and faithfulbijective-on-objectsdagger functor.

Equivalence of definitions

Given a one-set-of-edges setoid$E\rightrightarrows V$, we define a family-of-sets-of-edges setoid by taking$E(x,y)$ to be thepreimage of$(x,y)$ under thefunction$(s,t):E\to V\times V$. Conversely, given a family-of-sets-of-edges setoid we define a one-set-of-edges setoid by taking$E$ to be thedisjoint union of the families of edges$E={\coprod }_{x,y\in V}E(x,y)$.

…

Examples

Themorphisms$E(a,b)$ of acategory$V$ with acontravariantendofunctor that is theidentity-on-objects is a pseudo-equivalence relation where

• for every vertex$a\in V$,$b\in V$,$c\in V$, and$d\in V$ and edge$f\in E(a,b)$,$g\in E(b,c)$, and$h\in E(c,d)$

  $$\mathrm{trans}(a,b,d)(f,\mathrm{trans}(b,c,d)(g,h))=\mathrm{trans}(a,c,d)(\mathrm{trans}(a,b,c)(f,g),h)$$

• for every vertex$a\in V$,$b\in V$ and edge$f\in E(a,b)$

  $$\mathrm{trans}(a,b,b)(f,\mathrm{refl}(b))=f$$

• for every vertex$a\in V$,$b\in V$ and edge$f\in E(a,b)$

  $$\mathrm{trans}(a,a,b)(\mathrm{refl}(a),f)=f$$

This includesdagger categories, where additionally

• for every vertex$a\in V$,$b\in V$ and edge$f\in E(a,b)$

  $$\mathrm{sym}(a,b)(\mathrm{sym}(b,a)(f))=f$$

• for every vertex$a\in V$,$b\in V$,$c\in V$ and edge$f\in E(a,b)$,$g\in E(b,c)$

  $$\mathrm{sym}(a,c)(\mathrm{trans}(a,b,c)(f,g))=\mathrm{trans}(c,b,a)(\mathrm{sym}(a,b)(f),\mathrm{sym}(b,c)(g))$$

• for every vertex$a\in V$

  $$\mathrm{sym}(a,a)(\mathrm{refl}(a))=\mathrm{refl}(a)$$

andgroupoids, where

• for every vertex$a\in V$,$b\in V$ and edge$f\in E(a,b)$

  $$\mathrm{trans}(a,b,a)(f,\mathrm{sym}(a,b)(f))=\mathrm{refl}(a)$$

• for every vertex$a\in V$,$b\in V$ and edge$f:E(a,b)$

  $$\mathrm{trans}(b,a,b)(\mathrm{sym}(a,b)(f),f)=\mathrm{refl}(b)$$

Additionally, a pseudo-equivalence relation on a set with one vertex is equivalent to apointedmagma with anendofunction.

Thin setoids

Recall in graph theory that a loop directed pseudograph issimple or aloop digraph if for every vertex$a\in V$ and$b\in V$, the set of edges$E(a,b)$ is asubsingleton: for every edge$f\in E(a,b)$ and$g\in E(a,b)$,$f=g$. In the other definition, a loop directed pseudograph is a loop digraph if the functions$s:E\to V$ and$t:E\to V$ arejointly monic.

A setoid isthin orsimple if its underlying loop directed pseudograph is a loop digraph. In both cases, the pseudo-equivalence relation becomes anequivalence relation. The term “thin” originates from category theory, while the term “simple” originates from graph theory.

A thin setoid is equivalently athindagger category, or a dagger categoryenriched intruth values. A thin setoid is also a thingroupoid, or a groupoid enriched in truth values.

Sometimes in the mathematical literature, setoids are thin by default.

Core of a pseudo-equivalence relation

For any pseudo-equivalence relation$A$, thecore of$A$ is defined as the maximalsubgroupoid?$\mathrm{Core}(A)$ of$A$.

More specifically, a sub-pseudo-equivalence relation of a pseudo-equivalence relation$A$ is a set$G$ with a pseudo-equivalence relation and an faithful injective-on-objects dagger functor$f:G\to A$. A sub-pseudo-equivalence relation$G$ of$A$ is a subgroupoid if$G$ additionally satisfy the groupoid equational axioms:

• for every vertex$a\in V_G$,$b\in V_G$,$c\in V_G$, and$d\in V_G$ and edge$f\in E_G(a,b)$,$g\in E_G(b,c)$, and$h\in E_G(c,d)$

  $$\mathrm{trans}(a,b,d)(f,\mathrm{trans}(b,c,d)(g,h))=\mathrm{trans}(a,c,d)(\mathrm{trans}(a,b,c)(f,g),h)$$

• for every vertex$a\in V_G$,$b\in V_G$ and edge$f\in E_G(a,b)$

  $$\mathrm{trans}(a,b,b)(f,\mathrm{refl}(b))=f$$

• for every vertex$a\in V_G$,$b\in V_G$ and edge$f\in E_G(a,b)$

  $$\mathrm{trans}(a,a,b)(\mathrm{refl}(a),f)=f$$

• for every vertex$a\in V_G$,$b\in V_G$ and edge$f\in E_G(a,b)$

  $$\mathrm{trans}(a,b,a)(f,\mathrm{sym}(a,b)(f))=\mathrm{refl}(a)$$

• for every vertex$a\in V_G$,$b\in V_G$ and edge$f:E_G(a,b)$

  $$\mathrm{trans}(b,a,b)(\mathrm{sym}(a,b)(f),f)=\mathrm{refl}(b)$$

Every pseudo-equivalence relation has at least one subgroupoid given by only theidentity morphisms$\mathrm{refl}(a):E_A(a,a)$ of$A$. A subgroupoid$G$ of a pseudo-equivalence relation$A$ is a maximal subgroupoid if the dagger functor$f:G\to A$ is bijective-on-objects, and additionally if, for every other subgroupoid$H$ of$A$ with faithful injective-on-objects dagger functor$g:H\to A$, there is a unique faithful injective-on-objects dagger functor$h:H\to G$ such that$h\circ f=g$.

Category of pseudo-equivalence relations

Let the category$\mathrm{Set}$ be defined as acategory that isfinitely complete andwell-pointed (i.e. whoseterminal object is aextremalgenerating object). This category of sets is not even aregular category, let alone anexact category, as can happen in certainfoundations of mathematics, such as bareset-levelMartin-Löf type theory, orZFC andETCS without thepowersetaxiom. The category$\mathrm{PseudoEquivRel}$ of sets with pseudo-equivalence relations is then theex/lex completion of Set.

More specifically, using the definition of pseudo-equivalence relation with two sets: if$(s_R,t_R):R\rightrightarrows X$ and$(s_S,t_S):S\rightrightarrows Y$ are two pseudo-equivalence relations, a morphism between them in$\mathrm{PseudoEquivRel}$ is defined to be a function$f:X\to Y$ with functions$f_1:R\to S$ with$s_S\circ f_1=f\circ s_R$ and$t_S\circ f_1=f\circ t_R$. Moreover, we declare two such functions$f,g:X\to Y$ to beequal if there exists a function$h:X\to S$ such that$s\circ h=f$ and$t\circ h=g$. Because$(s_S,t_S):S\rightrightarrows Y$ is a pseudo-equivalence relation, this defines an actualequivalence relation on the morphisms$f:X\to Y$, which is compatible with composition; thus we have a well-defined category$\mathrm{PseudoEquivRel}$ of pseudo-equivalence relations, which is the ex/lex completion of$\mathrm{Set}$.

We have afull and faithful functor$\mathrm{Set}\to \mathrm{PseudoEquivRel}$ sending an object$X$ to the pseudo-equivalence relation$(s_X,t_X):X\rightrightarrows X$. One can then verify directly that$\mathrm{PseudoEquivRel}$ is exact, that this embedding preserves finite limits, and that it is universal with respect to lex functors from$\mathrm{Set}$ into exact categories.

If thepresentation axiom (a weak form of the full axiom of choice) holds in$\mathrm{Set}$, as a subcategory of$\mathrm{PseudoEquivRel}$,$\mathrm{Set}$ could be thought of as the category ofcompletely presented sets, the category of sets with aprojective presentation. If theaxiom of choice holds in$\mathrm{Set}$, then$\mathrm{Set}$ is equivalent to$\mathrm{PseudoEquivRel}$, as the axiom of choice implies that$\mathrm{Set}$ is its own free exact completion, and$\mathrm{Set}$ is equivalent to$\mathrm{PseudoEquivRel}$ because the free functor from$\mathrm{Set}$ to$\mathrm{PseudoEquivRel}$ is anequivalence of categories.

This construction could be generalized to anyfinitely complete category$C$, from which the category ofinternal pseudo-equivalence relations of$C$ is theex/lex completion of$C$, and denoted as$C_{\mathrm{ex}/\mathrm{lex}}$. If everyepimorphism in$C$ is additionally asplit epimorphism, then$C$ is its own free exact completion.

In type theory

Manyset-level type theories usetypes which are0-truncated and thush-sets by default because of the inclusion ofuniqueness of identity proofs oraxiom K to the rule system of the type theory. Sometimes, these type theories do not havequotients andimage factorizations, and as a result, setoids are used instead of the native h-sets.

Inhomotopy type theory, and more generally in anyintensional type theory where not all types areh-sets, such as in a type theory withoutuniqueness of identity proofs oraxiom K, the notion of “setoid” bifurcates into multiple distinct notions. In analogy withcategory, the definitions used above in this article could be called astrict setoid. When the vertex types are only required to be atype rather than aset, then this defines apresetoid. There is also the notion of aunivalent setoid, where equality of vertices is isomorphism of vertices in the core of a presetoid.

 Related concepts

• Bishop set,setoid

• completely presented set

• equivalence relation

• quotient type

• directed graph

• pseudo-proset

• ex/lex completion

• homotopy exact completion

• extensional function

• dagger functor

• presetoid

• univalent setoid

• internal pseudo-equivalence relation

References

For setoids defined as a set with an pseudo-equivalence relation:

• Olov Wilander,Constructing a small category of setoids, Mathematical Structures in Computer Science22 1 (2012) 103-121 [doi:10.1017/S0960129511000478,pdf]

• Erik Palmgren,Olov Wilander,Constructing categories and setoids of setoids in type theory, Logical Methods in Computer Science,10 3 (2014) lmcs:964 [arXiv:1408.1364,doi:10.2168/LMCS-10(3:25)2014]

• Jacopo Emmenegger,Erik Palmgren,Exact completion and constructive theories of sets, J. Symb. Log.85 2 (2020) [arXiv:1710.10685,doi:10.1017/jsl.2020.2]

• Cioffo Cipriano Junior, Def. 1.1.1 in:Homotopy setoids and generalized quotient completion [pdf,pdf]

Last revised on July 7, 2023 at 18:15:07. See thehistory of this page for a list of all contributions to it.