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> preorder 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> preorder </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/14836/#Item_4" 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>Contents</title></head> <body> <div class="rightHandSide"> <div class="toc clickDown" tabindex="0"> <h3 id="context">Context</h3> <h4 id="category_theory"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mn>0</mn><mo>,</mo><mn>1</mn><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(0,1)</annotation></semantics></math>-Category theory</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/%280%2C1%29-category+theory">(0,1)-category theory</a></strong>: <a class="existingWikiWord" href="/nlab/show/logic">logic</a>, <a class="existingWikiWord" href="/nlab/show/order+theory">order theory</a></p> <p><strong><a class="existingWikiWord" href="/nlab/show/%280%2C1%29-category">(0,1)-category</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/relation+between+preorders+and+%280%2C1%29-categories">relation between preorders and (0,1)-categories</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/proset">proset</a>, <a class="existingWikiWord" href="/nlab/show/partially+ordered+set">partially ordered set</a> (<a class="existingWikiWord" href="/nlab/show/directed+set">directed set</a>, <a class="existingWikiWord" href="/nlab/show/total+order">total order</a>, <a class="existingWikiWord" href="/nlab/show/linear+order">linear order</a>)</p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/top">top</a>, <a class="existingWikiWord" href="/nlab/show/true">true</a>,</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/bottom">bottom</a>, <a class="existingWikiWord" href="/nlab/show/false">false</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/monotone+function">monotone function</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/implication">implication</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/filter">filter</a>, <a class="existingWikiWord" href="/nlab/show/interval">interval</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/lattice">lattice</a>, <a class="existingWikiWord" href="/nlab/show/semilattice">semilattice</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/meet">meet</a>, <a class="existingWikiWord" href="/nlab/show/logical+conjunction">logical conjunction</a>, <a class="existingWikiWord" href="/nlab/show/and">and</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/join">join</a>, <a class="existingWikiWord" href="/nlab/show/logical+disjunction">logical disjunction</a>, <a class="existingWikiWord" href="/nlab/show/or">or</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/compact+element">compact element</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/lattice+of+subobjects">lattice of subobjects</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/complete+lattice">complete lattice</a>, <a class="existingWikiWord" href="/nlab/show/algebraic+lattice">algebraic lattice</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/distributive+lattice">distributive lattice</a>, <a class="existingWikiWord" href="/nlab/show/completely+distributive+lattice">completely distributive lattice</a>, <a class="existingWikiWord" href="/nlab/show/canonical+extension">canonical extension</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/hyperdoctrine">hyperdoctrine</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/first-order+hyperdoctrine">first-order</a>, <a class="existingWikiWord" href="/nlab/show/Boolean+hyperdoctrine">Boolean</a>, <a class="existingWikiWord" href="/nlab/show/coherent+hyperdoctrine">coherent</a>, <a class="existingWikiWord" href="/nlab/show/tripos">tripos</a></li> </ul> </li> </ul> <p><strong><a class="existingWikiWord" href="/nlab/show/%280%2C1%29-topos">(0,1)-topos</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Heyting+algebra">Heyting algebra</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/regular+element">regular element</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Boolean+algebra">Boolean algebra</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/frame">frame</a>, <a class="existingWikiWord" href="/nlab/show/locale">locale</a></p> </li> </ul> <h2 id="theorems">Theorems</h2> <ul> <li><a class="existingWikiWord" href="/nlab/show/Stone+duality">Stone duality</a></li> </ul> </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="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="homotopy_type_theory">Homotopy type theory</h4> <div class="hide"><div> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</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> <div class="property">category: <a class="category_link" href="/nlab/all_pages/type+theory">type theory</a></div></div></div> </div> </div> <h1 id="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='#as_a_set_with_a_relation'>As a set with a relation</a></li> <li><a href='#as_a_graph'>As a graph</a></li> <li><a href='#AsACategory'>As a category</a></li> <li><a href='#in_homotopy_type_theory'>In homotopy type theory</a></li> </ul> <li><a href='#properties'>Properties</a></li> <ul> <li><a href='#relation_to_partial_orders'>Relation to partial orders</a></li> <li><a href='#relation_to_thin_categories'>Relation to thin categories</a></li> <li><a href='#construction_of_preorders_from_any_binary_relation'>Construction of preorders from any binary relation</a></li> <li><a href='#preorder_reflection'>Preorder reflection</a></li> <li><a href='#cauchy_completion'>Cauchy completion</a></li> </ul> <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>preorder</em> or a <em>quasi-order</em> is like a <a class="existingWikiWord" href="/nlab/show/partial+order">partial order</a>, but without the “antisymmetry” requirement that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>≤</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">x \leq y</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>≤</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">y \leq x</annotation></semantics></math> implies <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>=</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">x = y</annotation></semantics></math>.</p> <p>By interpreting the relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≤</mo></mrow><annotation encoding="application/x-tex">\leq</annotation></semantics></math> as the existence of a unique <a class="existingWikiWord" href="/nlab/show/morphism">morphism</a>, preorders may be regarded as certain <a class="existingWikiWord" href="/nlab/show/categories">categories</a> (namely, <a class="existingWikiWord" href="/nlab/show/thin+categories">thin categories</a>). This category is sometimes called the <em>preorder category</em> associated to a preorder; see below for details.</p> <h2 id="definition">Definition</h2> <h3 id="as_a_set_with_a_relation">As a set with a relation</h3> <p>A <strong>preorder</strong> or <strong>quasiorder</strong> on a set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math> is a <a class="existingWikiWord" href="/nlab/show/reflexive+relation">reflexive</a> and <a class="existingWikiWord" href="/nlab/show/transitive+relation">transitive</a> relation, generally written <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≤</mo></mrow><annotation encoding="application/x-tex">\leq</annotation></semantics></math>. A <strong>preordered set</strong>, or <strong>proset</strong>, is a set equipped with a preorder. (This should not be confused with a <a class="existingWikiWord" href="/nlab/show/pro-set">pro-set</a>, i.e. a <a class="existingWikiWord" href="/nlab/show/pro-object">pro-object</a> in <a class="existingWikiWord" href="/nlab/show/Set">Set</a>.)</p> <h3 id="as_a_graph">As a graph</h3> <p>A <strong>preordered set</strong> is a <a class="existingWikiWord" href="/nlab/show/loop+digraph+object">loop</a> <a class="existingWikiWord" href="/nlab/show/digraph">digraph</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>V</mi><mo>,</mo><mi>E</mi><mo>,</mo><mi>s</mi><mo>:</mo><mi>E</mi><mo>→</mo><mi>V</mi><mo>,</mo><mi>t</mi><mo>:</mo><mi>E</mi><mo>→</mo><mi>V</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(V, E, s:E \to V, t:E \to V)</annotation></semantics></math>, with functions <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>refl</mi><mo>:</mo><mi>V</mi><mo>→</mo><mi>E</mi></mrow><annotation encoding="application/x-tex">refl:V \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>tr</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">tr:\{(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>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(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>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(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>tr</mi><mo stretchy="false">(</mo><mi>g</mi><mo>,</mo><mi>f</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(tr(g,f)) =_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>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>t</mi><mo stretchy="false">(</mo><mi>tr</mi><mo stretchy="false">(</mo><mi>g</mi><mo>,</mo><mi>f</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(tr(g,f)) =_E t(g)</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>tr</mi><mo stretchy="false">(</mo><mi>f</mi><mo>,</mo><mi>refl</mi><mo stretchy="false">(</mo><mi>s</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo stretchy="false">)</mo><msub><mo>=</mo> <mi>E</mi></msub><mi>f</mi></mrow><annotation encoding="application/x-tex">tr(f, refl(s(f))) =_E 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>tr</mi><mo stretchy="false">(</mo><mi>refl</mi><mo stretchy="false">(</mo><mi>t</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>,</mo><mi>f</mi><mo stretchy="false">)</mo><msub><mo>=</mo> <mi>E</mi></msub><mi>f</mi></mrow><annotation encoding="application/x-tex">tr(refl(t(f)), f) =_E 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>g</mi><mo>∈</mo><mi>E</mi></mrow><annotation encoding="application/x-tex">g \in E</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></mrow><annotation encoding="application/x-tex">h \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> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>t</mi><mo stretchy="false">(</mo><mi>g</mi><mo stretchy="false">)</mo><msub><mo>=</mo> <mi>V</mi></msub><mi>s</mi><mo stretchy="false">(</mo><mi>h</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">t(g) =_V s(h)</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>tr</mi><mo stretchy="false">(</mo><mi>h</mi><mo>,</mo><mi>tr</mi><mo stretchy="false">(</mo><mi>g</mi><mo>,</mo><mi>f</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><msub><mo>=</mo> <mi>E</mi></msub><mi>tr</mi><mo stretchy="false">(</mo><mi>tr</mi><mo stretchy="false">(</mo><mi>h</mi><mo>,</mo><mi>g</mi><mo stretchy="false">)</mo><mo>,</mo><mi>f</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">tr(h,tr(g,f)) =_E tr(tr(h,g),f)</annotation></semantics></math></li> </ul> <h3 id="AsACategory">As a category</h3> <p><a class="existingWikiWord" href="/nlab/show/relation+between+preorders+and+%280%2C1%29-categories">Equivalently, a preordered set is</a> a (<a class="existingWikiWord" href="/nlab/show/strict+category">strict</a>) <a class="existingWikiWord" href="/nlab/show/thin+category">thin category</a>: a <a class="existingWikiWord" href="/nlab/show/strict+category">strict category</a> such that for any <a class="existingWikiWord" href="/nlab/show/pair">pair</a> of <a class="existingWikiWord" href="/nlab/show/objects">objects</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>,</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">x, y</annotation></semantics></math>, there is at most one <a class="existingWikiWord" href="/nlab/show/morphism">morphism</a> from <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 <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi></mrow><annotation encoding="application/x-tex">y</annotation></semantics></math>. The existence of such a morphism corresponds to the truth of the relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>≤</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">x \leq y</annotation></semantics></math>. <a class="existingWikiWord" href="/nlab/show/relation+between+preorders+and+%280%2C1%29-categories">In other words, it's</a> a (strict) <a class="existingWikiWord" href="/nlab/show/category+enriched">category enriched</a> over the <a class="existingWikiWord" href="/nlab/show/cartesian+monoidal+category">cartesian monoidal category</a> of <a class="existingWikiWord" href="/nlab/show/truth+values">truth values</a> (a <a class="existingWikiWord" href="/nlab/show/%280%2C1%29-category">(0,1)-category</a>).</p> <h3 id="in_homotopy_type_theory">In homotopy type theory</h3> <p>In <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a>, we must be careful to distinguish <em>preorders</em> (on a homotopy type of arbitrary <a class="existingWikiWord" href="/nlab/show/h-level">h-level</a>) and <em>preordered sets</em> (which apply to an <a class="existingWikiWord" href="/nlab/show/h-set">h-set</a>). When translating ordinary, set-level mathematics to HoTT, preordered sets are almost always what is wanted. A preorder on a type <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> consists of:</p> <ul> <li> <p>For each pair of elements <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>,</mo><mi>b</mi><mo>:</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">a, b : A</annotation></semantics></math>, a <a class="existingWikiWord" href="/nlab/show/mere+proposition"> proposition</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>≤</mo><mi>b</mi></mrow><annotation encoding="application/x-tex">a \le b</annotation></semantics></math>;</p> </li> <li> <p>For every <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>:</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">a : A</annotation></semantics></math>, a witness of <em>reflexivity</em> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mo lspace="0em" rspace="thinmathspace">refl</mo> <mi>a</mi></msub><mo>:</mo><mi>a</mi><mo>≤</mo><mi>a</mi></mrow><annotation encoding="application/x-tex">\operatorname{refl}_a : a \le a</annotation></semantics></math></p> </li> <li> <p>For every <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>,</mo><mi>b</mi><mo>,</mo><mi>c</mi><mo>:</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">a, b, c : A</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi><mo>:</mo><mi>a</mi><mo>≤</mo><mi>b</mi></mrow><annotation encoding="application/x-tex">p : a \le b</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>q</mi><mo>:</mo><mi>b</mi><mo>≤</mo><mi>c</mi></mrow><annotation encoding="application/x-tex">q : b \le c</annotation></semantics></math>, a witness of <em>transitivity</em> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mo lspace="0em" rspace="thinmathspace">trans</mo> <mrow><mi>a</mi><mo>,</mo><mi>b</mi><mo>,</mo><mi>c</mi></mrow></msub><mo stretchy="false">(</mo><mi>p</mi><mo>,</mo><mi>q</mi><mo stretchy="false">)</mo><mo>:</mo><mi>a</mi><mo>≤</mo><mi>c</mi></mrow><annotation encoding="application/x-tex">\operatorname{trans}_{a,b,c}(p, q) : a \le c</annotation></semantics></math>.</p> </li> </ul> <p>Note that, as usual, the quantifiers “for each” and “for every” should be interpreted as applications of the corresponding <a class="existingWikiWord" href="/nlab/show/dependent+function+types">dependent function types</a>. Every homotopy type <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> has an <a class="existingWikiWord" href="/nlab/show/h-set">h-set</a> of possible preordered structures, but the <a class="existingWikiWord" href="/nlab/show/dependent+sum+type">sum</a> of all possible structures has h-level bounded by <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>‘s.</p> <h2 id="properties">Properties</h2> <h3 id="relation_to_partial_orders">Relation to partial orders</h3> <p>Any preordered set is <a class="existingWikiWord" href="/nlab/show/equivalence+of+categories">equivalent</a> to a <a class="existingWikiWord" href="/nlab/show/partial+order">poset</a>. This is a special case of the theorem that every category has a <a class="existingWikiWord" href="/nlab/show/skeleton">skeleton</a>, but (if you define ‘equivalence’ weakly enough) this case does <em>not</em> require the <a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a>.</p> <p>If the <a class="existingWikiWord" href="/nlab/show/foundations">foundations</a> have <a class="existingWikiWord" href="/nlab/show/quotient+sets">quotient sets</a>, then every preorder has a quotient set equivalent to a poset. Let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>P</mi><mo>,</mo><mo>≤</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(P, \leq)</annotation></semantics></math> be a preorder. Define the <a class="existingWikiWord" href="/nlab/show/equivalence+relation">equivalence relation</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">\sim</annotation></semantics></math> on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math> for all elements <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>,</mo><mi>b</mi><mo>∈</mo><mi>P</mi></mrow><annotation encoding="application/x-tex">a, b \in P</annotation></semantics></math> as <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∼</mo><mi>b</mi><mo>:</mo><mo>=</mo><mo stretchy="false">(</mo><mi>a</mi><mo>≤</mo><mi>b</mi><mo stretchy="false">)</mo><mo>∧</mo><mo stretchy="false">(</mo><mi>b</mi><mo>≤</mo><mi>a</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">a \sim b := (a \leq b) \wedge (b \leq a)</annotation></semantics></math>. Then the quotient set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo stretchy="false">/</mo><mo>∼</mo></mrow><annotation encoding="application/x-tex">P / \sim</annotation></semantics></math> is a poset. This is the 0-truncated version of the fact that because every <a class="existingWikiWord" href="/nlab/show/category+object+in+an+%28infinity%2C1%29-category">precategory</a> has a <a class="existingWikiWord" href="/nlab/show/core">core</a> <a class="existingWikiWord" href="/nlab/show/groupoid+object+in+an+%28infinity%2C1%29-category">pregroupoid</a> and every pregroupoid has a Rezk completion into a <a class="existingWikiWord" href="/nlab/show/groupoid">groupoid</a>, every precategory has a Rezk completion into a <a class="existingWikiWord" href="/nlab/show/category">category</a>.</p> <p>Note that while in <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a>, preorders can be applied to general types (thus the need for differentiating between preorders and preordered <em>sets</em>), partial orders necessarily apply to sets: Any map <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi><mo>:</mo><mo stretchy="false">(</mo><mi>a</mi><mo>≤</mo><mi>b</mi><mo stretchy="false">)</mo><mo>∧</mo><mo stretchy="false">(</mo><mi>b</mi><mo>≤</mo><mi>a</mi><mo stretchy="false">)</mo><mo>→</mo><mo stretchy="false">(</mo><mi>a</mi><mo>=</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">p : (a \le b) \wedge (b \le a) \to (a = b)</annotation></semantics></math> is necessarily a fibrewise equivalence (fixing <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 quantifying over <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>), since it induces an equivalence of total spaces. Thus, the codomain type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>a</mi><mo>=</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(a = b)</annotation></semantics></math> is a proposition, since the domain <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>a</mi><mo>≤</mo><mi>b</mi><mo stretchy="false">)</mo><mo>∧</mo><mo stretchy="false">(</mo><mi>b</mi><mo>≤</mo><mi>a</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(a \le b) \wedge (b \le a)</annotation></semantics></math>, being a product of propositions, is a proposition.</p> <h3 id="relation_to_thin_categories">Relation to thin categories</h3> <p>In <a class="existingWikiWord" href="/nlab/show/set+theory">set-theoretic</a> <a class="existingWikiWord" href="/nlab/show/foundations">foundations</a>, a preordered set is the same as a <a class="existingWikiWord" href="/nlab/show/thin+category">thin category</a> (a category in which any two parallel <a class="existingWikiWord" href="/nlab/show/morphisms">morphisms</a> are equal), and it is partially ordered just when it is <a class="existingWikiWord" href="/nlab/show/skeletal+category">skeletal</a>. Thus, asking for a preordered set to be partially ordered may seem to break the <a class="existingWikiWord" href="/nlab/show/principle+of+equivalence">principle of equivalence</a> of <a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a>. However, as remarked above, a thin category always has a <a class="existingWikiWord" href="/nlab/show/skeleton">skeleton</a> which is a poset; so working with posets up to isomorphism is the same as working with preordered sets up to equivalence. In other words, if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>≤</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">x \le y</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>≤</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">y \le x</annotation></semantics></math>, so that <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> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi></mrow><annotation encoding="application/x-tex">y</annotation></semantics></math> are <a class="existingWikiWord" href="/nlab/show/isomorphism">isomorphic</a>, we may as well say that they are equal (since they are isomorphic in only one way).</p> <p>Another way to say this is that the <a class="existingWikiWord" href="/nlab/show/nerve">nerve</a> <a class="existingWikiWord" href="/nlab/show/simplicial+set">simplicial set</a> of a preorder, which is necessarily a <em><a class="existingWikiWord" href="/nlab/show/Segal+space">Segal space</a></em> or <em><a class="existingWikiWord" href="/nlab/show/category+object+in+an+%28infinity%2C1%29-category">category object in an (infinity,1)-category</a></em> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi><mo>↪</mo><mn>∞</mn><mi>Grpd</mi></mrow><annotation encoding="application/x-tex">Set \hookrightarrow \infty Grpd</annotation></semantics></math>, is in addition a <em><a class="existingWikiWord" href="/nlab/show/complete+Segal+space">complete Segal space</a></em> or <em>genuine category object</em> 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> if the preorder is in fact a partial order. For more on this perspective see at <em><a href="Segal+space#InSetByNervesOfCategories">Segal space – Examples – In Set</a></em>.</p> <p>If we distinguish between isomorphism and <a class="existingWikiWord" href="/nlab/show/equality">equality</a> of elements in a preordered set (hence considering preordered sets up to isomorphism, rather than up to equivalence), then this is equivalent to considering the corresponding thin category to also be a <a class="existingWikiWord" href="/nlab/show/strict+category">strict category</a>. When treated in this sense, preordered sets are not equivalent to posets.</p> <p>On the other hand, in non-set-theoretic <a class="existingWikiWord" href="/nlab/show/foundations">foundations</a> where not every category need have an underlying set (i.e. need not be a <a class="existingWikiWord" href="/nlab/show/strict+category">strict category</a> in any canonical way) — such as <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a> or <a class="existingWikiWord" href="/nlab/show/preset">preset</a> theories — a preordered set defined as “a set with a relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≤</mo></mrow><annotation encoding="application/x-tex">\leq</annotation></semantics></math> …” is automatically a strict category, with a notion of equality of objects coming from the given set. By contrast, in this case a thin category (as opposed to a more general category) does have a canonical structure of strict category in which equality of objects <em>means</em> isomorphism, but not every strict thin category is canonical in this sense. In this case, partially ordered sets correspond to thin categories (with canonical strict-category structures), while preordered sets correspond to thin categories with arbitrary strict-category structures.</p> <h3 id="construction_of_preorders_from_any_binary_relation">Construction of preorders from any binary relation</h3> <p>(See also <a class="existingWikiWord" href="/nlab/show/codensity+monad">codensity monad</a>, <a class="existingWikiWord" href="/nlab/show/quantification#Guarded">guarded quantification</a>.)</p> <p> <div class='num_theorem'> <h6>Theorem</h6> <p>Given <a class="existingWikiWord" href="/nlab/show/sets">sets</a> <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> and a <a class="existingWikiWord" href="/nlab/show/binary+relation">binary relation</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>R</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">R(x, y)</annotation></semantics></math> between <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>, then the relation</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>T</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo>≔</mo><mo>∀</mo><mi>w</mi><mo>:</mo><mi>B</mi><mo>.</mo><mi>R</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>w</mi><mo stretchy="false">)</mo><mo>⇒</mo><mi>R</mi><mo stretchy="false">(</mo><mi>y</mi><mo>,</mo><mi>w</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">T(x, y) \coloneqq \forall w:B.R(x, w) \implies R(y, w)</annotation></semantics></math></div> <p>is a <a class="existingWikiWord" href="/nlab/show/preorder">preorder</a> on <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> </div> </p> <p> <div class='proof'> <h6>Proof</h6> <p>We work in <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a>, where implication is denoted by the <a class="existingWikiWord" href="/nlab/show/function+type">function type</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo>→</mo><mi>Q</mi></mrow><annotation encoding="application/x-tex">P \to Q</annotation></semantics></math> and universal quantification is denoted by the <a class="existingWikiWord" href="/nlab/show/dependent+product+type">dependent product type</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo> <mrow><mi>x</mi><mo>:</mo><mi>A</mi></mrow></msub><mi>P</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\prod_{x:A} P(x)</annotation></semantics></math>. Thus, the type family <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">T(x, y)</annotation></semantics></math> is represented as</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>T</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo>≔</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo> <mrow><mi>w</mi><mo>:</mo><mi>B</mi></mrow></munder><mi>R</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>w</mi><mo stretchy="false">)</mo><mo>→</mo><mi>R</mi><mo stretchy="false">(</mo><mi>y</mi><mo>,</mo><mi>w</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">T(x, y) \coloneqq \prod_{w:B} R(x, w) \to R(y, w)</annotation></semantics></math></div> <p>A <a class="existingWikiWord" href="/nlab/show/binary+relation">binary relation</a> in dependent type theory is a type family <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>:</mo><mi>A</mi><mo>,</mo><mi>y</mi><mo>:</mo><mi>B</mi><mo>⊢</mo><mi>R</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">x:A, y:B \vdash R(x, y)</annotation></semantics></math> such that each <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>R</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">R(x, y)</annotation></semantics></math> is an <a class="existingWikiWord" href="/nlab/show/h-proposition">h-proposition</a>. Since <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>R</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>w</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">R(x, w)</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>R</mi><mo stretchy="false">(</mo><mi>y</mi><mo>,</mo><mi>w</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">R(y, w)</annotation></semantics></math> are both <a class="existingWikiWord" href="/nlab/show/h-propositions">h-propositions</a>, and h-propositions are closed under <a class="existingWikiWord" href="/nlab/show/function+types">function types</a> and <a class="existingWikiWord" href="/nlab/show/dependent+product+types">dependent product types</a>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">T(x, y)</annotation></semantics></math> is also valued in <a class="existingWikiWord" href="/nlab/show/h-propositions">h-propositions</a>, and is a binary relation.</p> <p>In addition, for all elements <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>:</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">x:A</annotation></semantics></math>, there is an element</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msub><mi mathvariant="normal">refl</mi> <mi>T</mi></msub><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>:</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo> <mrow><mi>w</mi><mo>:</mo><mi>B</mi></mrow></munder><mi>R</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>w</mi><mo stretchy="false">)</mo><mo>→</mo><mi>R</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>w</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathrm{refl}_{T}(x):\prod_{w:B} R(x, w) \to R(x, w)</annotation></semantics></math></div> <p>defined by the <a class="existingWikiWord" href="/nlab/show/identity+function">identity function</a> on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>R</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>w</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">R(x, w)</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 mathvariant="normal">refl</mi> <mi>T</mi></msub><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi>w</mi><mo stretchy="false">)</mo><mo>≔</mo><msub><mi mathvariant="normal">id</mi> <mrow><mi>R</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>w</mi><mo stretchy="false">)</mo></mrow></msub></mrow><annotation encoding="application/x-tex">\mathrm{refl}_{T}(x)(w) \coloneqq \mathrm{id}_{R(x, w)}</annotation></semantics></math></div> <p>and for all elements <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>:</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">x:A</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>:</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">y:A</annotation></semantics></math>, and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>z</mi><mo>:</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">z:A</annotation></semantics></math>, there is a function</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msub><mi mathvariant="normal">trans</mi> <mi>T</mi></msub><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo>,</mo><mi>z</mi><mo stretchy="false">)</mo><mo>:</mo><mrow><mo>(</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo> <mrow><mi>w</mi><mo>:</mo><mi>B</mi></mrow></munder><mi>R</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>w</mi><mo stretchy="false">)</mo><mo>→</mo><mi>R</mi><mo stretchy="false">(</mo><mi>y</mi><mo>,</mo><mi>w</mi><mo stretchy="false">)</mo><mo>)</mo></mrow><mo>×</mo><mrow><mo>(</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo> <mrow><mi>w</mi><mo>:</mo><mi>B</mi></mrow></munder><mi>R</mi><mo stretchy="false">(</mo><mi>y</mi><mo>,</mo><mi>w</mi><mo stretchy="false">)</mo><mo>→</mo><mi>R</mi><mo stretchy="false">(</mo><mi>z</mi><mo>,</mo><mi>w</mi><mo stretchy="false">)</mo><mo>)</mo></mrow><mo>→</mo><mrow><mo>(</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo> <mrow><mi>w</mi><mo>:</mo><mi>B</mi></mrow></munder><mi>R</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>w</mi><mo stretchy="false">)</mo><mo>→</mo><mi>R</mi><mo stretchy="false">(</mo><mi>z</mi><mo>,</mo><mi>w</mi><mo stretchy="false">)</mo><mo>)</mo></mrow></mrow><annotation encoding="application/x-tex">\mathrm{trans}_{T}(x, y, z):\left(\prod_{w:B} R(x, w) \to R(y, w)\right) \times \left(\prod_{w:B} R(y, w) \to R(z, w)\right) \to \left(\prod_{w:B} R(x, w) \to R(z, w)\right)</annotation></semantics></math></div> <p>defined by <a class="existingWikiWord" href="/nlab/show/composition">composition</a> of the functions <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo stretchy="false">(</mo><mi>w</mi><mo stretchy="false">)</mo><mo>:</mo><mi>R</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>w</mi><mo stretchy="false">)</mo><mo>→</mo><mi>R</mi><mo stretchy="false">(</mo><mi>y</mi><mo>,</mo><mi>w</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f(w):R(x, w) \to R(y, w)</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>g</mi><mo stretchy="false">(</mo><mi>w</mi><mo stretchy="false">)</mo><mo>:</mo><mi>R</mi><mo stretchy="false">(</mo><mi>y</mi><mo>,</mo><mi>w</mi><mo stretchy="false">)</mo><mo>→</mo><mi>R</mi><mo stretchy="false">(</mo><mi>z</mi><mo>,</mo><mi>w</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">g(w):R(y, w) \to R(z, w)</annotation></semantics></math> dependent upon element <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>w</mi><mo>:</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">w: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><msub><mi mathvariant="normal">trans</mi> <mi>T</mi></msub><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo>,</mo><mi>z</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><mi>w</mi><mo stretchy="false">)</mo><mo>≔</mo><mi>g</mi><mo stretchy="false">(</mo><mi>w</mi><mo stretchy="false">)</mo><mo>∘</mo><mi>f</mi><mo stretchy="false">(</mo><mi>w</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathrm{trans}_{T}(x, y, z)(f, g)(w) \coloneqq g(w) \circ f(w)</annotation></semantics></math></div> <p>Since the type</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><munder><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo> <mrow><mi>w</mi><mo>:</mo><mi>B</mi></mrow></munder><mi>R</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>w</mi><mo stretchy="false">)</mo><mo>→</mo><mi>R</mi><mo stretchy="false">(</mo><mi>y</mi><mo>,</mo><mi>w</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\prod_{w:B} R(x, w) \to R(y, w)</annotation></semantics></math></div> <p>is a <a class="existingWikiWord" href="/nlab/show/binary+relation">binary relation</a> valued in <a class="existingWikiWord" href="/nlab/show/h-propositions">h-propositions</a> which satisfies <a class="existingWikiWord" href="/nlab/show/reflexivity">reflexivity</a> and <a class="existingWikiWord" href="/nlab/show/transitivity">transitivity</a>, it is a <a class="existingWikiWord" href="/nlab/show/preorder">preorder</a>.</p> </div> </p> <h3 id="preorder_reflection">Preorder reflection</h3> <p>The 2-category of preorders (more precisely, that of <a class="existingWikiWord" href="/nlab/show/thin+categories">thin categories</a>) is <a class="existingWikiWord" href="/nlab/show/reflective+subcategory">reflective</a> in <a class="existingWikiWord" href="/nlab/show/Cat">Cat</a>. The reflector preserves the objects and declares <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>≤</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">x \leq y</annotation></semantics></math> if there exists an arrow from <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 <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi></mrow><annotation encoding="application/x-tex">y</annotation></semantics></math>.</p> <h3 id="cauchy_completion">Cauchy completion</h3> <div class="num_prop"> <h6 id="proposition">Proposition</h6> <p><a class="existingWikiWord" href="/nlab/show/internalization">Internal</a> to any <a class="existingWikiWord" href="/nlab/show/regular+category">regular category</a> every <a class="existingWikiWord" href="/nlab/show/poset">poset</a> is a <a class="existingWikiWord" href="/nlab/show/Cauchy+complete+category">Cauchy complete category</a>.</p> </div> <p>This appears as (<a href="#Rosolini">Rosolini, prop. 2.1</a>).</p> <div class="num_prop"> <h6 id="proposition_2">Proposition</h6> <p><a class="existingWikiWord" href="/nlab/show/internalization">Internal to</a> any <a class="existingWikiWord" href="/nlab/show/exact+category">exact category</a> the Cauchy completion of any <a class="existingWikiWord" href="/nlab/show/preorder">preorder</a> exists and is its <span class="newWikiWord">poset reflection<a href="/nlab/new/poset+reflection">?</a></span>.</p> </div> <p>This appears as (<a href="#Rosolini">Rosolini, corollary. 2.3</a>).</p> <h2 id="related_concepts">Related concepts</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/relation+between+preorders+and+%280%2C1%29-categories">relation between preorders and (0,1)-categories</a></p> </li> <li> <p><strong>preorder</strong></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/upper+bound">upper bound</a>, <a class="existingWikiWord" href="/nlab/show/lower+bound">lower bound</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/directed+set">directed set</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/partial+order">partial order</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/thin+category">thin category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/specialization+topology">specialization topology</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/specialization+order">specialization order</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/PreOrd">PreOrd</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/graph">graph</a>, <a class="existingWikiWord" href="/nlab/show/digraph">digraph</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/symmetric+preorder">symmetric preorder</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/preordered+object">preordered object</a></p> </li> </ul> <h2 id="references">References</h2> <p><a class="existingWikiWord" href="/nlab/show/Cauchy+completion">Cauchy completion</a> for preorders is discussed in</p> <ul> <li id="Rosolini">G. Rosolini, <em>A note on Cauchy completeness for preorders</em> (<a href="http://rivista.math.unipr.it/fulltext/1999-2s/06.pdf">pdf</a>)</li> </ul> </body></html> </div> <div class="revisedby"> <p> Last revised on December 25, 2023 at 00:59:01. See the <a href="/nlab/history/preorder" 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/preorder" accesskey="E" class="navlink" id="edit" rel="nofollow">Edit</a><a href="https://nforum.ncatlab.org/discussion/14836/#Item_4">Discuss</a><span class="backintime"><a href="/nlab/revision/preorder/68" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/diff/preorder" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Changes from previous revision</a><a href="/nlab/history/preorder" accesskey="S" class="navlink" id="history" rel="nofollow">History (68 revisions)</a> <a href="/nlab/show/preorder/cite" style="color: black">Cite</a> <a href="/nlab/print/preorder" accesskey="p" id="view_print" rel="nofollow">Print</a> <a href="/nlab/source/preorder" id="view_source" rel="nofollow">Source</a> </div> </div>  </div>  </body> </html>