CINXE.COM

<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1 plus MathML 2.0 plus SVG 1.1//EN" "http://www.w3.org/2002/04/xhtml-math-svg/xhtml-math-svg-flat.dtd" > <html xmlns="http://www.w3.org/1999/xhtml"> <head> <title> pseudo-equivalence relation in nLab </title> <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /> <meta name="robots" content="index,follow" /> <meta name="viewport" content="width=device-width, initial-scale=1" /> <link href="/stylesheets/instiki.css?1676280126" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/mathematics.css?1660229990" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/syntax.css?1660229990" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/nlab.css?1676280126" media="all" rel="stylesheet" type="text/css" /> <link rel="stylesheet" type="text/css" href="https://cdn.jsdelivr.net/gh/dreampulse/computer-modern-web-font@master/fonts.css"/> <style type="text/css"> h1#pageName, div.info, .newWikiWord a, a.existingWikiWord, .newWikiWord a:hover, [actiontype="toggle"]:hover, #TextileHelp h3 { color: #226622; } a:visited.existingWikiWord { color: #164416; } </style> <style type="text/css"><![CDATA[/*></style> <script src="/javascripts/prototype.js?1660229990" type="text/javascript"></script> <script src="/javascripts/effects.js?1660229990" type="text/javascript"></script> <script src="/javascripts/dragdrop.js?1660229990" type="text/javascript"></script> <script src="/javascripts/controls.js?1660229990" type="text/javascript"></script> <script src="/javascripts/application.js?1660229990" type="text/javascript"></script> <script src="/javascripts/page_helper.js?1660229990" type="text/javascript"></script> <script src="/javascripts/thm_numbering.js?1660229990" type="text/javascript"></script> <script type="text/x-mathjax-config"> <![CDATA[//><!]]> </script> <script type="text/javascript"> <![CDATA[//><!]]> </script> <link href="https://ncatlab.org/nlab/atom_with_headlines" rel="alternate" title="Atom with headlines" type="application/atom+xml" /> <link href="https://ncatlab.org/nlab/atom_with_content" rel="alternate" title="Atom with full content" type="application/atom+xml" /> <script type="text/javascript"> document.observe("dom:loaded", function() { generateThmNumbers(); }); </script> </head> <body> <div id="Container"> <div id="Content"> <h1 id="pageName"> <span style="float: left; margin: 0.5em 0.25em -0.25em 0"> <svg xmlns="http://www.w3.org/2000/svg" width="1.872em" height="1.8em" viewBox="0 0 190 181"> <path fill="#226622" d="M72.8 145c-1.6 17.3-15.7 10-23.6 20.2-5.6 7.3 4.8 15 11.4 15 11.5-.2 19-13.4 26.4-20.3 3.3-3 8.2-4 11.2-7.2a14 14 0 0 0 2.9-11.1c-1.4-9.6-12.4-18.6-16.9-27.2-5-9.6-10.7-27.4-24.1-27.7-17.4-.3-.4 26 4.7 30.7 2.4 2.3 5.4 4.1 7.3 6.9 1.6 2.3 2.1 5.8-1 7.2-5.9 2.6-12.4-6.3-15.5-10-8.8-10.6-15.5-23-26.2-31.8-5.2-4.3-11.8-8-18-3.7-7.3 4.9-4.2 12.9.2 18.5a81 81 0 0 0 30.7 23c3.3 1.5 12.8 5.6 10 10.7-2.5 5.2-11.7 3-15.6 1.1-8.4-3.8-24.3-21.3-34.4-13.7-3.5 2.6-2.3 7.6-1.2 11.1 2.8 9 12.2 17.2 20.9 20.5 17.3 6.7 34.3-8 50.8-12.1z"/> <path fill="#a41e32" d="M145.9 121.3c-.2-7.5 0-19.6-4.5-26-5.4-7.5-12.9-1-14.1 5.8-1.4 7.8 2.7 14.1 4.8 21.3 3.4 12 5.8 29-.8 40.1-3.6-6.7-5.2-13-7-20.4-2.1-8.2-12.8-13.2-15.1-1.9-2 9.7 9 21.2 12 30.1 1.2 4 2 8.8 6.4 10.3 6.9 2.3 13.3-4.7 17.7-8.8 12.2-11.5 36.6-20.7 43.4-36.4 6.7-15.7-13.7-14-21.3-7.2-9.1 8-11.9 20.5-23.6 25.1 7.5-23.7 31.8-37.6 38.4-61.4 2-7.3-.8-29.6-13-19.8-14.5 11.6-6.6 37.6-23.3 49.2z"/> <path fill="#193c78" d="M86.3 47.5c0-13-10.2-27.6-5.8-40.4 2.8-8.4 14.1-10.1 17-1 3.8 11.6-.3 26.3-1.8 38 11.7-.7 10.5-16 14.8-24.3 2.1-4.2 5.7-9.1 11-6.7 6 2.7 7.4 9.2 6.6 15.1-2.2 14-12.2 18.8-22.4 27-3.4 2.7-8 6.6-5.9 11.6 2 4.4 7 4.5 10.7 2.8 7.4-3.3 13.4-16.5 21.7-16 14.6.7 12 21.9.9 26.2-5 1.9-10.2 2.3-15.2 3.9-5.8 1.8-9.4 8.7-15.7 8.9-6.1.1-9-6.9-14.3-9-14.4-6-33.3-2-44.7-14.7-3.7-4.2-9.6-12-4.9-17.4 9.3-10.7 28 7.2 35.7 12 2 1.1 11 6.9 11.4 1.1.4-5.2-10-8.2-13.5-10-11.1-5.2-30-15.3-35-27.3-2.5-6 2.8-13.8 9.4-13.6 6.9.2 13.4 7 17.5 12C70.9 34 75 43.8 86.3 47.4z"/> </svg> </span> <span class="webName">nLab</span> pseudo-equivalence relation </h1> <div class="navigation"> <span class="skipNav"><a href='#navEnd'>Skip the Navigation Links</a> | </span> <span style="display:inline-block; width: 0.3em;"></span> <a href="/nlab/show/HomePage" accesskey="H" title="Home page">Home Page</a> | <a href="/nlab/all_pages" accesskey="A" title="List of all pages">All Pages</a> | <a href="/nlab/latest_revisions" accesskey="U" title="Latest edits and page creations">Latest Revisions</a> | <a href="https://nforum.ncatlab.org/discussion/16710/#Item_1" title="Discuss this page in its dedicated thread on the nForum" style="color: black">Discuss this page</a> | <form accept-charset="utf-8" action="/nlab/search" id="navigationSearchForm" method="get"> <fieldset class="search"><input type="text" id="searchField" name="query" value="Search" style="display:inline-block; float: left;" onfocus="this.value == 'Search' ? this.value = '' : true" onblur="this.value == '' ? this.value = 'Search' : true" /></fieldset> </form> <span id='navEnd'></span> </div> <div id="revision"> <html xmlns="http://www.w3.org/1999/xhtml" xmlns:svg="http://www.w3.org/2000/svg" xml:lang="en" lang="en"> <head><meta http-equiv="Content-type" content="application/xhtml+xml;charset=utf-8" /><title></title></head> <body> <div class="rightHandSide"> <div class="toc clickDown" tabindex="0"> <h3 id="context">Context</h3> <h4 id="category_theory">Category theory</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a></strong></p> <h2 id="sidebar_concepts">Concepts</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/category">category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/functor">functor</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/natural+transformation">natural transformation</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Cat">Cat</a></p> </li> </ul> <h2 id="sidebar_universal_constructions">Universal constructions</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/universal+construction">universal construction</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/representable+functor">representable functor</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/adjoint+functor">adjoint functor</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/limit">limit</a>/<a class="existingWikiWord" href="/nlab/show/colimit">colimit</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/weighted+limit">weighted limit</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/end">end</a>/<a class="existingWikiWord" href="/nlab/show/coend">coend</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Kan+extension">Kan extension</a></p> </li> </ul> </li> </ul> <h2 id="sidebar_theorems">Theorems</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Yoneda+lemma">Yoneda lemma</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Isbell+duality">Isbell duality</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Grothendieck+construction">Grothendieck construction</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/adjoint+functor+theorem">adjoint functor theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/monadicity+theorem">monadicity theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/adjoint+lifting+theorem">adjoint lifting theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Tannaka+duality">Tannaka duality</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Gabriel-Ulmer+duality">Gabriel-Ulmer duality</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/small+object+argument">small object argument</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Freyd-Mitchell+embedding+theorem">Freyd-Mitchell embedding theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/relation+between+type+theory+and+category+theory">relation between type theory and category theory</a></p> </li> </ul> <h2 id="sidebar_extensions">Extensions</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/sheaf+and+topos+theory">sheaf and topos theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/enriched+category+theory">enriched category theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/higher+category+theory">higher category theory</a></p> </li> </ul> <h2 id="sidebar_applications">Applications</h2> <ul> <li><a class="existingWikiWord" href="/nlab/show/applications+of+%28higher%29+category+theory">applications of (higher) category theory</a></li> </ul> <div> <p> <a href="/nlab/edit/category+theory+-+contents">Edit this sidebar</a> </p> </div></div></div> <h4 id="relations">Relations</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/relation">relation</a></strong>, <a class="existingWikiWord" href="/nlab/show/internal+relation">internal relation</a></p> <p><strong><a class="existingWikiWord" href="/nlab/show/Rel">Rel</a></strong>, <a class="existingWikiWord" href="/nlab/show/bicategory+of+relations">bicategory of relations</a>, <a class="existingWikiWord" href="/nlab/show/allegory">allegory</a></p> <h2 id="types_of_binary_relation">Types of Binary relation</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/reflexive+relation">reflexive</a>, <a class="existingWikiWord" href="/nlab/show/irreflexive+relation">irreflexive</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/symmetric+relation">symmetric</a>, <a class="existingWikiWord" href="/nlab/show/antisymmetric+relation">antisymmetric</a> <a class="existingWikiWord" href="/nlab/show/asymmetric+relation">asymmetric</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/transitive+relation">transitive</a>, <a class="existingWikiWord" href="/nlab/show/comparison">comparison</a>;</p> </li> <li> <p>left and right <a class="existingWikiWord" href="/nlab/show/euclidean+relation">euclidean</a>;</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/total+relation">total</a>, <a class="existingWikiWord" href="/nlab/show/connected+relation">connected</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/extensional+relation">extensional</a>, <a class="existingWikiWord" href="/nlab/show/well-founded+relation">well-founded</a> relations.</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/functional+relations">functional relations</a>,</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/entire+relations">entire relations</a>,</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/equivalence+relations">equivalence relations</a>, <a class="existingWikiWord" href="/nlab/show/congruence">congruence</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/apartness+relations">apartness relations</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/simple+graph">simple graph</a></p> </li> </ul> <h2 id="in_higher_category_theory">In higher category theory</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/2-congruence">2-congruence</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/%28n%2Cr%29-congruence">(n,r)-congruence</a></p> </li> </ul> <div> <p> <a href="/nlab/edit/relations+-+contents">Edit this sidebar</a> </p> </div></div></div> <h4 id="graph_theory">Graph theory</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/graph+theory">graph theory</a></strong></p> <p><a class="existingWikiWord" href="/nlab/show/graph">graph</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/vertex">vertex</a>, <a class="existingWikiWord" href="/nlab/show/edge">edge</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/omega-graph">omega-graph</a>, <a class="existingWikiWord" href="/nlab/show/hypergraph">hypergraph</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/quiver">quiver</a>, <a class="existingWikiWord" href="/nlab/show/n-quiver">n-quiver</a></p> </li> </ul> <p><a class="existingWikiWord" href="/nlab/show/category+of+simple+graphs">category of simple graphs</a></p> <h3 id="properties">Properties</h3> <ul> <li><a class="existingWikiWord" href="/nlab/show/graph+distance">graph distance</a></li> </ul> <h3 id="extra_properties">Extra properties</h3> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/reflexive+graph">reflexive</a>, <a class="existingWikiWord" href="/nlab/show/directed+graph">directed</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/bipartite+graph">bipartite</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/planar+graph">planar</a></p> </li> </ul> <h3 id="extra_structure">Extra structure</h3> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/reflexive+graph">reflexive</a><a class="existingWikiWord" href="/nlab/show/directed+graph">directed graph</a> + <a class="existingWikiWord" href="/nlab/show/unit+law">unital</a> <a class="existingWikiWord" href="/nlab/show/associative">associative</a> <a class="existingWikiWord" href="/nlab/show/composition">composition</a> = <a class="existingWikiWord" href="/nlab/show/category">category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/ribbon+graph">ribbon graph</a>, <a class="existingWikiWord" href="/nlab/show/combinatorial+map">combinatorial map</a>, <a class="existingWikiWord" href="/nlab/show/topological+map">topological map</a>, <a class="existingWikiWord" href="/nlab/show/child%27s+drawing">child's drawing</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/vertex+coloring">vertex coloring</a>, <a class="existingWikiWord" href="/nlab/show/clique">clique</a></p> </li> </ul> </div></div> </div> </div> <h1 id='section_table_of_contents'>Contents</h1> <div class='maruku_toc'> <ul> <li><a href='#idea'>Idea</a></li> <li><a href='#definition'>Definition</a></li> <ul> <li><a href='#with_a_family_of_sets'>With a family of sets</a></li> <li><a href='#with_a_set'>With a set</a></li> <li><a href='#extensional_functions_dagger_functors_and_isomorphisms'>Extensional functions, dagger functors, and isomorphisms</a></li> <li><a href='#equivalence_of_definitions'>Equivalence of definitions</a></li> </ul> <li><a href='#examples'>Examples</a></li> <li><a href='#thin_setoids'>Thin setoids</a></li> <li><a href='#core_of_a_pseudoequivalence_relation'>Core of a pseudo-equivalence relation</a></li> <li><a href='#category_of_pseudoequivalence_relations'>Category of pseudo-equivalence relations</a></li> <li><a href='#in_type_theory'>In type theory</a></li> <li><a href='#related_concepts'> Related concepts</a></li> <li><a href='#references'>References</a></li> </ul> </div> <h2 id="idea">Idea</h2> <p>A <em>pseudo-equivalence relation</em> is like an <a class="existingWikiWord" href="/nlab/show/equivalence+relation">equivalence relation</a>, but where we allow more than one element in the relation; i.e. the underlying <a class="existingWikiWord" href="/nlab/show/directed+graph">directed graph</a> of the relation is a <a class="existingWikiWord" href="/nlab/show/directed+pseudograph">directed pseudograph</a>. In the same way that <a class="existingWikiWord" href="/nlab/show/magmoids">magmoids</a> are the raw structure used to build <a class="existingWikiWord" href="/nlab/show/semicategories">semicategories</a> and <a class="existingWikiWord" href="/nlab/show/categories">categories</a>, sets with pseudo-equivalence relations are the raw structure used to build <a class="existingWikiWord" href="/nlab/show/dagger+categories">dagger categories</a> and <a class="existingWikiWord" href="/nlab/show/groupoids">groupoids</a> (i.e. a groupoid without associativity, unital laws, and inverse laws).</p> <p>Sets equipped with pseudo-equivalence relations are sometimes called <em><a class="existingWikiWord" href="/nlab/show/setoids">setoids</a></em> (i.e. in <a href="#Wilander12">Wilander (2012), §4</a>; <a href="#PalmgrenWilander14">Palmgren & Wilander (2014), §2, §6</a>; <a href="#EmmeneggerPalmgren20">Emmenegger & Palmgren (2020), §6</a>; <a href="#Cipriano20">Cipriano (2020), Def. 1.1.1</a>), but the term “setoid” is also used in mathematics to refer only to the sets with <a class="existingWikiWord" href="/nlab/show/equivalence+relations">equivalence relations</a>. In this article, the term “setoid” is used in the former sense of “sets equipped with pseudo-equivalence relations”.</p> <h2 id="definition">Definition</h2> <h3 id="with_a_family_of_sets">With a family of sets</h3> <p>Using graph theoretic terminology, a <strong>pseudo-equivalence relation</strong> on a set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>V</mi></mrow><annotation encoding="application/x-tex">V</annotation></semantics></math> of <a class="existingWikiWord" href="/nlab/show/vertices">vertices</a> is a family of sets <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>E</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">E(a, b)</annotation></semantics></math> of <a class="existingWikiWord" href="/nlab/show/edges">edges</a> for each vertex <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∈</mo><mi>V</mi></mrow><annotation encoding="application/x-tex">a \in V</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi><mo>∈</mo><mi>V</mi></mrow><annotation encoding="application/x-tex">b \in V</annotation></semantics></math>, which comes with the following additional structure</p> <ul> <li> <p>for each vertex <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∈</mo><mi>V</mi></mrow><annotation encoding="application/x-tex">a \in V</annotation></semantics></math> an element</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">refl</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo><mo>∈</mo><mi>E</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>a</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathrm{refl}(a) \in E(a, a)</annotation></semantics></math></div></li> <li> <p>for each vertex <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∈</mo><mi>V</mi></mrow><annotation encoding="application/x-tex">a \in V</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi><mo>∈</mo><mi>V</mi></mrow><annotation encoding="application/x-tex">b \in V</annotation></semantics></math> a family of functions</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">sym</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><mo>:</mo><mi>E</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><mo>→</mo><mi>E</mi><mo stretchy="false">(</mo><mi>b</mi><mo>,</mo><mi>a</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathrm{sym}(a, b):E(a, b) \to E(b, a)</annotation></semantics></math></div></li> <li> <p>for each vertex <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∈</mo><mi>V</mi></mrow><annotation encoding="application/x-tex">a \in V</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi><mo>∈</mo><mi>V</mi></mrow><annotation encoding="application/x-tex">b \in V</annotation></semantics></math>, and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>c</mi><mo lspace="0em" rspace="thinmathspace">inV</mo></mrow><annotation encoding="application/x-tex">c \inV</annotation></semantics></math>, a family of functions</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">trans</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo>,</mo><mi>c</mi><mo stretchy="false">)</mo><mo>:</mo><mo stretchy="false">(</mo><mi>E</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><mo>×</mo><mi>E</mi><mo stretchy="false">(</mo><mi>b</mi><mo>,</mo><mi>c</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>→</mo><mi>E</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>c</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathrm{trans}(a, b, c):(E(a, b) \times E(b, c)) \to E(a, c)</annotation></semantics></math></div></li> </ul> <h3 id="with_a_set">With a set</h3> <p>A <strong>pseuodo-equivalence relation</strong> on a <a class="existingWikiWord" href="/nlab/show/set">set</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>V</mi></mrow><annotation encoding="application/x-tex">V</annotation></semantics></math> is a set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>E</mi></mrow><annotation encoding="application/x-tex">E</annotation></semantics></math> and functions <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi><mo>:</mo><mi>E</mi><mo>→</mo><mi>V</mi></mrow><annotation encoding="application/x-tex">s:E \to V</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>t</mi><mo>:</mo><mi>E</mi><mo>→</mo><mi>V</mi></mrow><annotation encoding="application/x-tex">t:E \to V</annotation></semantics></math> (a loop <a class="existingWikiWord" href="/nlab/show/directed+pseudograph">directed pseudograph</a>), with with functions <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">refl</mi><mo>:</mo><mi>V</mi><mo>→</mo><mi>E</mi></mrow><annotation encoding="application/x-tex">\mathrm{refl}:V \to E</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">sym</mi><mo>:</mo><mi>E</mi><mo>→</mo><mi>E</mi></mrow><annotation encoding="application/x-tex">\mathrm{sym}:E \to E</annotation></semantics></math>, and</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">trans</mi><mo>:</mo><mo stretchy="false">{</mo><mo stretchy="false">(</mo><mi>f</mi><mo>,</mo><mi>g</mi><mo stretchy="false">)</mo><mo>∈</mo><mi>E</mi><mo>×</mo><mi>E</mi><mo stretchy="false">|</mo><mi>t</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><msub><mo>=</mo> <mi>V</mi></msub><mi>s</mi><mo stretchy="false">(</mo><mi>g</mi><mo stretchy="false">)</mo><mo stretchy="false">}</mo><mo>→</mo><mi>E</mi></mrow><annotation encoding="application/x-tex">\mathrm{trans}:\{(f,g) \in E \times E \vert t(f) =_V s(g)\} \to E</annotation></semantics></math></div> <p>such that</p> <ul> <li>for every <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∈</mo><mi>V</mi></mrow><annotation encoding="application/x-tex">a \in V</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi><mo stretchy="false">(</mo><mi mathvariant="normal">refl</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><msub><mo>=</mo> <mi>E</mi></msub><mi>a</mi></mrow><annotation encoding="application/x-tex">s(\mathrm{refl}(a)) =_E a</annotation></semantics></math></li> <li>for every <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∈</mo><mi>V</mi></mrow><annotation encoding="application/x-tex">a \in V</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>t</mi><mo stretchy="false">(</mo><mi mathvariant="normal">refl</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><msub><mo>=</mo> <mi>E</mi></msub><mi>a</mi></mrow><annotation encoding="application/x-tex">t(\mathrm{refl}(a)) =_E a</annotation></semantics></math></li> <li>for every <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>∈</mo><mi>E</mi></mrow><annotation encoding="application/x-tex">f \in E</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><msub><mo>=</mo> <mi>V</mi></msub><mi>t</mi><mo stretchy="false">(</mo><mi mathvariant="normal">sym</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">s(f) =_V t(\mathrm{sym}(f))</annotation></semantics></math></li> <li>for every <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>∈</mo><mi>E</mi></mrow><annotation encoding="application/x-tex">f \in E</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>t</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><msub><mo>=</mo> <mi>V</mi></msub><mi>s</mi><mo stretchy="false">(</mo><mi mathvariant="normal">sym</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">t(f) =_V s(\mathrm{sym}(f))</annotation></semantics></math></li> <li>for every <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>∈</mo><mi>E</mi></mrow><annotation encoding="application/x-tex">f \in E</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>g</mi><mo>∈</mo><mi>E</mi></mrow><annotation encoding="application/x-tex">g \in E</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>t</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><msub><mo>=</mo> <mi>V</mi></msub><mi>s</mi><mo stretchy="false">(</mo><mi>g</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">t(f) =_V s(g)</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi><mo stretchy="false">(</mo><mi mathvariant="normal">trans</mi><mo stretchy="false">(</mo><mi>f</mi><mo>,</mo><mi>g</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><msub><mo>=</mo> <mi>E</mi></msub><mi>s</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">s(\mathrm{trans}(f,g)) =_E s(f)</annotation></semantics></math></li> <li>for every <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>∈</mo><mi>E</mi></mrow><annotation encoding="application/x-tex">f \in E</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>g</mi><mo>∈</mo><mi>E</mi></mrow><annotation encoding="application/x-tex">g \in E</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>t</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><msub><mo>=</mo> <mi>V</mi></msub><mi>s</mi><mo stretchy="false">(</mo><mi>g</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">t(f) =_V s(g)</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>t</mi><mo stretchy="false">(</mo><mi mathvariant="normal">trans</mi><mo stretchy="false">(</mo><mi>f</mi><mo>,</mo><mi>g</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><msub><mo>=</mo> <mi>E</mi></msub><mi>t</mi><mo stretchy="false">(</mo><mi>g</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">t(\mathrm{trans}(f,g)) =_E t(g)</annotation></semantics></math></li> </ul> <h3 id="extensional_functions_dagger_functors_and_isomorphisms">Extensional functions, dagger functors, and isomorphisms</h3> <p>We define an <strong><a class="existingWikiWord" href="/nlab/show/extensional+function">extensional function</a></strong> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><mi>A</mi><mo>→</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">f:A \to B</annotation></semantics></math> between two sets <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math> with pseudo-equivalence relations <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><msub><mi>E</mi> <mi>A</mi></msub><mo>,</mo><msub><mi mathvariant="normal">refl</mi> <mi>A</mi></msub><mo>,</mo><msub><mi mathvariant="normal">sym</mi> <mi>A</mi></msub><mo>,</mo><msub><mi mathvariant="normal">trans</mi> <mi>A</mi></msub><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(E_A, \mathrm{refl}_A, \mathrm{sym}_A, \mathrm{trans}_A)</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><msub><mi>E</mi> <mi>B</mi></msub><mo>,</mo><msub><mi mathvariant="normal">refl</mi> <mi>B</mi></msub><mo>,</mo><msub><mi mathvariant="normal">sym</mi> <mi>B</mi></msub><mo>,</mo><msub><mi mathvariant="normal">trans</mi> <mi>B</mi></msub><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(E_B, \mathrm{refl}_B, \mathrm{sym}_B, \mathrm{trans}_B)</annotation></semantics></math> to be a function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>f</mi> <mi>V</mi></msub><mo>:</mo><mi>A</mi><mo>→</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">f_V:A \to B</annotation></semantics></math> and a family of functions <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>f</mi> <mi>E</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><mo>:</mo><msub><mi>E</mi> <mi>A</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><mo>→</mo><msub><mi>E</mi> <mi>B</mi></msub><mo stretchy="false">(</mo><msub><mi>f</mi> <mi>V</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo><mo>,</mo><msub><mi>f</mi> <mi>V</mi></msub><mo stretchy="false">(</mo><mi>b</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f_E(a, b):E_A(a, b) \to E_B(f_V(a), f_V(b))</annotation></semantics></math></p> <p>Composition of extensional functions is defined as composition of the vertex function and of each edge function.</p> <p>An extensional function between two sets with pseudo-equivalence relations is <strong>full</strong> if every edge function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>f</mi> <mi>E</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><mo>:</mo><msub><mi>E</mi> <mi>A</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><mo>→</mo><msub><mi>E</mi> <mi>B</mi></msub><mo stretchy="false">(</mo><msub><mi>f</mi> <mi>V</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo><mo>,</mo><msub><mi>f</mi> <mi>V</mi></msub><mo stretchy="false">(</mo><mi>b</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f_E(a, b):E_A(a, b) \to E_B(f_V(a), f_V(b))</annotation></semantics></math> is a <a class="existingWikiWord" href="/nlab/show/surjection">surjection</a>, and an extensional function is <strong>faithful</strong> if every edge function is an <a class="existingWikiWord" href="/nlab/show/injection">injection</a>. An extensional function is <strong><span class="newWikiWord">injective-on-objects<a href="/nlab/new/injective-on-objects">?</a></span></strong> if the vertex function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>f</mi> <mi>V</mi></msub><mo>:</mo><msub><mi>V</mi> <mi>A</mi></msub><mo>→</mo><msub><mi>V</mi> <mi>B</mi></msub></mrow><annotation encoding="application/x-tex">f_V:V_A \to V_B</annotation></semantics></math> is an <a class="existingWikiWord" href="/nlab/show/injection">injection</a>, <strong><a class="existingWikiWord" href="/nlab/show/surjective-on-objects">surjective-on-objects</a></strong> if the vertex function is a <a class="existingWikiWord" href="/nlab/show/surjection">surjection</a>, and <strong><a class="existingWikiWord" href="/nlab/show/bijective-on-objects">bijective-on-objects</a></strong> if the vertex function is a <a class="existingWikiWord" href="/nlab/show/bijection">bijection</a>.</p> <p>An extensional function is a <strong><a class="existingWikiWord" href="/nlab/show/dagger+functor">dagger functor</a></strong> if additionally it preserves the functions <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">refl</mi></mrow><annotation encoding="application/x-tex">\mathrm{refl}</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">sym</mi></mrow><annotation encoding="application/x-tex">\mathrm{sym}</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">trans</mi></mrow><annotation encoding="application/x-tex">\mathrm{trans}</annotation></semantics></math></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msub><mi>f</mi> <mi>E</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>a</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><msub><mi mathvariant="normal">refl</mi> <mi>A</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>=</mo><msub><mi mathvariant="normal">refl</mi> <mi>B</mi></msub><mo stretchy="false">(</mo><msub><mi>f</mi> <mi>V</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f_E(a, a)(\mathrm{refl}_A(a)) = \mathrm{refl}_B(f_V(a))</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msub><mi>f</mi> <mi>E</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><msub><mi mathvariant="normal">sym</mi> <mi>A</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>=</mo><msub><mi mathvariant="normal">sym</mi> <mi>B</mi></msub><mo stretchy="false">(</mo><msub><mi>f</mi> <mi>V</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo><mo>,</mo><msub><mi>f</mi> <mi>V</mi></msub><mo stretchy="false">(</mo><mi>b</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo stretchy="false">(</mo><msub><mi>f</mi> <mi>E</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f_E(a, b)(\mathrm{sym}_A(a, b)(f)) = \mathrm{sym}_B(f_V(a), f_V(b))(f_E(a, b)(f))</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msub><mi>f</mi> <mi>E</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>c</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><msub><mi mathvariant="normal">trans</mi> <mi>A</mi></msub><mo stretchy="false">(</mo><mi>f</mi><mo>,</mo><mi>g</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>=</mo><msub><mi mathvariant="normal">trans</mi> <mi>B</mi></msub><mo stretchy="false">(</mo><msub><mi>f</mi> <mi>E</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo>,</mo><msub><mi>f</mi> <mi>E</mi></msub><mo stretchy="false">(</mo><mi>b</mi><mo>,</mo><mi>c</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi>g</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f_E(a, c)(\mathrm{trans}_A(f,g)) = \mathrm{trans}_B(f_E(a, b)(f), f_E(b, c)(g)</annotation></semantics></math></div> <p>An <strong>isomorphism of setoids</strong> is a <a class="existingWikiWord" href="/nlab/show/full+and+faithful">full and faithful</a> <a class="existingWikiWord" href="/nlab/show/bijective-on-objects">bijective-on-objects</a> <a class="existingWikiWord" href="/nlab/show/dagger+functor">dagger functor</a>.</p> <h3 id="equivalence_of_definitions">Equivalence of definitions</h3> <p>Given a one-set-of-edges setoid <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>E</mi><mo>⇉</mo><mi>V</mi></mrow><annotation encoding="application/x-tex">E\rightrightarrows V</annotation></semantics></math>, we define a family-of-sets-of-edges setoid by taking <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>E</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">E(x,y)</annotation></semantics></math> to be the <a class="existingWikiWord" href="/nlab/show/preimage">preimage</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(x,y)</annotation></semantics></math> under the <a class="existingWikiWord" href="/nlab/show/function">function</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>s</mi><mo>,</mo><mi>t</mi><mo stretchy="false">)</mo><mo>:</mo><mi>E</mi><mo>→</mo><mi>V</mi><mo>×</mo><mi>V</mi></mrow><annotation encoding="application/x-tex">(s,t):E \to V\times V</annotation></semantics></math>. Conversely, given a family-of-sets-of-edges setoid we define a one-set-of-edges setoid by taking <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>E</mi></mrow><annotation encoding="application/x-tex">E</annotation></semantics></math> to be the <a class="existingWikiWord" href="/nlab/show/disjoint+union">disjoint union</a> of the families of edges <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>E</mi><mo>=</mo><msub><mo lspace="thinmathspace" rspace="thinmathspace">∐</mo> <mrow><mi>x</mi><mo>,</mo><mi>y</mi><mo>∈</mo><mi>V</mi></mrow></msub><mi>E</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">E = \coprod_{x,y\in V} E(x,y)</annotation></semantics></math>.</p> <p>…</p> <h2 id="examples">Examples</h2> <p>The <a class="existingWikiWord" href="/nlab/show/morphisms">morphisms</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>E</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">E(a, b)</annotation></semantics></math> of a <a class="existingWikiWord" href="/nlab/show/category">category</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>V</mi></mrow><annotation encoding="application/x-tex">V</annotation></semantics></math> with a <a class="existingWikiWord" href="/nlab/show/contravariant+functor">contravariant</a> <a class="existingWikiWord" href="/nlab/show/endofunctor">endofunctor</a> that is the <a class="existingWikiWord" href="/nlab/show/identity-on-objects">identity-on-objects</a> is a pseudo-equivalence relation where</p> <ul> <li> <p>for every vertex <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∈</mo><mi>V</mi></mrow><annotation encoding="application/x-tex">a \in V</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi><mo>∈</mo><mi>V</mi></mrow><annotation encoding="application/x-tex">b \in V</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>c</mi><mo>∈</mo><mi>V</mi></mrow><annotation encoding="application/x-tex">c \in V</annotation></semantics></math>, and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>d</mi><mo>∈</mo><mi>V</mi></mrow><annotation encoding="application/x-tex">d \in V</annotation></semantics></math> and edge <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>∈</mo><mi>E</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f \in E(a, b)</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>g</mi><mo>∈</mo><mi>E</mi><mo stretchy="false">(</mo><mi>b</mi><mo>,</mo><mi>c</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">g \in E(b, c)</annotation></semantics></math>, and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>h</mi><mo>∈</mo><mi>E</mi><mo stretchy="false">(</mo><mi>c</mi><mo>,</mo><mi>d</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">h \in E(c, d)</annotation></semantics></math></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">trans</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo>,</mo><mi>d</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi>f</mi><mo>,</mo><mi mathvariant="normal">trans</mi><mo stretchy="false">(</mo><mi>b</mi><mo>,</mo><mi>c</mi><mo>,</mo><mi>d</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi>g</mi><mo>,</mo><mi>h</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>=</mo><mi mathvariant="normal">trans</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>c</mi><mo>,</mo><mi>d</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi mathvariant="normal">trans</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo>,</mo><mi>c</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi>f</mi><mo>,</mo><mi>g</mi><mo stretchy="false">)</mo><mo>,</mo><mi>h</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\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)</annotation></semantics></math></div></li> <li> <p>for every vertex <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∈</mo><mi>V</mi></mrow><annotation encoding="application/x-tex">a \in V</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi><mo>∈</mo><mi>V</mi></mrow><annotation encoding="application/x-tex">b \in V</annotation></semantics></math> and edge <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>∈</mo><mi>E</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f \in E(a, b)</annotation></semantics></math></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">trans</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi>f</mi><mo>,</mo><mi mathvariant="normal">refl</mi><mo stretchy="false">(</mo><mi>b</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>=</mo><mi>f</mi></mrow><annotation encoding="application/x-tex">\mathrm{trans}(a, b, b)(f, \mathrm{refl}(b)) = f</annotation></semantics></math></div></li> <li> <p>for every vertex <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∈</mo><mi>V</mi></mrow><annotation encoding="application/x-tex">a \in V</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi><mo>∈</mo><mi>V</mi></mrow><annotation encoding="application/x-tex">b \in V</annotation></semantics></math> and edge <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>∈</mo><mi>E</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f \in E(a, b)</annotation></semantics></math></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">trans</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi mathvariant="normal">refl</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo><mo>,</mo><mi>f</mi><mo stretchy="false">)</mo><mo>=</mo><mi>f</mi></mrow><annotation encoding="application/x-tex">\mathrm{trans}(a, a, b)(\mathrm{refl}(a), f) = f</annotation></semantics></math></div></li> </ul> <p>This includes <a class="existingWikiWord" href="/nlab/show/dagger+categories">dagger categories</a>, where additionally</p> <ul> <li> <p>for every vertex <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∈</mo><mi>V</mi></mrow><annotation encoding="application/x-tex">a \in V</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi><mo>∈</mo><mi>V</mi></mrow><annotation encoding="application/x-tex">b \in V</annotation></semantics></math> and edge <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>∈</mo><mi>E</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f \in E(a, b)</annotation></semantics></math></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">sym</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi mathvariant="normal">sym</mi><mo stretchy="false">(</mo><mi>b</mi><mo>,</mo><mi>a</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>=</mo><mi>f</mi></mrow><annotation encoding="application/x-tex">\mathrm{sym}(a, b)(\mathrm{sym}(b, a)(f)) = f</annotation></semantics></math></div></li> <li> <p>for every vertex <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∈</mo><mi>V</mi></mrow><annotation encoding="application/x-tex">a \in V</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi><mo>∈</mo><mi>V</mi></mrow><annotation encoding="application/x-tex">b \in V</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>c</mi><mo>∈</mo><mi>V</mi></mrow><annotation encoding="application/x-tex">c \in V</annotation></semantics></math> and edge <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>∈</mo><mi>E</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f \in E(a, b)</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>g</mi><mo>∈</mo><mi>E</mi><mo stretchy="false">(</mo><mi>b</mi><mo>,</mo><mi>c</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">g \in E(b, c)</annotation></semantics></math></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">sym</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>c</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi mathvariant="normal">trans</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo>,</mo><mi>c</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi>f</mi><mo>,</mo><mi>g</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>=</mo><mi mathvariant="normal">trans</mi><mo stretchy="false">(</mo><mi>c</mi><mo>,</mo><mi>b</mi><mo>,</mo><mi>a</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi mathvariant="normal">sym</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo>,</mo><mi mathvariant="normal">sym</mi><mo stretchy="false">(</mo><mi>b</mi><mo>,</mo><mi>c</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi>g</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\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))</annotation></semantics></math></div></li> <li> <p>for every vertex <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∈</mo><mi>V</mi></mrow><annotation encoding="application/x-tex">a \in V</annotation></semantics></math></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">sym</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>a</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi mathvariant="normal">refl</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>=</mo><mi mathvariant="normal">refl</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathrm{sym}(a, a)(\mathrm{refl}(a)) = \mathrm{refl}(a)</annotation></semantics></math></div></li> </ul> <p>and <a class="existingWikiWord" href="/nlab/show/groupoids">groupoids</a>, where</p> <ul> <li> <p>for every vertex <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∈</mo><mi>V</mi></mrow><annotation encoding="application/x-tex">a \in V</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi><mo>∈</mo><mi>V</mi></mrow><annotation encoding="application/x-tex">b \in V</annotation></semantics></math> and edge <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>∈</mo><mi>E</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f \in E(a, b)</annotation></semantics></math></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">trans</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo>,</mo><mi>a</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi>f</mi><mo>,</mo><mi mathvariant="normal">sym</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>=</mo><mi mathvariant="normal">refl</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathrm{trans}(a, b, a)(f, \mathrm{sym}(a, b)(f)) = \mathrm{refl}(a)</annotation></semantics></math></div></li> <li> <p>for every vertex <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∈</mo><mi>V</mi></mrow><annotation encoding="application/x-tex">a \in V</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi><mo>∈</mo><mi>V</mi></mrow><annotation encoding="application/x-tex">b \in V</annotation></semantics></math> and edge <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><mi>E</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f:E(a, b)</annotation></semantics></math></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">trans</mi><mo stretchy="false">(</mo><mi>b</mi><mo>,</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi mathvariant="normal">sym</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo>,</mo><mi>f</mi><mo stretchy="false">)</mo><mo>=</mo><mi mathvariant="normal">refl</mi><mo stretchy="false">(</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathrm{trans}(b, a, b)(\mathrm{sym}(a, b)(f), f) = \mathrm{refl}(b)</annotation></semantics></math></div></li> </ul> <p>Additionally, a pseudo-equivalence relation on a set with one vertex is equivalent to a <a class="existingWikiWord" href="/nlab/show/pointed+set">pointed</a> <a class="existingWikiWord" href="/nlab/show/magma">magma</a> with an <a class="existingWikiWord" href="/nlab/show/endofunction">endofunction</a>.</p> <h2 id="thin_setoids">Thin setoids</h2> <p>Recall in graph theory that a loop directed pseudograph is <strong>simple</strong> or a <strong>loop digraph</strong> if for every vertex <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∈</mo><mi>V</mi></mrow><annotation encoding="application/x-tex">a \in V</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi><mo>∈</mo><mi>V</mi></mrow><annotation encoding="application/x-tex">b \in V</annotation></semantics></math>, the set of edges <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>E</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">E(a, b)</annotation></semantics></math> is a <a class="existingWikiWord" href="/nlab/show/subsingleton">subsingleton</a>: for every edge <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>∈</mo><mi>E</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f \in E(a, b)</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>g</mi><mo>∈</mo><mi>E</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">g \in E(a, b)</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>=</mo><mi>g</mi></mrow><annotation encoding="application/x-tex">f = g</annotation></semantics></math>. In the other definition, a loop directed pseudograph is a loop digraph if the functions <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi><mo>:</mo><mi>E</mi><mo>→</mo><mi>V</mi></mrow><annotation encoding="application/x-tex">s:E \to V</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>t</mi><mo>:</mo><mi>E</mi><mo>→</mo><mi>V</mi></mrow><annotation encoding="application/x-tex">t:E \to V</annotation></semantics></math> are <a class="existingWikiWord" href="/nlab/show/jointly+monic">jointly monic</a>.</p> <p>A setoid is <strong>thin</strong> or <strong>simple</strong> if its underlying loop directed pseudograph is a loop digraph. In both cases, the pseudo-equivalence relation becomes an <strong><a class="existingWikiWord" href="/nlab/show/equivalence+relation">equivalence relation</a></strong>. The term “thin” originates from category theory, while the term “simple” originates from graph theory.</p> <p>A thin setoid is equivalently a <a class="existingWikiWord" href="/nlab/show/thin+category">thin</a> <a class="existingWikiWord" href="/nlab/show/dagger+category">dagger category</a>, or a dagger category <a class="existingWikiWord" href="/nlab/show/enriched+category">enriched</a> in <a class="existingWikiWord" href="/nlab/show/truth+values">truth values</a>. A thin setoid is also a thin <a class="existingWikiWord" href="/nlab/show/groupoid">groupoid</a>, or a groupoid enriched in truth values.</p> <p>Sometimes in the mathematical literature, setoids are thin by default.</p> <h2 id="core_of_a_pseudoequivalence_relation">Core of a pseudo-equivalence relation</h2> <p>For any pseudo-equivalence relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>, the <a class="existingWikiWord" href="/nlab/show/core">core</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> is defined as the maximal <span class="newWikiWord">subgroupoid<a href="/nlab/new/subgroupoid">?</a></span> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">Core</mi><mo stretchy="false">(</mo><mi>A</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathrm{Core}(A)</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>.</p> <p>More specifically, a sub-pseudo-equivalence relation of a pseudo-equivalence relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> is a set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>G</mi></mrow><annotation encoding="application/x-tex">G</annotation></semantics></math> with a pseudo-equivalence relation and an faithful injective-on-objects dagger functor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><mi>G</mi><mo>→</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">f:G \to A</annotation></semantics></math>. A sub-pseudo-equivalence relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>G</mi></mrow><annotation encoding="application/x-tex">G</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> is a subgroupoid if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>G</mi></mrow><annotation encoding="application/x-tex">G</annotation></semantics></math> additionally satisfy the groupoid equational axioms:</p> <ul> <li> <p>for every vertex <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∈</mo><msub><mi>V</mi> <mi>G</mi></msub></mrow><annotation encoding="application/x-tex">a \in V_G</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi><mo>∈</mo><msub><mi>V</mi> <mi>G</mi></msub></mrow><annotation encoding="application/x-tex">b \in V_G</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>c</mi><mo>∈</mo><msub><mi>V</mi> <mi>G</mi></msub></mrow><annotation encoding="application/x-tex">c \in V_G</annotation></semantics></math>, and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>d</mi><mo>∈</mo><msub><mi>V</mi> <mi>G</mi></msub></mrow><annotation encoding="application/x-tex">d \in V_G</annotation></semantics></math> and edge <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>∈</mo><msub><mi>E</mi> <mi>G</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f \in E_G(a, b)</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>g</mi><mo>∈</mo><msub><mi>E</mi> <mi>G</mi></msub><mo stretchy="false">(</mo><mi>b</mi><mo>,</mo><mi>c</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">g \in E_G(b, c)</annotation></semantics></math>, and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>h</mi><mo>∈</mo><msub><mi>E</mi> <mi>G</mi></msub><mo stretchy="false">(</mo><mi>c</mi><mo>,</mo><mi>d</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">h \in E_G(c, d)</annotation></semantics></math></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">trans</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo>,</mo><mi>d</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi>f</mi><mo>,</mo><mi mathvariant="normal">trans</mi><mo stretchy="false">(</mo><mi>b</mi><mo>,</mo><mi>c</mi><mo>,</mo><mi>d</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi>g</mi><mo>,</mo><mi>h</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>=</mo><mi mathvariant="normal">trans</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>c</mi><mo>,</mo><mi>d</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi mathvariant="normal">trans</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo>,</mo><mi>c</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi>f</mi><mo>,</mo><mi>g</mi><mo stretchy="false">)</mo><mo>,</mo><mi>h</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\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)</annotation></semantics></math></div></li> <li> <p>for every vertex <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∈</mo><msub><mi>V</mi> <mi>G</mi></msub></mrow><annotation encoding="application/x-tex">a \in V_G</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi><mo>∈</mo><msub><mi>V</mi> <mi>G</mi></msub></mrow><annotation encoding="application/x-tex">b \in V_G</annotation></semantics></math> and edge <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>∈</mo><msub><mi>E</mi> <mi>G</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f \in E_G(a, b)</annotation></semantics></math></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">trans</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi>f</mi><mo>,</mo><mi mathvariant="normal">refl</mi><mo stretchy="false">(</mo><mi>b</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>=</mo><mi>f</mi></mrow><annotation encoding="application/x-tex">\mathrm{trans}(a, b, b)(f, \mathrm{refl}(b)) = f</annotation></semantics></math></div></li> <li> <p>for every vertex <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∈</mo><msub><mi>V</mi> <mi>G</mi></msub></mrow><annotation encoding="application/x-tex">a \in V_G</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi><mo>∈</mo><msub><mi>V</mi> <mi>G</mi></msub></mrow><annotation encoding="application/x-tex">b \in V_G</annotation></semantics></math> and edge <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>∈</mo><msub><mi>E</mi> <mi>G</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f \in E_G(a, b)</annotation></semantics></math></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">trans</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi mathvariant="normal">refl</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo><mo>,</mo><mi>f</mi><mo stretchy="false">)</mo><mo>=</mo><mi>f</mi></mrow><annotation encoding="application/x-tex">\mathrm{trans}(a, a, b)(\mathrm{refl}(a), f) = f</annotation></semantics></math></div></li> <li> <p>for every vertex <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∈</mo><msub><mi>V</mi> <mi>G</mi></msub></mrow><annotation encoding="application/x-tex">a \in V_G</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi><mo>∈</mo><msub><mi>V</mi> <mi>G</mi></msub></mrow><annotation encoding="application/x-tex">b \in V_G</annotation></semantics></math> and edge <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>∈</mo><msub><mi>E</mi> <mi>G</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f \in E_G(a, b)</annotation></semantics></math></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">trans</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo>,</mo><mi>a</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi>f</mi><mo>,</mo><mi mathvariant="normal">sym</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>=</mo><mi mathvariant="normal">refl</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathrm{trans}(a, b, a)(f, \mathrm{sym}(a, b)(f)) = \mathrm{refl}(a)</annotation></semantics></math></div></li> <li> <p>for every vertex <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∈</mo><msub><mi>V</mi> <mi>G</mi></msub></mrow><annotation encoding="application/x-tex">a \in V_G</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi><mo>∈</mo><msub><mi>V</mi> <mi>G</mi></msub></mrow><annotation encoding="application/x-tex">b \in V_G</annotation></semantics></math> and edge <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><msub><mi>E</mi> <mi>G</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f:E_G(a, b)</annotation></semantics></math></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">trans</mi><mo stretchy="false">(</mo><mi>b</mi><mo>,</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi mathvariant="normal">sym</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo>,</mo><mi>f</mi><mo stretchy="false">)</mo><mo>=</mo><mi mathvariant="normal">refl</mi><mo stretchy="false">(</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathrm{trans}(b, a, b)(\mathrm{sym}(a, b)(f), f) = \mathrm{refl}(b)</annotation></semantics></math></div></li> </ul> <p>Every pseudo-equivalence relation has at least one subgroupoid given by only the <a class="existingWikiWord" href="/nlab/show/identity+morphisms">identity morphisms</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">refl</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo><mo>:</mo><msub><mi>E</mi> <mi>A</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>a</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathrm{refl}(a):E_A(a, a)</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>. A subgroupoid <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>G</mi></mrow><annotation encoding="application/x-tex">G</annotation></semantics></math> of a pseudo-equivalence relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> is a maximal subgroupoid if the dagger functor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><mi>G</mi><mo>→</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">f:G \to A</annotation></semantics></math> is bijective-on-objects, and additionally if, for every other subgroupoid <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>H</mi></mrow><annotation encoding="application/x-tex">H</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> with faithful injective-on-objects dagger functor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>g</mi><mo>:</mo><mi>H</mi><mo>→</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">g:H \to A</annotation></semantics></math>, there is a unique faithful injective-on-objects dagger functor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>h</mi><mo>:</mo><mi>H</mi><mo>→</mo><mi>G</mi></mrow><annotation encoding="application/x-tex">h:H \to G</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>h</mi><mo>∘</mo><mi>f</mi><mo>=</mo><mi>g</mi></mrow><annotation encoding="application/x-tex">h \circ f = g</annotation></semantics></math>.</p> <h2 id="category_of_pseudoequivalence_relations">Category of pseudo-equivalence relations</h2> <p>Let the category <a class="existingWikiWord" href="/nlab/show/Set"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"> <semantics> <mrow> <mi>Set</mi> </mrow> <annotation encoding="application/x-tex">Set</annotation> </semantics> </math></a> be defined as a <a class="existingWikiWord" href="/nlab/show/category">category</a> that is <a class="existingWikiWord" href="/nlab/show/finitely+complete+category">finitely complete</a> and <a class="existingWikiWord" href="/nlab/show/well-pointed+category">well-pointed</a> (i.e. whose <a class="existingWikiWord" href="/nlab/show/terminal+object">terminal object</a> is a <a class="existingWikiWord" href="/nlab/show/extremal+epimorphism">extremal</a> <a class="existingWikiWord" href="/nlab/show/separator">generating object</a>). This category of sets is not even a <a class="existingWikiWord" href="/nlab/show/regular+category">regular category</a>, let alone an <a class="existingWikiWord" href="/nlab/show/exact+category">exact category</a>, as can happen in certain <a class="existingWikiWord" href="/nlab/show/foundations+of+mathematics">foundations of mathematics</a>, such as bare <a class="existingWikiWord" href="/nlab/show/set-level+type+theory">set-level</a> <a class="existingWikiWord" href="/nlab/show/Martin-L%C3%B6f+type+theory">Martin-Löf type theory</a>, or <a class="existingWikiWord" href="/nlab/show/ZFC">ZFC</a> and <a class="existingWikiWord" href="/nlab/show/ETCS">ETCS</a> without the <a class="existingWikiWord" href="/nlab/show/powerset">powerset</a> <a class="existingWikiWord" href="/nlab/show/axiom">axiom</a>. The category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">PseudoEquivRel</mi></mrow><annotation encoding="application/x-tex">\mathrm{PseudoEquivRel}</annotation></semantics></math> of sets with pseudo-equivalence relations is then the <a class="existingWikiWord" href="/nlab/show/exact+completion">ex/lex completion</a> of Set.</p> <p>More specifically, using the definition of pseudo-equivalence relation with two sets: if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><msub><mi>s</mi> <mi>R</mi></msub><mo>,</mo><msub><mi>t</mi> <mi>R</mi></msub><mo stretchy="false">)</mo><mo>:</mo><mi>R</mi><mo>⇉</mo><mi>X</mi></mrow><annotation encoding="application/x-tex">(s_R, t_R):R\rightrightarrows X</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><msub><mi>s</mi> <mi>S</mi></msub><mo>,</mo><msub><mi>t</mi> <mi>S</mi></msub><mo stretchy="false">)</mo><mo>:</mo><mi>S</mi><mo>⇉</mo><mi>Y</mi></mrow><annotation encoding="application/x-tex">(s_S, t_S):S\rightrightarrows Y</annotation></semantics></math> are two pseudo-equivalence relations, a morphism between them in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">PseudoEquivRel</mi></mrow><annotation encoding="application/x-tex">\mathrm{PseudoEquivRel}</annotation></semantics></math> is defined to be a function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><mi>X</mi><mo>→</mo><mi>Y</mi></mrow><annotation encoding="application/x-tex">f:X\to Y</annotation></semantics></math> with functions <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>f</mi> <mn>1</mn></msub><mo>:</mo><mi>R</mi><mo>→</mo><mi>S</mi></mrow><annotation encoding="application/x-tex">f_1:R \to S</annotation></semantics></math> with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>s</mi> <mi>S</mi></msub><mo>∘</mo><msub><mi>f</mi> <mn>1</mn></msub><mo>=</mo><mi>f</mi><mo>∘</mo><msub><mi>s</mi> <mi>R</mi></msub></mrow><annotation encoding="application/x-tex">s_S \circ f_1 = f \circ s_R</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>t</mi> <mi>S</mi></msub><mo>∘</mo><msub><mi>f</mi> <mn>1</mn></msub><mo>=</mo><mi>f</mi><mo>∘</mo><msub><mi>t</mi> <mi>R</mi></msub></mrow><annotation encoding="application/x-tex">t_S \circ f_1 = f \circ t_R</annotation></semantics></math>. Moreover, we declare two such functions <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>,</mo><mi>g</mi><mo>:</mo><mi>X</mi><mo>→</mo><mi>Y</mi></mrow><annotation encoding="application/x-tex">f,g:X\to Y</annotation></semantics></math> to be <em>equal</em> if there exists a function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>h</mi><mo>:</mo><mi>X</mi><mo>→</mo><mi>S</mi></mrow><annotation encoding="application/x-tex">h:X\to S</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi><mo>∘</mo><mi>h</mi><mo>=</mo><mi>f</mi></mrow><annotation encoding="application/x-tex">s \circ h = f</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>t</mi><mo>∘</mo><mi>h</mi><mo>=</mo><mi>g</mi></mrow><annotation encoding="application/x-tex">t \circ h = g</annotation></semantics></math>. Because <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><msub><mi>s</mi> <mi>S</mi></msub><mo>,</mo><msub><mi>t</mi> <mi>S</mi></msub><mo stretchy="false">)</mo><mo>:</mo><mi>S</mi><mo>⇉</mo><mi>Y</mi></mrow><annotation encoding="application/x-tex">(s_S, t_S):S\rightrightarrows Y</annotation></semantics></math> is a pseudo-equivalence relation, this defines an actual <a class="existingWikiWord" href="/nlab/show/equivalence+relation">equivalence relation</a> on the morphisms <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><mi>X</mi><mo>→</mo><mi>Y</mi></mrow><annotation encoding="application/x-tex">f:X\to Y</annotation></semantics></math>, which is compatible with composition; thus we have a well-defined category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">PseudoEquivRel</mi></mrow><annotation encoding="application/x-tex">\mathrm{PseudoEquivRel}</annotation></semantics></math> of pseudo-equivalence relations, which is the ex/lex completion of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math>.</p> <p>We have a <a class="existingWikiWord" href="/nlab/show/full+and+faithful+functor">full and faithful functor</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi><mo>→</mo><mi mathvariant="normal">PseudoEquivRel</mi></mrow><annotation encoding="application/x-tex">Set\to \mathrm{PseudoEquivRel}</annotation></semantics></math> sending an object <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> to the pseudo-equivalence relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><msub><mi>s</mi> <mi>X</mi></msub><mo>,</mo><msub><mi>t</mi> <mi>X</mi></msub><mo stretchy="false">)</mo><mo>:</mo><mi>X</mi><mo>⇉</mo><mi>X</mi></mrow><annotation encoding="application/x-tex">(s_X, t_X):X\rightrightarrows X</annotation></semantics></math>. One can then verify directly that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">PseudoEquivRel</mi></mrow><annotation encoding="application/x-tex">\mathrm{PseudoEquivRel}</annotation></semantics></math> is exact, that this embedding preserves finite limits, and that it is universal with respect to lex functors from <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> into exact categories.</p> <p>If the <a class="existingWikiWord" href="/nlab/show/presentation+axiom">presentation axiom</a> (a weak form of the full axiom of choice) holds in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math>, as a subcategory of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">PseudoEquivRel</mi></mrow><annotation encoding="application/x-tex">\mathrm{PseudoEquivRel}</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> could be thought of as the category of <a class="existingWikiWord" href="/nlab/show/completely+presented+sets">completely presented sets</a>, the category of sets with a <a class="existingWikiWord" href="/nlab/show/projective+presentation">projective presentation</a>. If the <a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a> holds in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> is equivalent to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">PseudoEquivRel</mi></mrow><annotation encoding="application/x-tex">\mathrm{PseudoEquivRel}</annotation></semantics></math>, as the axiom of choice implies that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> is its own free exact completion, and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> is equivalent to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">PseudoEquivRel</mi></mrow><annotation encoding="application/x-tex">\mathrm{PseudoEquivRel}</annotation></semantics></math> because the free functor from <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">PseudoEquivRel</mi></mrow><annotation encoding="application/x-tex">\mathrm{PseudoEquivRel}</annotation></semantics></math> is an <a class="existingWikiWord" href="/nlab/show/equivalence+of+categories">equivalence of categories</a>.</p> <p>This construction could be generalized to any <a class="existingWikiWord" href="/nlab/show/finitely+complete+category">finitely complete category</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math>, from which the category of <a class="existingWikiWord" href="/nlab/show/internal+pseudo-equivalence+relations">internal pseudo-equivalence relations</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> is the <a class="existingWikiWord" href="/nlab/show/ex%2Flex+completion">ex/lex completion</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math>, and denoted as <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>C</mi> <mrow><mi>ex</mi><mo stretchy="false">/</mo><mi>lex</mi></mrow></msub></mrow><annotation encoding="application/x-tex">C_{ex/lex}</annotation></semantics></math>. If every <a class="existingWikiWord" href="/nlab/show/epimorphism">epimorphism</a> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> is additionally a <a class="existingWikiWord" href="/nlab/show/split+epimorphism">split epimorphism</a>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> is its own free exact completion.</p> <h2 id="in_type_theory">In type theory</h2> <p>Many <a class="existingWikiWord" href="/nlab/show/set-level+type+theories">set-level type theories</a> use <a class="existingWikiWord" href="/nlab/show/type">types</a> which are <a class="existingWikiWord" href="/nlab/show/0-truncated">0-truncated</a> and thus <a class="existingWikiWord" href="/nlab/show/h-sets">h-sets</a> by default because of the inclusion of <a class="existingWikiWord" href="/nlab/show/uniqueness+of+identity+proofs">uniqueness of identity proofs</a> or <a class="existingWikiWord" href="/nlab/show/axiom+K">axiom K</a> to the rule system of the type theory. Sometimes, these type theories do not have <a class="existingWikiWord" href="/nlab/show/quotient+set">quotients</a> and <a class="existingWikiWord" href="/nlab/show/image+factorizations">image factorizations</a>, and as a result, setoids are used instead of the native h-sets.</p> <p>In <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a>, and more generally in any <a class="existingWikiWord" href="/nlab/show/intensional+type+theory">intensional type theory</a> where not all types are <a class="existingWikiWord" href="/nlab/show/h-sets">h-sets</a>, such as in a type theory without <a class="existingWikiWord" href="/nlab/show/uniqueness+of+identity+proofs">uniqueness of identity proofs</a> or <a class="existingWikiWord" href="/nlab/show/axiom+K">axiom K</a>, the notion of “setoid” bifurcates into multiple distinct notions. In analogy with <a class="existingWikiWord" href="/nlab/show/category">category</a>, the definitions used above in this article could be called a <strong>strict setoid</strong>. When the vertex types are only required to be a <a class="existingWikiWord" href="/nlab/show/type">type</a> rather than a <a class="existingWikiWord" href="/nlab/show/set">set</a>, then this defines a <strong><a class="existingWikiWord" href="/nlab/show/presetoid">presetoid</a></strong>. There is also the notion of a <strong><a class="existingWikiWord" href="/nlab/show/univalent+setoid">univalent setoid</a></strong>, where equality of vertices is isomorphism of vertices in the core of a presetoid.</p> <h2 id="related_concepts"> Related concepts</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Bishop+set">Bishop set</a>, <a class="existingWikiWord" href="/nlab/show/setoid">setoid</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/completely+presented+set">completely presented set</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/equivalence+relation">equivalence relation</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/quotient+type">quotient type</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/directed+graph">directed graph</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/pseudo-proset">pseudo-proset</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/ex%2Flex+completion">ex/lex completion</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/homotopy+exact+completion">homotopy exact completion</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/extensional+function">extensional function</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/dagger+functor">dagger functor</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/presetoid">presetoid</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/univalent+setoid">univalent setoid</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/internal+pseudo-equivalence+relation">internal pseudo-equivalence relation</a></p> </li> </ul> <div> <table><thead><tr><th><a class="existingWikiWord" href="/nlab/show/algebra">algebraic</a> <a class="existingWikiWord" href="/nlab/show/mathematical+structure">structure</a></th><th><a class="existingWikiWord" href="/nlab/show/oidification">oidification</a></th></tr></thead><tbody><tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/magma">magma</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/magmoid">magmoid</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/pointed+set">pointed</a> <a class="existingWikiWord" href="/nlab/show/magma">magma</a> with an <a class="existingWikiWord" href="/nlab/show/endofunction">endofunction</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/setoid">setoid</a>/<a class="existingWikiWord" href="/nlab/show/Bishop+set">Bishop set</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/unital+magma">unital magma</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/unital+magmoid">unital magmoid</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/quasigroup">quasigroup</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/quasigroupoid">quasigroupoid</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/loop+%28algebra%29">loop</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/loopoid">loopoid</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/semigroup">semigroup</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/semicategory">semicategory</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/monoid">monoid</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/category">category</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/anti-involution">anti-involutive</a> <a class="existingWikiWord" href="/nlab/show/monoid">monoid</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/dagger+category">dagger category</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/associative+quasigroup">associative quasigroup</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/associative+quasigroupoid">associative quasigroupoid</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/group">group</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/groupoid">groupoid</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/flexible+magma">flexible magma</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/flexible+magmoid">flexible magmoid</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/alternative+magma">alternative magma</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/alternative+magmoid">alternative magmoid</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/absorption+monoid">absorption monoid</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/absorption+category">absorption category</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/cancellative+monoid">cancellative monoid</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/cancellative+category">cancellative category</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/rig">rig</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/CMon">CMon</a>-<a class="existingWikiWord" href="/nlab/show/enriched+category">enriched category</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/nonunital+ring">nonunital ring</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/Ab">Ab</a>-<a class="existingWikiWord" href="/nlab/show/enriched+magmoid">enriched</a> <a class="existingWikiWord" href="/nlab/show/semicategory">semicategory</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/nonassociative+ring">nonassociative ring</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/Ab">Ab</a>-<a class="existingWikiWord" href="/nlab/show/enriched+magmoid">enriched</a> <a class="existingWikiWord" href="/nlab/show/unital+magmoid">unital magmoid</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/ring">ring</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/ringoid">ringoid</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/nonassociative+algebra">nonassociative algebra</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/linear+magmoid">linear magmoid</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/nonassociative+algebra">nonassociative unital algebra</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/unital+magmoid">unital</a> <a class="existingWikiWord" href="/nlab/show/linear+magmoid">linear magmoid</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/nonunital+algebra">nonunital algebra</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/linear+magmoid">linear</a> <a class="existingWikiWord" href="/nlab/show/semicategory">semicategory</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/associative+unital+algebra">associative unital algebra</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/linear+category">linear category</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/C-star+algebra">C-star algebra</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/C-star+category">C-star category</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/differential+algebra">differential algebra</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/differential+algebroid">differential algebroid</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/flexible+algebra">flexible algebra</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/flexible+magmoid">flexible</a> <a class="existingWikiWord" href="/nlab/show/linear+magmoid">linear magmoid</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/alternative+algebra">alternative algebra</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/alternative+magmoid">alternative</a> <a class="existingWikiWord" href="/nlab/show/linear+magmoid">linear magmoid</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/Lie+algebra">Lie algebra</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/Lie+algebroid">Lie algebroid</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/monoidal+poset">monoidal poset</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/2-poset">2-poset</a></td></tr> <tr><td style="text-align: left;"><span class="newWikiWord">strict monoidal groupoid<a href="/nlab/new/strict+monoidal+groupoid">?</a></span></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/strict+%282%2C1%29-category">strict (2,1)-category</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/strict+2-group">strict 2-group</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/strict+2-groupoid">strict 2-groupoid</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/strict+monoidal+category">strict monoidal category</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/strict+2-category">strict 2-category</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/monoidal+groupoid">monoidal groupoid</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/%282%2C1%29-category">(2,1)-category</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/2-group">2-group</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/2-groupoid">2-groupoid</a>/<a class="existingWikiWord" href="/nlab/show/bigroupoid">bigroupoid</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/monoidal+category">monoidal category</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/2-category">2-category</a>/<a class="existingWikiWord" href="/nlab/show/bicategory">bicategory</a></td></tr> </tbody></table> </div><div> <p><strong><a class="existingWikiWord" href="/nlab/show/computational+trinitarianism">computational trinitarianism</a></strong> = <br /> <strong><a class="existingWikiWord" href="/nlab/show/propositions+as+types">propositions as types</a></strong> +<strong><a class="existingWikiWord" href="/nlab/show/programs+as+proofs">programs as proofs</a></strong> +<strong><a class="existingWikiWord" href="/nlab/show/relation+between+type+theory+and+category+theory">relation type theory/category theory</a></strong></p> <table><thead><tr><th><a class="existingWikiWord" href="/nlab/show/logic">logic</a></th><th><a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a> (<a class="existingWikiWord" href="/nlab/show/internal+logic+of+set+theory">internal logic</a> of)</th><th><a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a></th><th><a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a></th></tr></thead><tbody><tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/proposition">proposition</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/set">set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/object">object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/type">type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/predicate">predicate</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/family+of+sets">family of sets</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/display+morphism">display morphism</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/dependent+type">dependent type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/proof">proof</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/element">element</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/generalized+element">generalized element</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/term">term</a>/<a class="existingWikiWord" href="/nlab/show/program">program</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/cut+rule">cut rule</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/composition">composition</a> of <a class="existingWikiWord" href="/nlab/show/classifying+morphisms">classifying morphisms</a> / <a class="existingWikiWord" href="/nlab/show/pullback">pullback</a> of <a class="existingWikiWord" href="/nlab/show/display+maps">display maps</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/substitution">substitution</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/introduction+rule">introduction rule</a> for <a class="existingWikiWord" href="/nlab/show/implication">implication</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/counit">counit</a> for hom-tensor adjunction</td><td style="text-align: left;">lambda</td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/elimination+rule">elimination rule</a> for <a class="existingWikiWord" href="/nlab/show/implication">implication</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/unit">unit</a> for hom-tensor adjunction</td><td style="text-align: left;">application</td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/cut+elimination">cut elimination</a> for <a class="existingWikiWord" href="/nlab/show/implication">implication</a></td><td style="text-align: left;"></td><td style="text-align: left;">one of the <a class="existingWikiWord" href="/nlab/show/zigzag+identities">zigzag identities</a> for hom-tensor adjunction</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/beta+reduction">beta reduction</a></td></tr> <tr><td style="text-align: left;">identity elimination for <a class="existingWikiWord" href="/nlab/show/implication">implication</a></td><td style="text-align: left;"></td><td style="text-align: left;">the other <a class="existingWikiWord" href="/nlab/show/zigzag+identity">zigzag identity</a> for hom-tensor adjunction</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/eta+conversion">eta conversion</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/true">true</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/singleton">singleton</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/terminal+object">terminal object</a>/<a class="existingWikiWord" href="/nlab/show/%28-2%29-truncated+object">(-2)-truncated object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/h-level+0">h-level 0</a>-<a class="existingWikiWord" href="/nlab/show/type">type</a>/<a class="existingWikiWord" href="/nlab/show/unit+type">unit type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/false">false</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/empty+set">empty set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/initial+object">initial object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/empty+type">empty type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/proposition">proposition</a>, <a class="existingWikiWord" href="/nlab/show/truth+value">truth value</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/subsingleton">subsingleton</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/subterminal+object">subterminal object</a>/<a class="existingWikiWord" href="/nlab/show/%28-1%29-truncated+object">(-1)-truncated object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/h-proposition">h-proposition</a>, <a class="existingWikiWord" href="/nlab/show/mere+proposition">mere proposition</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/logical+conjunction">logical conjunction</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/cartesian+product">cartesian product</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/product">product</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/product+type">product type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/disjunction">disjunction</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/disjoint+union">disjoint union</a> (<a class="existingWikiWord" href="/nlab/show/support">support</a> of)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/coproduct">coproduct</a> (<a class="existingWikiWord" href="/nlab/show/%28-1%29-truncation">(-1)-truncation</a> of)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/sum+type">sum type</a> (<a class="existingWikiWord" href="/nlab/show/bracket+type">bracket type</a> of)</td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/implication">implication</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/function+set">function set</a> (into <a class="existingWikiWord" href="/nlab/show/subsingleton">subsingleton</a>)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/internal+hom">internal hom</a> (into <a class="existingWikiWord" href="/nlab/show/subterminal+object">subterminal object</a>)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/function+type">function type</a> (into <a class="existingWikiWord" href="/nlab/show/h-proposition">h-proposition</a>)</td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/negation">negation</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/function+set">function set</a> into <a class="existingWikiWord" href="/nlab/show/empty+set">empty set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/internal+hom">internal hom</a> into <a class="existingWikiWord" href="/nlab/show/initial+object">initial object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/function+type">function type</a> into <a class="existingWikiWord" href="/nlab/show/empty+type">empty type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/universal+quantification">universal quantification</a></td><td style="text-align: left;">indexed <a class="existingWikiWord" href="/nlab/show/cartesian+product">cartesian product</a> (of family of <a class="existingWikiWord" href="/nlab/show/subsingletons">subsingletons</a>)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/dependent+product">dependent product</a> (of family of <a class="existingWikiWord" href="/nlab/show/subterminal+objects">subterminal objects</a>)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/dependent+product+type">dependent product type</a> (of family of <a class="existingWikiWord" href="/nlab/show/h-propositions">h-propositions</a>)</td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/existential+quantification">existential quantification</a></td><td style="text-align: left;">indexed <a class="existingWikiWord" href="/nlab/show/disjoint+union">disjoint union</a> (<a class="existingWikiWord" href="/nlab/show/support">support</a> of)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/dependent+sum">dependent sum</a> (<a class="existingWikiWord" href="/nlab/show/%28-1%29-truncation">(-1)-truncation</a> of)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/dependent+sum+type">dependent sum type</a> (<a class="existingWikiWord" href="/nlab/show/bracket+type">bracket type</a> of)</td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/logical+equivalence">logical equivalence</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/bijection+set">bijection set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/object+of+isomorphisms">object of isomorphisms</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/equivalence+type">equivalence type</a></td></tr> <tr><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/support+set">support set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/support+object">support object</a>/<a class="existingWikiWord" href="/nlab/show/%28-1%29-truncation">(-1)-truncation</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/propositional+truncation">propositional truncation</a>/<a class="existingWikiWord" href="/nlab/show/bracket+type">bracket type</a></td></tr> <tr><td style="text-align: left;"></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/n-image">n-image</a> of <a class="existingWikiWord" href="/nlab/show/morphism">morphism</a> into <a class="existingWikiWord" href="/nlab/show/terminal+object">terminal object</a>/<a class="existingWikiWord" href="/nlab/show/n-truncation">n-truncation</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/n-truncation+modality">n-truncation modality</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/equality">equality</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/diagonal+function">diagonal function</a>/<a class="existingWikiWord" href="/nlab/show/diagonal+subset">diagonal subset</a>/<a class="existingWikiWord" href="/nlab/show/diagonal+relation">diagonal relation</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/path+space+object">path space object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/identity+type">identity type</a>/<a class="existingWikiWord" href="/nlab/show/path+type">path type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/completely+presented+set">completely presented set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/set">set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/discrete+object">discrete object</a>/<a class="existingWikiWord" href="/nlab/show/0-truncated+object">0-truncated object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/h-level+2">h-level 2</a>-<a class="existingWikiWord" href="/nlab/show/type">type</a>/<a class="existingWikiWord" href="/nlab/show/set">set</a>/<a class="existingWikiWord" href="/nlab/show/h-set">h-set</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/set">set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/set">set</a> with <a class="existingWikiWord" href="/nlab/show/equivalence+relation">equivalence relation</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/groupoid+object+in+an+%28infinity%2C1%29-category">internal 0-groupoid</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/Bishop+set">Bishop set</a>/<a class="existingWikiWord" href="/nlab/show/setoid">setoid</a> with its <a class="existingWikiWord" href="/nlab/show/pseudo-equivalence+relation">pseudo-equivalence relation</a> an actual <a class="existingWikiWord" href="/nlab/show/equivalence+relation">equivalence relation</a></td></tr> <tr><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/equivalence+class">equivalence class</a>/<a class="existingWikiWord" href="/nlab/show/quotient+set">quotient set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/quotient">quotient</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/quotient+type">quotient type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/induction">induction</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/colimit">colimit</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/inductive+type">inductive type</a>, <a class="existingWikiWord" href="/nlab/show/W-type">W-type</a>, <a class="existingWikiWord" href="/nlab/show/M-type">M-type</a></td></tr> <tr><td style="text-align: left;">higher <a class="existingWikiWord" href="/nlab/show/induction">induction</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/%28infinity%2C1%29-colimit">higher colimit</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/higher+inductive+type">higher inductive type</a></td></tr> <tr><td style="text-align: left;">-</td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/0-truncated">0-truncated</a> <a class="existingWikiWord" href="/nlab/show/%28infinity%2C1%29-colimit">higher colimit</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/quotient+inductive+type">quotient inductive type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/coinduction">coinduction</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/limit">limit</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/coinductive+type">coinductive type</a></td></tr> <tr><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/preset">preset</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/type">type</a> without <a class="existingWikiWord" href="/nlab/show/identity+types">identity types</a></td></tr> <tr><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/set">set</a> of <a class="existingWikiWord" href="/nlab/show/truth+values">truth values</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/subobject+classifier">subobject classifier</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/type+of+propositions">type of propositions</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/domain+of+discourse">domain of discourse</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/universe">universe</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/object+classifier">object classifier</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/type+universe">type universe</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/modality">modality</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/closure+operator">closure operator</a>, (<a class="existingWikiWord" href="/nlab/show/idempotent+monad">idempotent</a>) <a class="existingWikiWord" href="/nlab/show/monad">monad</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/modal+type+theory">modal type theory</a>, <a class="existingWikiWord" href="/nlab/show/monad+%28in+computer+science%29">monad (in computer science)</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/linear+logic">linear logic</a></td><td style="text-align: left;"></td><td style="text-align: left;">(<a class="existingWikiWord" href="/nlab/show/symmetric+monoidal+category">symmetric</a>, <a class="existingWikiWord" href="/nlab/show/closed+monoidal+category">closed</a>) <a class="existingWikiWord" href="/nlab/show/monoidal+category">monoidal category</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/linear+type+theory">linear type theory</a>/<a class="existingWikiWord" href="/nlab/show/quantum+computation">quantum computation</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/proof+net">proof net</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/string+diagram">string diagram</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/quantum+circuit">quantum circuit</a></td></tr> <tr><td style="text-align: left;">(absence of) <a class="existingWikiWord" href="/nlab/show/contraction+rule">contraction rule</a></td><td style="text-align: left;"></td><td style="text-align: left;">(absence of) <a class="existingWikiWord" href="/nlab/show/diagonal">diagonal</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/no-cloning+theorem">no-cloning theorem</a></td></tr> <tr><td style="text-align: left;"></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/synthetic+mathematics">synthetic mathematics</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/domain+specific+embedded+programming+language">domain specific embedded programming language</a></td></tr> </tbody></table> </div> <h2 id="references">References</h2> <p>For setoids defined as a set with an pseudo-equivalence relation:</p> <ul> <li id="Wilander12"> <p><a class="existingWikiWord" href="/nlab/show/Olov+Wilander">Olov Wilander</a>, <em>Constructing a small category of setoids</em>, Mathematical Structures in Computer Science <strong>22</strong> 1 (2012) 103-121 [<a href="https://doi.org/10.1017/S0960129511000478">doi:10.1017/S0960129511000478</a>, <a href="http://www.diva-portal.org/smash/get/diva2:399799/FULLTEXT01.pdf">pdf</a>]</p> </li> <li id="PalmgrenWilander14"> <p><a class="existingWikiWord" href="/nlab/show/Erik+Palmgren">Erik Palmgren</a>, <a class="existingWikiWord" href="/nlab/show/Olov+Wilander">Olov Wilander</a>, <em>Constructing categories and setoids of setoids in type theory</em>, Logical Methods in Computer Science, <strong>10</strong> 3 (2014) lmcs:964 [<a href="https://arxiv.org/abs/1408.1364">arXiv:1408.1364</a>, <a href="https://doi.org/10.2168/LMCS-10(3:25)2014">doi:10.2168/LMCS-10(3:25)2014</a>]</p> </li> <li id="EmmeneggerPalmgren20"> <p><a class="existingWikiWord" href="/nlab/show/Jacopo+Emmenegger">Jacopo Emmenegger</a>, <a class="existingWikiWord" href="/nlab/show/Erik+Palmgren">Erik Palmgren</a>, <em>Exact completion and constructive theories of sets</em>, J. Symb. Log. <strong>85</strong> 2 (2020) [<a href="https://arxiv.org/abs/1710.10685">arXiv:1710.10685</a>, <a href="https://doi.org/10.1017/jsl.2020.2">doi:10.1017/jsl.2020.2</a>]</p> </li> <li id="Cipriano20"> <p>Cioffo Cipriano Junior, Def. 1.1.1 in: <em>Homotopy setoids and generalized quotient completion</em> [<a href="https://air.unimi.it/retrieve/d7ab68cc-fc12-4fe9-8a21-617deb888f36/phd_unimi_R12371.pdf">pdf</a>, <a class="existingWikiWord" href="/nlab/files/Cipriano-HomotopySetoids.pdf" title="pdf">pdf</a>]</p> </li> </ul> </body></html> </div> <div class="revisedby"> <p> Last revised on July 7, 2023 at 18:15:07. See the <a href="/nlab/history/pseudo-equivalence+relation" style="color: #005c19">history</a> of this page for a list of all contributions to it. </p> </div> <div class="navigation navfoot"> <a href="/nlab/edit/pseudo-equivalence+relation" accesskey="E" class="navlink" id="edit" rel="nofollow">Edit</a><a href="https://nforum.ncatlab.org/discussion/16710/#Item_1">Discuss</a><span class="backintime"><a href="/nlab/revision/pseudo-equivalence+relation/3" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/diff/pseudo-equivalence+relation" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Changes from previous revision</a><a href="/nlab/history/pseudo-equivalence+relation" accesskey="S" class="navlink" id="history" rel="nofollow">History (3 revisions)</a> <a href="/nlab/show/pseudo-equivalence+relation/cite" style="color: black">Cite</a> <a href="/nlab/print/pseudo-equivalence+relation" accesskey="p" id="view_print" rel="nofollow">Print</a> <a href="/nlab/source/pseudo-equivalence+relation" id="view_source" rel="nofollow">Source</a> </div> </div>  </div>  </body> </html>