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> setoid 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> setoid </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/12612/#Item_14" 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>Setoids</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="constructivism_realizability_computability">Constructivism, Realizability, Computability</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/constructive+mathematics">constructive mathematics</a></strong>, <strong><a class="existingWikiWord" href="/nlab/show/realizability">realizability</a></strong>, <strong><a class="existingWikiWord" href="/nlab/show/computability">computability</a></strong></p> <p><a class="existingWikiWord" href="/nlab/show/intuitionistic+mathematics">intuitionistic mathematics</a></p> <p><a class="existingWikiWord" href="/nlab/show/propositions+as+types">propositions as types</a>, <a class="existingWikiWord" href="/nlab/show/proofs+as+programs">proofs as programs</a>, <a class="existingWikiWord" href="/nlab/show/computational+trinitarianism">computational trinitarianism</a></p> <h3 id="constructive_mathematics">Constructive mathematics</h3> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/topos">topos</a>, <a class="existingWikiWord" href="/nlab/show/%28infinity%2C1%29-topos">homotopy topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a>, <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/canonical+form">canonical form</a>, <a class="existingWikiWord" href="/nlab/show/univalence">univalence</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Bishop+set">Bishop set</a>, <a class="existingWikiWord" href="/nlab/show/h-set">h-set</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/decidable+equality">decidable equality</a>, <a class="existingWikiWord" href="/nlab/show/decidable+subset">decidable subset</a>, <a class="existingWikiWord" href="/nlab/show/inhabited+set">inhabited set</a>, <a class="existingWikiWord" href="/nlab/show/subsingleton">subsingleton</a></p> </li> </ul> <h3 id="realizability">Realizability</h3> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/realizability+topos">realizability topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/realizability+model">realizability model</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/realizability+interpretation">realizability interpretation</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/effective+topos">effective topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Kleene%27s+first+algebra">Kleene's first algebra</a>, <a class="existingWikiWord" href="/nlab/show/Kleene%27s+second+algebra">Kleene's second algebra</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/function+realizability">function realizability</a></p> </li> </ul> <h3 id="computability">Computability</h3> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/computability">computability</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/computation">computation</a>, <a class="existingWikiWord" href="/nlab/show/computational+type+theory">computational type theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/computable+function">computable function</a>, <a class="existingWikiWord" href="/nlab/show/partial+recursive+function">partial recursive function</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/computable+analysis">computable analysis</a>, <a class="existingWikiWord" href="/nlab/show/constructive+analysis">constructive analysis</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Type+Two+Theory+of+Effectivity">Type Two Theory of Effectivity</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/computable+function+%28analysis%29">computable function (analysis)</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/exact+real+computer+arithmetic">exact real computer arithmetic</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/computable+set">computable set</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/persistent+homology">persistent homology</a>, <a class="existingWikiWord" href="/nlab/show/effective+homology">effective homology</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/computable+physics">computable physics</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Church-Turing+thesis">Church-Turing thesis</a></p> </li> </ul> </div></div> <h4 id="type_theory">Type theory</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/natural+deduction">natural deduction</a></strong> <a class="existingWikiWord" href="/nlab/show/metalanguage">metalanguage</a>, <a class="existingWikiWord" href="/nlab/show/practical+foundations">practical foundations</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/judgement">judgement</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/hypothetical+judgement">hypothetical judgement</a>, <a class="existingWikiWord" href="/nlab/show/sequent">sequent</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/antecedents">antecedents</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊢</mo></mrow><annotation encoding="application/x-tex">\vdash</annotation></semantics></math> <a class="existingWikiWord" href="/nlab/show/consequent">consequent</a>, <a class="existingWikiWord" href="/nlab/show/succedents">succedents</a></li> </ul> </li> </ul> <ol> <li><a class="existingWikiWord" href="/nlab/show/type+formation+rule">type formation rule</a></li> <li><a class="existingWikiWord" href="/nlab/show/term+introduction+rule">term introduction rule</a></li> <li><a class="existingWikiWord" href="/nlab/show/term+elimination+rule">term elimination rule</a></li> <li><a class="existingWikiWord" href="/nlab/show/computation+rule">computation rule</a></li> </ol> <p><strong><a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a></strong> (<a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent</a>, <a class="existingWikiWord" href="/nlab/show/intensional+type+theory">intensional</a>, <a class="existingWikiWord" href="/nlab/show/observational+type+theory">observational type theory</a>, <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a>)</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/calculus+of+constructions">calculus of constructions</a></li> </ul> <p><strong><a class="existingWikiWord" href="/nlab/show/syntax">syntax</a></strong> <a class="existingWikiWord" href="/nlab/show/object+language">object language</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/theory">theory</a>, <a class="existingWikiWord" href="/nlab/show/axiom">axiom</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/proposition">proposition</a>/<a class="existingWikiWord" href="/nlab/show/type">type</a> (<a class="existingWikiWord" href="/nlab/show/propositions+as+types">propositions as types</a>)</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/definition">definition</a>/<a class="existingWikiWord" href="/nlab/show/proof">proof</a>/<a class="existingWikiWord" href="/nlab/show/program">program</a> (<a class="existingWikiWord" href="/nlab/show/proofs+as+programs">proofs as programs</a>)</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/theorem">theorem</a></p> </li> </ul> <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> <p><strong><a class="existingWikiWord" href="/nlab/show/homotopy+levels">homotopy levels</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/2-type+theory">2-type theory</a>, <a class="existingWikiWord" href="/michaelshulman/show/2-categorical+logic">2-categorical logic</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a>, <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory+-+contents">homotopy type theory - contents</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/homotopy+type">homotopy type</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/univalence">univalence</a>, <a class="existingWikiWord" href="/nlab/show/function+extensionality">function extensionality</a>, <a class="existingWikiWord" href="/nlab/show/internal+logic+of+an+%28%E2%88%9E%2C1%29-topos">internal logic of an (∞,1)-topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/cohesive+homotopy+type+theory">cohesive homotopy type theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/directed+homotopy+type+theory">directed homotopy type theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/HoTT+methods+for+homotopy+theorists">HoTT methods for homotopy theorists</a></p> </li> </ul> </li> </ul> <p><strong><a class="existingWikiWord" href="/nlab/show/semantics">semantics</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/internal+logic">internal logic</a>, <a class="existingWikiWord" href="/nlab/show/categorical+semantics">categorical semantics</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/display+map">display map</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/internal+logic+of+a+topos">internal logic of a topos</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Mitchell-Benabou+language">Mitchell-Benabou language</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Kripke-Joyal+semantics">Kripke-Joyal semantics</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/internal+logic+of+an+%28%E2%88%9E%2C1%29-topos">internal logic of an (∞,1)-topos</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/type-theoretic+model+category">type-theoretic model category</a></li> </ul> </li> </ul> <div> <p> <a href="/nlab/edit/type+theory+-+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> <h4 id="foundations">Foundations</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/foundations">foundations</a></strong></p> <h2 id="the_basis_of_it_all">The basis of it all</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/mathematical+logic">mathematical logic</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/deduction+system">deduction system</a>, <a class="existingWikiWord" href="/nlab/show/natural+deduction">natural deduction</a>, <a class="existingWikiWord" href="/nlab/show/sequent+calculus">sequent calculus</a>, <a class="existingWikiWord" href="/nlab/show/lambda-calculus">lambda-calculus</a>, <a class="existingWikiWord" href="/nlab/show/judgment">judgment</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a>, <a class="existingWikiWord" href="/nlab/show/simple+type+theory">simple type theory</a>, <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/collection">collection</a>, <a class="existingWikiWord" href="/nlab/show/object">object</a>, <a class="existingWikiWord" href="/nlab/show/type">type</a>, <a class="existingWikiWord" href="/nlab/show/term">term</a>, <a class="existingWikiWord" href="/nlab/show/set">set</a>, <a class="existingWikiWord" href="/nlab/show/element">element</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/equality">equality</a>, <a class="existingWikiWord" href="/nlab/show/judgmental+equality">judgmental equality</a>, <a class="existingWikiWord" href="/nlab/show/typal+equality">typal equality</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/universe">universe</a>, <a class="existingWikiWord" href="/nlab/show/size+issues">size issues</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/higher-order+logic">higher-order logic</a></p> </li> </ul> <h2 id="set_theory"> Set theory</h2> <div> <p><strong><a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a></strong></p> <ul> <li>fundamentals of set theory <ul> <li><a class="existingWikiWord" href="/nlab/show/propositional+logic">propositional logic</a></li> <li><a class="existingWikiWord" href="/nlab/show/first-order+logic">first-order logic</a></li> <li><a class="existingWikiWord" href="/nlab/show/typed+predicate+logic">typed predicate logic</a></li> <li><a class="existingWikiWord" href="/nlab/show/membership+relation">membership relation</a></li> <li><a class="existingWikiWord" href="/nlab/show/propositional+equality">propositional equality</a></li> <li><a class="existingWikiWord" href="/nlab/show/set">set</a>, <a class="existingWikiWord" href="/nlab/show/element">element</a>, <a class="existingWikiWord" href="/nlab/show/function">function</a>, <a class="existingWikiWord" href="/nlab/show/relation">relation</a></li> <li><a class="existingWikiWord" href="/nlab/show/universe">universe</a>, <a class="existingWikiWord" href="/nlab/show/small+set">small set</a>, <a class="existingWikiWord" href="/nlab/show/large+set">large set</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/material+set+theory">material set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/membership+relation">membership relation</a>, <a class="existingWikiWord" href="/nlab/show/propositional+equality">propositional equality</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+extensionality">axiom of extensionality</a></li> <li><a class="existingWikiWord" href="/nlab/show/pairing+structure">pairing structure</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+pairing">axiom of pairing</a></li> <li><a class="existingWikiWord" href="/nlab/show/union+structure">union structure</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+union">axiom of union</a></li> <li><a class="existingWikiWord" href="/nlab/show/powerset+structure">powerset structure</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+power+sets">axiom of power sets</a></li> <li><a class="existingWikiWord" href="/nlab/show/natural+numbers+structure">natural numbers structure</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+infinity">axiom of infinity</a></li> </ul> </li> <li>presentations of set theory <ul> <li><a class="existingWikiWord" href="/nlab/show/first-order+set+theory">first-order set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/unsorted+set+theory">unsorted set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/simply+sorted+set+theory">simply sorted set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/one-sorted+set+theory">one-sorted set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/two-sorted+set+theory">two-sorted set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/three-sorted+set+theory">three-sorted set theory</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/dependently+sorted+set+theory">dependently sorted set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/structurally+presented+set+theory">structurally presented set theory</a></li> </ul> </li> <li>structuralism in set theory <ul> <li><a class="existingWikiWord" href="/nlab/show/material+set+theory">material set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/ZFC">ZFC</a></li> <li><a class="existingWikiWord" href="/nlab/show/ZFA">ZFA</a></li> <li><a class="existingWikiWord" href="/nlab/show/Mostowski+set+theory">Mostowski set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/New+Foundations">New Foundations</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/structural+set+theory">structural set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/categorical+set+theory">categorical set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/ETCS">ETCS</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/fully+formal+ETCS">fully formal ETCS</a></li> <li><a class="existingWikiWord" href="/nlab/show/ETCS+with+elements">ETCS with elements</a></li> <li><a class="existingWikiWord" href="/nlab/show/Trimble+on+ETCS+I">Trimble on ETCS I</a></li> <li><a class="existingWikiWord" href="/nlab/show/Trimble+on+ETCS+II">Trimble on ETCS II</a></li> <li><a class="existingWikiWord" href="/nlab/show/Trimble+on+ETCS+III">Trimble on ETCS III</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/structural+ZFC">structural ZFC</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/allegorical+set+theory">allegorical set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/SEAR">SEAR</a></li> </ul> </li> </ul> </li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/class-set+theory">class-set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/class">class</a>, <a class="existingWikiWord" href="/nlab/show/proper+class">proper class</a></li> <li><a class="existingWikiWord" href="/nlab/show/universal+class">universal class</a>, <a class="existingWikiWord" href="/nlab/show/universe">universe</a></li> <li><a class="existingWikiWord" href="/nlab/show/category+of+classes">category of classes</a></li> <li><a class="existingWikiWord" href="/nlab/show/category+with+class+structure">category with class structure</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/constructive+set+theory">constructive set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/algebraic+set+theory">algebraic set theory</a></li> </ul> </div> <h2 id="foundational_axioms">Foundational axioms</h2> <div> <p><strong><a class="existingWikiWord" href="/nlab/show/foundational+axiom">foundational</a> <a class="existingWikiWord" href="/nlab/show/axioms">axioms</a></strong></p> <ul> <li> <p>basic constructions:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+cartesian+products">axiom of cartesian products</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+disjoint+unions">axiom of disjoint unions</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+the+empty+set">axiom of the empty set</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+fullness">axiom of fullness</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+function+sets">axiom of function sets</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+power+sets">axiom of power sets</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+quotient+sets">axiom of quotient sets</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/material+set+theory">material axioms</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+extensionality">axiom of extensionality</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+foundation">axiom of foundation</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+anti-foundation">axiom of anti-foundation</a></li> <li><a class="existingWikiWord" href="/nlab/show/Mostowski%27s+axiom">Mostowski's axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+pairing">axiom of pairing</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+transitive+closure">axiom of transitive closure</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+union">axiom of union</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/structural+set+theory">structural axioms</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+materialization">axiom of materialization</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/type+theory">type theoretic axioms</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axioms+of+set+truncation">axioms of set truncation</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/uniqueness+of+identity+proofs">uniqueness of identity proofs</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+K">axiom K</a></li> <li><a class="existingWikiWord" href="/nlab/show/boundary+separation">boundary separation</a></li> <li><a class="existingWikiWord" href="/nlab/show/equality+reflection">equality reflection</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+circle+type+localization">axiom of circle type localization</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theoretic axioms</a>: <ul> <li><a class="existingWikiWord" href="/nlab/show/univalence+axiom">univalence axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/Whitehead%27s+principle">Whitehead's principle</a></li> </ul> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/axioms+of+choice">axioms of choice</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+countable+choice">axiom of countable choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+dependent+choice">axiom of dependent choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+excluded+middle">axiom of excluded middle</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+existence">axiom of existence</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+multiple+choice">axiom of multiple choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/Markov%27s+axiom">Markov's axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/presentation+axiom">presentation axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/small+cardinality+selection+axiom">small cardinality selection axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+small+violations+of+choice">axiom of small violations of choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+weakly+initial+sets+of+covers">axiom of weakly initial sets of covers</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/large+cardinal+axioms">large cardinal axioms</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+infinity">axiom of infinity</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+universes">axiom of universes</a></li> <li><a class="existingWikiWord" href="/nlab/show/regular+extension+axiom">regular extension axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/inaccessible+cardinal">inaccessible cardinal</a></li> <li><a class="existingWikiWord" href="/nlab/show/measurable+cardinal">measurable cardinal</a></li> <li><a class="existingWikiWord" href="/nlab/show/elementary+embedding">elementary embedding</a></li> <li><a class="existingWikiWord" href="/nlab/show/supercompact+cardinal">supercompact cardinal</a></li> <li><a class="existingWikiWord" href="/nlab/show/Vop%C4%9Bnka%27s+principle">Vopěnka's principle</a></li> </ul> </li> <li> <p>strong axioms</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+separation">axiom of separation</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+replacement">axiom of replacement</a></li> </ul> </li> <li> <p>further</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/reflection+principle">reflection principle</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/axiom+of+inequality+spaces">axiom of inequality spaces</a></p> </li> </ul> </div> <h2 id="removing_axioms">Removing axioms</h2> <ul> <li><a class="existingWikiWord" href="/nlab/show/constructive+mathematics">constructive mathematics</a></li> <li><a class="existingWikiWord" href="/nlab/show/predicative+mathematics">predicative mathematics</a></li> </ul> <div> <p> <a href="/nlab/edit/foundations+-+contents">Edit this sidebar</a> </p> </div></div></div> </div> </div> <h1 id="setoids">Setoids</h1> <div class='maruku_toc'> <ul> <li><a href='#Disambiguation'>Disambiguation</a></li> <li><a href='#applications'>Applications</a></li> <li><a href='#fixing_inadequate_foundations'>Fixing inadequate foundations</a></li> <li><a href='#related_concepts'>Related concepts</a></li> <li><a href='#references'>References</a></li> </ul> </div> <h2 id="Disambiguation">Disambiguation</h2> <p>In <a class="existingWikiWord" href="/nlab/show/constructive+mathematics">constructive mathematics</a>, such as in <a class="existingWikiWord" href="/nlab/show/intuitionistic+type+theory">intuitionistic type theory</a>, the notion of <em>setoids</em> [<a href="#Hofmann95">Hofmann (1995)</a>] is a formalization of the idea of <em><a class="existingWikiWord" href="/nlab/show/Bishop+sets">Bishop sets</a></em> (following <a href="#Bishop67">Bishop (1967)</a>) and serves as a way of “constructively” speaking about <a class="existingWikiWord" href="/nlab/show/quotient+sets">quotient sets</a> without, in a sense, actually constructing these: A setoid is essentially a <a class="existingWikiWord" href="/nlab/show/set">set</a> equipped with an <a class="existingWikiWord" href="/nlab/show/equivalence+relation">equivalence relation</a> or a similar <a class="existingWikiWord" href="/nlab/show/structure">structure</a> (such as a <em><a class="existingWikiWord" href="/nlab/show/pseudo-equivalence+relation">pseudo-equivalence relation</a></em>), and thought of as a stand-in for the would-be <a class="existingWikiWord" href="/nlab/show/quotient+set">quotient set</a> (<a class="existingWikiWord" href="/nlab/show/quotient+type">quotient type</a>) by that relation.</p> <p id="UsageInTheLiterature"> Accounts which take setoids to be…</p> <ul> <li> <p>…actual <a class="existingWikiWord" href="/nlab/show/equivalence+relations">equivalence relations</a>, i.e. <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Setoids</mi><mo>≔</mo><mo stretchy="false">(</mo><mi>X</mi><mo lspace="verythinmathspace">:</mo><mi>Set</mi><mo stretchy="false">)</mo><mo>×</mo><mo stretchy="false">(</mo><mi>R</mi><mo lspace="verythinmathspace">:</mo><mi>X</mi><mo>×</mo><mi>X</mi><mo>→</mo><mstyle mathcolor="purple"><mi>Prop</mi></mstyle><mo stretchy="false">)</mo><mo>×</mo><mi>ReflSymTrans</mi><mo stretchy="false">(</mo><mi>R</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Setoids \coloneqq (X \colon Set) \times (R \colon X \times X \to {\color{purple}Prop}) \times ReflSymTrans(R)</annotation></semantics></math>:</p> <p><a href="#Hofmann95">Hofmann (1995), §5.1.1</a>; <a href="#BartheCaprettaPons03">Barthe, Capretta & Pons (2003), §2.1</a>; <a href="https://stacks.math.columbia.edu/tag/04S9">Stacks Project</a>; <a href="https://hackage.haskell.org/package/setoid-0.1.0.0/docs/Data-Setoid.html">hackage.haskell</a>; <a href="https://en.wikipedia.org/wiki/Setoid">Wikipedia</a>;</p> </li> <li> <p>…<a class="existingWikiWord" href="/nlab/show/pseudo-equivalence+relations">pseudo-equivalence relations</a>, i.e. <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Setoids</mi><mo>≔</mo><mo stretchy="false">(</mo><mi>X</mi><mo lspace="verythinmathspace">:</mo><mi>Set</mi><mo stretchy="false">)</mo><mo>×</mo><mo stretchy="false">(</mo><mi>R</mi><mo lspace="verythinmathspace">:</mo><mi>X</mi><mo>×</mo><mi>X</mi><mo>→</mo><mstyle mathcolor="purple"><mi>Set</mi></mstyle><mo stretchy="false">)</mo><mo>×</mo><mi>ReflSymTrans</mi><mo stretchy="false">(</mo><mi>R</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Setoids \coloneqq (X \colon Set) \times (R \colon X \times X \to {\color{purple}Set}) \times ReflSymTrans(R)</annotation></semantics></math>:</p> <p><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>,</p> </li> <li> <p>… either:</p> <p><a href="#vdBergMoerdijk18">van den Berg & Moerdijk (2018)</a></p> </li> </ul> <p id="PointOfFirstDefinition"> Here the definition of setoids in terms of <a class="existingWikiWord" href="/nlab/show/equivalence+relations">equivalence relations</a> may be closer to the original intention of <a href="#Bishop67">Bishop (1967)</a> (though this remains a little vague) and is natural from the point of view of <a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a>/<a class="existingWikiWord" href="/nlab/show/homotopy+theory">homotopy theory</a> where setoids in this sense, and with equivalence of elements regarded as <a class="existingWikiWord" href="/nlab/show/isomorphism">isomorphism</a>, are exactly those <a class="existingWikiWord" href="/nlab/show/groupoids">groupoids</a> which are <a class="existingWikiWord" href="/nlab/show/equivalence+of+categories">equivalent</a> to sets (the <a class="existingWikiWord" href="/nlab/show/0-truncated">0-truncated</a> groupoids).</p> <p>Another perspective is that setoids in the sense of equivalence relations consitute the <a class="existingWikiWord" href="/nlab/show/ex%2Freg+completion">ex/reg completion</a> of <a class="existingWikiWord" href="/nlab/show/Sets">Sets</a>, while those in terms of pseudo-equivalence relations constitute the <a class="existingWikiWord" href="/nlab/show/ex%2Flex+completion">ex/lex completion</a> of <a class="existingWikiWord" href="/nlab/show/Sets">Sets</a>.</p> <p>In terms of <a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a>, the definition in terms of <a class="existingWikiWord" href="/nlab/show/equivalence+relations">equivalence relations</a> is natural under the <em><a class="existingWikiWord" href="/nlab/show/propositions+as+some+types">propositions as some types</a></em>-paradigm, while the definition in terms of <a class="existingWikiWord" href="/nlab/show/pseudo-equivalence+relations">pseudo-equivalence relations</a> is natural under the <em><a class="existingWikiWord" href="/nlab/show/propositions-as-types">types as propositions</a></em>-paradigm.</p> <p id="TerminologyDiffers"> In any case, beware that terminology and definitions may differ significantly across authors, cf. <a href="#Palmgren05">Palmgren (2005)</a> <a href="https://ncatlab.org/nlab/files/Palmgren-BishopSetTheory.pdf#page=9">p. 9</a>.</p> <p>Setoids are also sometimes used in “impoverished” <a class="existingWikiWord" href="/nlab/show/foundations+of+mathematics">foundations of mathematics</a> that lack a primitive notion of <a class="existingWikiWord" href="/nlab/show/quotient+set">quotient set</a>; see for instance <em><a class="existingWikiWord" href="/nlab/show/Bishop+set">Bishop set</a></em>.</p> <h2 id="applications">Applications</h2> <p>In <a class="existingWikiWord" href="/nlab/show/constructive+mathematics">constructive mathematics</a>, we want the <a class="existingWikiWord" href="/nlab/show/real+numbers">real numbers</a> to form a <a class="existingWikiWord" href="/nlab/show/linearly+ordered+set">linearly ordered</a> <a class="existingWikiWord" href="/nlab/show/Heyting+field">Heyting field</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>R</mi></mrow><annotation encoding="application/x-tex">R</annotation></semantics></math> with completeness for located <a class="existingWikiWord" href="/nlab/show/Dedekind+cuts">Dedekind cuts</a>. Using <a class="existingWikiWord" href="/nlab/show/power+sets">power sets</a> and a set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>N</mi></mrow><annotation encoding="application/x-tex">N</annotation></semantics></math> of <a class="existingWikiWord" href="/nlab/show/natural+numbers">natural numbers</a>, one may form <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>R</mi></mrow><annotation encoding="application/x-tex">R</annotation></semantics></math> directly as a <a class="existingWikiWord" href="/nlab/show/subset">subset</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>𝒫</mi><mi>N</mi></mrow><annotation encoding="application/x-tex">\mathcal{P}N</annotation></semantics></math> (or something equivalent), but what if you wish to be (at least weakly) <a class="existingWikiWord" href="/nlab/show/predicative+mathematics">predicative</a>? Using <a class="existingWikiWord" href="/nlab/show/function+sets">function sets</a>, one may form the Cauchy reals as a <a class="existingWikiWord" href="/nlab/show/subquotient">subquotient</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>N</mi> <mi>N</mi></msup></mrow><annotation encoding="application/x-tex">N^N</annotation></semantics></math>, but these are complete in the desired sense only if a weak form of <a class="existingWikiWord" href="/nlab/show/countable+choice">countable choice</a> (which follows from either the presentation axiom or <a class="existingWikiWord" href="/nlab/show/excluded+middle">excluded middle</a>) holds. (Essentially, there may not be enough <a class="existingWikiWord" href="/nlab/show/sequences">sequences</a> of natural numbers.) Alternatively, if you have them, you can use <a class="existingWikiWord" href="/nlab/show/prefunction">prefunction</a> sets and form <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>R</mi></mrow><annotation encoding="application/x-tex">R</annotation></semantics></math> as a subquotient of the set of <em>presequences</em> of natural numbers.</p> <p>The construction of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>R</mi></mrow><annotation encoding="application/x-tex">R</annotation></semantics></math> above may also be done with entire relations if the <a class="existingWikiWord" href="/nlab/show/axiom+of+fullness">axiom of fullness</a> holds (see also <a class="existingWikiWord" href="/nlab/show/real+numbers+object">real numbers object</a>). Conversely, the axiom of fullness follows from the existence of sets of prefunctions; in addition to defining a functional entire prerelation, a prefunction between sets also defines an entire relation, and the set of these satisfies fullness. (This is related to the idea that prefunctions between sets may be formalised as entire relations.)</p> <p>See also the discussion at <a class="existingWikiWord" href="/nlab/show/net">net</a> about how to force the domain of a net to be <a class="existingWikiWord" href="/nlab/show/partially+ordered">partial order</a>, by using either entire relations or prefunctions as nets.</p> <p>More generally, setoids (defined using <a class="existingWikiWord" href="/nlab/show/equivalence+relations">equivalence relations</a>) are <a class="existingWikiWord" href="/nlab/show/thin+category">thin</a> <a class="existingWikiWord" href="/nlab/show/groupoids">groupoids</a>. As a result, various concepts translate from the setting of <a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a> to setoid theory, such as</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/monoidal+setoid">monoidal setoid</a></li> <li><a class="existingWikiWord" href="/nlab/show/braided+monoidal+setoid">braided monoidal setoid</a></li> <li><a class="existingWikiWord" href="/nlab/show/groupal+setoid">groupal setoid</a> (i.e. <a class="existingWikiWord" href="/nlab/show/locally+thin+2-category">locally thin</a> <a class="existingWikiWord" href="/nlab/show/2-groups">2-groups</a>)</li> <li><a class="existingWikiWord" href="/nlab/show/braided+groupal+setoid">braided groupal setoid</a></li> <li><a class="existingWikiWord" href="/nlab/show/ring+setoid">ring setoid</a></li> <li><a class="existingWikiWord" href="/nlab/show/braided+ring+setoid">braided ring setoid</a></li> </ul> <h2 id="fixing_inadequate_foundations">Fixing inadequate foundations</h2> <p>Sometimes one finds a <a class="existingWikiWord" href="/nlab/show/foundation">foundation</a> of <a class="existingWikiWord" href="/nlab/show/predicative+mathematics">predicative mathematics</a> in which it appears to be impossible to construct <a class="existingWikiWord" href="/nlab/show/quotient+sets">quotient sets</a>, leading to much hand-wringing. (For a simple example, simply remove the axiom of <a class="existingWikiWord" href="/nlab/show/power+sets">power sets</a> from <a class="existingWikiWord" href="/nlab/show/ZFC">ZFC</a> as normally presented.)</p> <p>Assuming (as usual) that the original foundation had equality relations on its sets, there will be identity prerelations on the presets, leading to a special class of sets which we may again call the <strong>completely presented sets</strong>.</p> <p>When you do this, the new kind of set is called a setoid, and then there may be hand-wringing about the need to use setoids instead of sets as one would like. But if you didn't have quotient sets originally, then you shouldn't have been talking about ‘sets’ in the first place; theories of sets without quotient sets are really theories of presets.</p> <p>Some foundations also adopt an <a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a> for functions which do not preserve the equivalence relation that, together with the identity relations, proves the <a class="existingWikiWord" href="/nlab/show/presentation+axiom">presentation axiom</a> for general sets, which means that free sets are completely presented sets.</p> <p>If you are willing to accept the <a class="existingWikiWord" href="/nlab/show/presentation+axiom">presentation axiom</a>, then you can define a notion of setoid internal to a given theory of sets: as a <a class="existingWikiWord" href="/nlab/show/projective+set">projective set</a>. (With the full axiom of choice, therefore, a setoid is simply a set.) Alternatively, you might forgo setoid as such but define a <a class="existingWikiWord" href="/nlab/show/prefunction">prefunction</a> between sets to be an entire relation.</p> <p>A similar result holds for <a class="existingWikiWord" href="/nlab/show/SEAR+plus+epsilon">SEAR+<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"> <semantics> <mrow> <mi>ϵ</mi> </mrow> <annotation encoding="application/x-tex">\epsilon</annotation> </semantics> </math></a>.</p> <h2 id="related_concepts">Related concepts</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Bishop+set">Bishop set</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>, <a class="existingWikiWord" href="/nlab/show/pseudo-equivalence+relation">pseudo-equivalence relation</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/homotopy+exact+completion">homotopy exact completion</a></p> </li> </ul> <h2 id="references">References</h2> <p>The notion of “<a class="existingWikiWord" href="/nlab/show/Bishop+sets">Bishop sets</a>” goes to back the definition of sets in <a class="existingWikiWord" href="/nlab/show/constructive+mathematics">constructive mathematics</a>/<a class="existingWikiWord" href="/nlab/show/constructive+analysis">constructive analysis</a> according to:</p> <ul> <li id="Bishop67"> <p><a class="existingWikiWord" href="/nlab/show/Errett+Bishop">Errett Bishop</a>, <em><a class="existingWikiWord" href="/nlab/show/Foundations+of+Constructive+Analysis">Foundations of Constructive Analysis</a></em>, Mcgraw-Hill (1967)</p> </li> <li id="BishopBridges85"> <p><a class="existingWikiWord" href="/nlab/show/Errett+Bishop">Errett Bishop</a>, <a class="existingWikiWord" href="/nlab/show/Douglas+Bridges">Douglas Bridges</a>, p. 15 of: <em><a class="existingWikiWord" href="/nlab/show/Constructive+Analysis">Constructive Analysis</a></em>, Grundlehren der mathematischen Wissenschaften <strong>279</strong>, Springer (1985) [<a href="https://doi.org/10.1007/978-3-642-61667-9">doi:10.1007/978-3-642-61667-9</a>]</p> </li> </ul> <p>The connection to <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a> and the term <em>setoid</em> is due to</p> <ul> <li id="Hofmann95"><a class="existingWikiWord" href="/nlab/show/Martin+Hofmann">Martin Hofmann</a>, §1.3, §5.1 in: <em>Extensional concepts in intensional type theory</em>, Ph.D. thesis, University of Edinburgh (1995), Distinguished Dissertations, Springer (1997) [<a href="http://www.lfcs.inf.ed.ac.uk/reports/95/ECS-LFCS-95-327/">ECS-LFCS-95-327</a>, <a class="existingWikiWord" href="/nlab/files/HofmannExtensionalIntensionalTypeTheory.pdf" title="pdf">pdf</a>, <a href="https://doi.org/10.1007/978-1-4471-0963-1">doi:10.1007/978-1-4471-0963-1</a>]</li> </ul> <p>Survey of further developments:</p> <ul> <li id="BartheCaprettaPons03"> <p><a class="existingWikiWord" href="/nlab/show/Gilles+Barthe">Gilles Barthe</a>, Venanzio Capretta, <a class="existingWikiWord" href="/nlab/show/Olivier+Pons">Olivier Pons</a>, <em>Setoids in type theory</em>, Journal of Functional Programming <strong>13</strong> 2 (2003) 261-293 [<a href="https://doi.org/10.1017/S0956796802004501">doi:10.1017/S0956796802004501</a>]</p> </li> <li id="Palmgren05"> <p><a class="existingWikiWord" href="/nlab/show/Erik+Palmgren">Erik Palmgren</a>, <em>Bishop’s set theory</em> (2005) [<a href="http://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/palmgren.pdf">pdf</a>, <a class="existingWikiWord" href="/nlab/files/Palmgren-BishopSetTheory.pdf" title="pdf">pdf</a>]</p> </li> </ul> <p>See also:</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="vdBergMoerdijk18"> <p><a class="existingWikiWord" href="/nlab/show/Benno+van+den+Berg">Benno van den Berg</a>, <a class="existingWikiWord" href="/nlab/show/Ieke+Moerdijk">Ieke Moerdijk</a>, <em>Exact completion of path categories and algebraic set theory: Part I: Exact completion of path categories</em>, Journal of Pure and Applied Algebra <strong>222</strong> 10 (2018) 3137-3181 [<a href="https://doi.org/10.1016/j.jpaa.2017.11.017">doi:10.1016/j.jpaa.2017.11.017</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> <li> <p>hackage.haskell, <em><a href="https://hackage.haskell.org/package/setoid-0.1.0.0/docs/Data-Setoid.html">Data-Setoid.html</a></em></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Stacks+Project">Stacks Project</a>, <em>Categories fibred in setoids</em> [<a href="https://stacks.math.columbia.edu/tag/04S9">tag:04S9</a>]</p> </li> <li> <p>Wikipedia, <em><a href="https://en.wikipedia.org/wiki/Setoid">Setoid</a></em></p> </li> </ul> <div class="property">category: <a class="category_link" href="/nlab/all_pages/disambiguation">disambiguation</a></div></body></html> </div> <div class="revisedby"> <p> Last revised on July 10, 2024 at 14:51:49. See the <a href="/nlab/history/setoid" 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/setoid" accesskey="E" class="navlink" id="edit" rel="nofollow">Edit</a><a href="https://nforum.ncatlab.org/discussion/12612/#Item_14">Discuss</a><span class="backintime"><a href="/nlab/revision/setoid/36" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/diff/setoid" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Changes from previous revision</a><a href="/nlab/history/setoid" accesskey="S" class="navlink" id="history" rel="nofollow">History (36 revisions)</a> <a href="/nlab/show/setoid/cite" style="color: black">Cite</a> <a href="/nlab/print/setoid" accesskey="p" id="view_print" rel="nofollow">Print</a> <a href="/nlab/source/setoid" id="view_source" rel="nofollow">Source</a> </div> </div>  </div>  </body> </html>