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> extensional relation in nLab </title> <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /> <meta name="robots" content="index,follow" /> <meta name="viewport" content="width=device-width, initial-scale=1" /> <link href="/stylesheets/instiki.css?1676280126" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/mathematics.css?1660229990" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/syntax.css?1660229990" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/nlab.css?1676280126" media="all" rel="stylesheet" type="text/css" /> <link rel="stylesheet" type="text/css" href="https://cdn.jsdelivr.net/gh/dreampulse/computer-modern-web-font@master/fonts.css"/> <style type="text/css"> h1#pageName, div.info, .newWikiWord a, a.existingWikiWord, .newWikiWord a:hover, [actiontype="toggle"]:hover, #TextileHelp h3 { color: #226622; } a:visited.existingWikiWord { color: #164416; } </style> <style type="text/css"><![CDATA[/*></style> <script src="/javascripts/prototype.js?1660229990" type="text/javascript"></script> <script src="/javascripts/effects.js?1660229990" type="text/javascript"></script> <script src="/javascripts/dragdrop.js?1660229990" type="text/javascript"></script> <script src="/javascripts/controls.js?1660229990" type="text/javascript"></script> <script src="/javascripts/application.js?1660229990" type="text/javascript"></script> <script src="/javascripts/page_helper.js?1660229990" type="text/javascript"></script> <script src="/javascripts/thm_numbering.js?1660229990" type="text/javascript"></script> <script type="text/x-mathjax-config"> <![CDATA[//><!]]> </script> <script type="text/javascript"> <![CDATA[//><!]]> </script> <link href="https://ncatlab.org/nlab/atom_with_headlines" rel="alternate" title="Atom with headlines" type="application/atom+xml" /> <link href="https://ncatlab.org/nlab/atom_with_content" rel="alternate" title="Atom with full content" type="application/atom+xml" /> <script type="text/javascript"> document.observe("dom:loaded", function() { generateThmNumbers(); }); </script> </head> <body> <div id="Container"> <div id="Content"> <h1 id="pageName"> <span style="float: left; margin: 0.5em 0.25em -0.25em 0"> <svg xmlns="http://www.w3.org/2000/svg" width="1.872em" height="1.8em" viewBox="0 0 190 181"> <path fill="#226622" d="M72.8 145c-1.6 17.3-15.7 10-23.6 20.2-5.6 7.3 4.8 15 11.4 15 11.5-.2 19-13.4 26.4-20.3 3.3-3 8.2-4 11.2-7.2a14 14 0 0 0 2.9-11.1c-1.4-9.6-12.4-18.6-16.9-27.2-5-9.6-10.7-27.4-24.1-27.7-17.4-.3-.4 26 4.7 30.7 2.4 2.3 5.4 4.1 7.3 6.9 1.6 2.3 2.1 5.8-1 7.2-5.9 2.6-12.4-6.3-15.5-10-8.8-10.6-15.5-23-26.2-31.8-5.2-4.3-11.8-8-18-3.7-7.3 4.9-4.2 12.9.2 18.5a81 81 0 0 0 30.7 23c3.3 1.5 12.8 5.6 10 10.7-2.5 5.2-11.7 3-15.6 1.1-8.4-3.8-24.3-21.3-34.4-13.7-3.5 2.6-2.3 7.6-1.2 11.1 2.8 9 12.2 17.2 20.9 20.5 17.3 6.7 34.3-8 50.8-12.1z"/> <path fill="#a41e32" d="M145.9 121.3c-.2-7.5 0-19.6-4.5-26-5.4-7.5-12.9-1-14.1 5.8-1.4 7.8 2.7 14.1 4.8 21.3 3.4 12 5.8 29-.8 40.1-3.6-6.7-5.2-13-7-20.4-2.1-8.2-12.8-13.2-15.1-1.9-2 9.7 9 21.2 12 30.1 1.2 4 2 8.8 6.4 10.3 6.9 2.3 13.3-4.7 17.7-8.8 12.2-11.5 36.6-20.7 43.4-36.4 6.7-15.7-13.7-14-21.3-7.2-9.1 8-11.9 20.5-23.6 25.1 7.5-23.7 31.8-37.6 38.4-61.4 2-7.3-.8-29.6-13-19.8-14.5 11.6-6.6 37.6-23.3 49.2z"/> <path fill="#193c78" d="M86.3 47.5c0-13-10.2-27.6-5.8-40.4 2.8-8.4 14.1-10.1 17-1 3.8 11.6-.3 26.3-1.8 38 11.7-.7 10.5-16 14.8-24.3 2.1-4.2 5.7-9.1 11-6.7 6 2.7 7.4 9.2 6.6 15.1-2.2 14-12.2 18.8-22.4 27-3.4 2.7-8 6.6-5.9 11.6 2 4.4 7 4.5 10.7 2.8 7.4-3.3 13.4-16.5 21.7-16 14.6.7 12 21.9.9 26.2-5 1.9-10.2 2.3-15.2 3.9-5.8 1.8-9.4 8.7-15.7 8.9-6.1.1-9-6.9-14.3-9-14.4-6-33.3-2-44.7-14.7-3.7-4.2-9.6-12-4.9-17.4 9.3-10.7 28 7.2 35.7 12 2 1.1 11 6.9 11.4 1.1.4-5.2-10-8.2-13.5-10-11.1-5.2-30-15.3-35-27.3-2.5-6 2.8-13.8 9.4-13.6 6.9.2 13.4 7 17.5 12C70.9 34 75 43.8 86.3 47.4z"/> </svg> </span> <span class="webName">nLab</span> extensional relation </h1> <div class="navigation"> <span class="skipNav"><a href='#navEnd'>Skip the Navigation Links</a> | </span> <span style="display:inline-block; width: 0.3em;"></span> <a href="/nlab/show/HomePage" accesskey="H" title="Home page">Home Page</a> | <a href="/nlab/all_pages" accesskey="A" title="List of all pages">All Pages</a> | <a href="/nlab/latest_revisions" accesskey="U" title="Latest edits and page creations">Latest Revisions</a> | <a href="https://nforum.ncatlab.org/discussion/15297/#Item_7" 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>Extensional relations</title></head> <body> <div class="rightHandSide"> <div class="toc clickDown" tabindex="0"> <h3 id="context">Context</h3> <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> </div> </div> <h1 id="extensional_relations">Extensional relations</h1> <div class='maruku_toc'> <ul> <li><a href='#idea'>Idea</a></li> <li><a href='#definitions'>Definitions</a></li> <ul> <li><a href='#weak_extensionality'>Weak extensionality</a></li> <li><a href='#finsler_extensionality'>Finsler extensionality</a></li> <li><a href='#scott_extensionality'>Scott extensionality</a></li> <li><a href='#strong_extensionality'>Strong extensionality</a></li> <li><a href='#weak_extensionality_for_arbitrary_binary_relations'>Weak extensionality for arbitrary binary relations</a></li> <li><a href='#in_homotopy_type_theory'>In homotopy type theory</a></li> </ul> <li><a href='#examples'>Examples</a></li> <li><a href='#extensional_quotients'>Extensional quotients</a></li> <li><a href='#simulations'>Simulations</a></li> <li><a href='#references'>References</a></li> </ul> </div> <h2 id="idea">Idea</h2> <p>Given an extensional 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">\prec</annotation></semantics></math> on a set, two elements are equal if they cannot be distinguished by the structure of the set of elements that they are related to, that those elements are related to, and so on forever in one direction. We generally think of <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 \prec y</annotation></semantics></math> as saying 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> is a ‘member’ of <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>, so that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≺</mo></mrow><annotation encoding="application/x-tex">\prec</annotation></semantics></math> is extensional when “<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> is determined by its members” as in the <a class="existingWikiWord" href="/nlab/show/axiom+of+extensionality">axiom of extensionality</a> for material <a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a>.</p> <h2 id="definitions">Definitions</h2> <p>We begin with the historically first definition, which is correct for <a class="existingWikiWord" href="/nlab/show/well-founded+relations">well-founded relations</a>. We then consider ways to extend this to more general relations, where the last version seems to be most correct.</p> <h3 id="weak_extensionality">Weak extensionality</h3> <p>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">\prec</annotation></semantics></math> 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 <strong>weakly extensional</strong> if, given any elements <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> of <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>, <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> whenever (for all <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>t</mi></mrow><annotation encoding="application/x-tex">t</annotation></semantics></math>) <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>t</mi><mo>≺</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">t \prec x</annotation></semantics></math> if and only if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>t</mi><mo>≺</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">t \prec y</annotation></semantics></math>.</p> <p>Interpreting <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≺</mo></mrow><annotation encoding="application/x-tex">\prec</annotation></semantics></math> as membership <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∈</mo></mrow><annotation encoding="application/x-tex">\in</annotation></semantics></math>, this corresponds to the <a class="existingWikiWord" href="/nlab/show/axiom+of+extensionality">axiom of extensionality</a> as usually stated for <a class="existingWikiWord" href="/nlab/show/pure+sets">pure sets</a>. However, it is really only appropriate when <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≺</mo></mrow><annotation encoding="application/x-tex">\prec</annotation></semantics></math> is <a class="existingWikiWord" href="/nlab/show/well-founded+relation">well-founded</a>, just as the usual axiom of extensionality must be strengthened in the absence of the <a class="existingWikiWord" href="/nlab/show/axiom+of+foundation">axiom of foundation</a>.</p> <p>However, when <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≺</mo></mrow><annotation encoding="application/x-tex">\prec</annotation></semantics></math> is well-founded, weak extensionality is equivalent to all the stronger notions below; thus in that case it is usually called just <strong>extensionality</strong>.</p> <h3 id="finsler_extensionality">Finsler extensionality</h3> <p>Let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mo>≺</mo> <mo>*</mo></msup></mrow><annotation encoding="application/x-tex">\prec^*</annotation></semantics></math> be the reflexive-<a class="existingWikiWord" href="/nlab/show/transitive+closure">transitive closure</a> of 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">\prec</annotation></semantics></math> on <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> (so <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mo>≺</mo> <mo>*</mo></msup></mrow><annotation encoding="application/x-tex">\prec^*</annotation></semantics></math> is a <a class="existingWikiWord" href="/nlab/show/preorder">preorder</a>). Given an element <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> of <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>, let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi><msup><mo stretchy="false">↓</mo> <mo>*</mo></msup><mi>y</mi></mrow><annotation encoding="application/x-tex">S \downarrow^* y</annotation></semantics></math> be the <a class="existingWikiWord" href="/nlab/show/downset">downset</a> of <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> under <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mo>≺</mo> <mo>*</mo></msup></mrow><annotation encoding="application/x-tex">\prec^*</annotation></semantics></math>:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>S</mi><msup><mo stretchy="false">↓</mo> <mo>*</mo></msup><mi>y</mi><mo>=</mo><mo stretchy="false">{</mo><mi>x</mi><mo>:</mo><mi>S</mi><mspace width="thickmathspace"></mspace><mo stretchy="false">|</mo><mspace width="thickmathspace"></mspace><mi>x</mi><mo>=</mo><msub><mi>t</mi> <mn>0</mn></msub><mo>≺</mo><mi>⋯</mi><mo>≺</mo><msub><mi>t</mi> <mi>n</mi></msub><mo>=</mo><mi>y</mi><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex"> S \downarrow^* y = \{ x: S \;|\; x = t_0 \prec \cdots \prec t_n = y \} </annotation></semantics></math></div> <p>with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>n</mi><mo>≥</mo><mn>0</mn></mrow><annotation encoding="application/x-tex">n \geq 0</annotation></semantics></math>. Note that <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> itself belongs to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi><msup><mo stretchy="false">↓</mo> <mo>*</mo></msup><mi>y</mi></mrow><annotation encoding="application/x-tex">S \downarrow^* y</annotation></semantics></math> (through <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>n</mi><mo>=</mo><mn>0</mn></mrow><annotation encoding="application/x-tex">n = 0</annotation></semantics></math>, if in no other way), so we may take it to be a <a class="existingWikiWord" href="/nlab/show/pointed+set">pointed set</a>. Then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≺</mo></mrow><annotation encoding="application/x-tex">\prec</annotation></semantics></math> is <strong>Finsler-extensional</strong> if it is weakly extensional and, given any elements <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> of <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>, <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> whenever <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi><msup><mo stretchy="false">↓</mo> <mo>*</mo></msup><mi>x</mi></mrow><annotation encoding="application/x-tex">S \downarrow^* x</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi><msup><mo stretchy="false">↓</mo> <mo>*</mo></msup><mi>y</mi></mrow><annotation encoding="application/x-tex">S \downarrow^* y</annotation></semantics></math> are isomorphic as pointed sets equipped 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">\prec</annotation></semantics></math>.</p> <p>Note that this definition includes weak extensionality, which won't follow from the other half unless <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≺</mo></mrow><annotation encoding="application/x-tex">\prec</annotation></semantics></math> is well-founded (see the examples below). It is possible to get weak extensionality free by using the <a class="existingWikiWord" href="/nlab/show/transitive+closure">transitive closure</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mo>≺</mo> <mo>+</mo></msup></mrow><annotation encoding="application/x-tex">\prec^+</annotation></semantics></math> instead; that is, define <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi><msup><mo stretchy="false">↓</mo> <mo>+</mo></msup><mi>y</mi></mrow><annotation encoding="application/x-tex">S \downarrow^+ y</annotation></semantics></math> with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>n</mi><mo>></mo><mn>0</mn></mrow><annotation encoding="application/x-tex">n \gt 0</annotation></semantics></math> only. But then you need another step; define <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>S</mi><msup><mo stretchy="false">↓</mo> <mo>+</mo></msup><mi>y</mi><msup><mo stretchy="false">)</mo> <mo>⊤</mo></msup></mrow><annotation encoding="application/x-tex">(S \downarrow^+ y)^\top</annotation></semantics></math> to be a pointed set with a new point <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊤</mo></mrow><annotation encoding="application/x-tex">\top</annotation></semantics></math> adjoined to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi><msup><mo stretchy="false">↓</mo> <mo>+</mo></msup><mi>y</mi></mrow><annotation encoding="application/x-tex">S \downarrow^+ y</annotation></semantics></math>; let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>≺</mo><mo>⊤</mo></mrow><annotation encoding="application/x-tex">x \prec \top</annotation></semantics></math> if and only 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 \prec y</annotation></semantics></math> in <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> itself. (For a well-founded relation, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>S</mi><msup><mo stretchy="false">↓</mo> <mo>+</mo></msup><mi>y</mi><msup><mo stretchy="false">)</mo> <mo>⊤</mo></msup><mo>≅</mo><mi>S</mi><msup><mo stretchy="false">↓</mo> <mo>*</mo></msup><mi>y</mi></mrow><annotation encoding="application/x-tex">(S \downarrow^+ y)^\top \cong S \downarrow^* y</annotation></semantics></math>; in general, however, <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> may already belong to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi><msup><mo stretchy="false">↓</mo> <mo>+</mo></msup><mi>y</mi></mrow><annotation encoding="application/x-tex">S \downarrow^+ y</annotation></semantics></math>, yet <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>≠</mo><mo>⊤</mo></mrow><annotation encoding="application/x-tex">y \ne \top</annotation></semantics></math> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>S</mi><msup><mo stretchy="false">↓</mo> <mo>+</mo></msup><mi>y</mi><msup><mo stretchy="false">)</mo> <mo>⊤</mo></msup></mrow><annotation encoding="application/x-tex">(S \downarrow^+ y)^\top</annotation></semantics></math>.) Then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≺</mo></mrow><annotation encoding="application/x-tex">\prec</annotation></semantics></math> is Finsler-extensional on <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> if and only 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 = y</annotation></semantics></math> whenever <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>S</mi><msup><mo stretchy="false">↓</mo> <mo>+</mo></msup><mi>x</mi><msup><mo stretchy="false">)</mo> <mo>⊤</mo></msup><mo>≅</mo><mo stretchy="false">(</mo><mi>S</mi><msup><mo stretchy="false">↓</mo> <mo>+</mo></msup><mi>y</mi><msup><mo stretchy="false">)</mo> <mo>⊤</mo></msup></mrow><annotation encoding="application/x-tex">(S \downarrow^+ x)^\top \cong (S \downarrow^+ y)^\top</annotation></semantics></math> as pointed sets equipped with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≺</mo></mrow><annotation encoding="application/x-tex">\prec</annotation></semantics></math>.</p> <p>It is immediate that Finsler extensionality implies weak extensionality; the converse may be proved (using <a class="existingWikiWord" href="/nlab/show/induction">induction</a>) for well-founded relations.</p> <h3 id="scott_extensionality">Scott extensionality</h3> <p>Given an element <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> of <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>, let a <strong>path</strong> 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> consist of a sequence</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>=</mo><msub><mi>t</mi> <mn>0</mn></msub><mo>≺</mo><mi>⋯</mi><mo>≺</mo><msub><mi>t</mi> <mi>n</mi></msub><mo>=</mo><mi>y</mi></mrow><annotation encoding="application/x-tex"> x = t_0 \prec \cdots \prec t_n = y </annotation></semantics></math></div> <p>for <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>n</mi><mo>≥</mo><mn>0</mn></mrow><annotation encoding="application/x-tex">n \geq 0</annotation></semantics></math>. Then let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>T</mi> <mi>y</mi></msub></mrow><annotation encoding="application/x-tex">T_y</annotation></semantics></math> be the set of paths 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>; given paths <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mover><mi>t</mi><mo stretchy="false">→</mo></mover></mrow><annotation encoding="application/x-tex">\vec{t}</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mover><mi>u</mi><mo stretchy="false">→</mo></mover></mrow><annotation encoding="application/x-tex">\vec{u}</annotation></semantics></math> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>N</mi> <mi>y</mi></msub></mrow><annotation encoding="application/x-tex">N_y</annotation></semantics></math>, say that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mover><mi>t</mi><mo stretchy="false">→</mo></mover><mo>→</mo><mover><mi>u</mi><mo stretchy="false">→</mo></mover></mrow><annotation encoding="application/x-tex">\vec{t} \to \vec{u}</annotation></semantics></math> if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mover><mi>u</mi><mo stretchy="false">→</mo></mover><mo>=</mo><mo stretchy="false">(</mo><msub><mi>t</mi> <mn>1</mn></msub><mo>,</mo><mi>…</mi><mo>,</mo><msub><mi>t</mi> <mi>m</mi></msub><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\vec{u} = (t_1, \ldots, t_m)</annotation></semantics></math> for some <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>m</mi><mo>≤</mo><mi>n</mi></mrow><annotation encoding="application/x-tex">m \leq n</annotation></semantics></math>. Then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>T</mi> <mi>y</mi></msub></mrow><annotation encoding="application/x-tex">T_y</annotation></semantics></math> with 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">\to</annotation></semantics></math> is the <strong>tree</strong> 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> <p><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 <strong>Scott-extensional</strong> if the only <a class="existingWikiWord" href="/nlab/show/automorphism">automorphism</a> of any such tree <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>T</mi> <mi>y</mi></msub></mrow><annotation encoding="application/x-tex">T_y</annotation></semantics></math> (as a set equipped 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">\to</annotation></semantics></math>) is 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><msub><mi>T</mi> <mi>y</mi></msub></mrow><annotation encoding="application/x-tex">T_y</annotation></semantics></math>.</p> <p>Then Scott extensionality implies Finsler extensionality, and the converse holds for well-founded relations.</p> <h3 id="strong_extensionality">Strong extensionality</h3> <p>The strongest version of extensionality is motivated by the study of <a class="existingWikiWord" href="/nlab/show/terminal+coalgebra">terminal coalgebra</a>s and <a class="existingWikiWord" href="/nlab/show/coinduction">coinduction</a>.</p> <p>Let <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> be equipped with a binary 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">\prec</annotation></semantics></math>. A <strong><a class="existingWikiWord" href="/nlab/show/bisimulation">bisimulation</a></strong> on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>S</mi><mo>,</mo><mo>≺</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(S,\prec)</annotation></semantics></math> is a binary 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">\sim</annotation></semantics></math> such that whenever <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 \sim y</annotation></semantics></math>, for any <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>≺</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">a \prec x</annotation></semantics></math> there is a <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi><mo>≺</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">b \prec y</annotation></semantics></math> with <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 \sim b</annotation></semantics></math>, and conversely for every <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi><mo>≺</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">b \prec y</annotation></semantics></math> there is an <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>≺</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">a \prec x</annotation></semantics></math> with again <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 \sim b</annotation></semantics></math>. We then say that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≺</mo></mrow><annotation encoding="application/x-tex">\prec</annotation></semantics></math> is <strong>strongly extensional</strong> if every bisimulation is contained in the identity relation; i.e., <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> whenever <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 \sim y</annotation></semantics></math> for any bisimulation <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>. In general, this is probably the best situation in which to say that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≺</mo></mrow><annotation encoding="application/x-tex">\prec</annotation></semantics></math> is simply <strong>extensional</strong>.</p> <p>Finsler and Scott extensionality may be understood as special cases of this for particular bisimulations <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>. (So can strong extensionality, since any set equipped with a relation has a weakest bisimulation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≈</mo></mrow><annotation encoding="application/x-tex">\approx</annotation></semantics></math>.) This is the approach taken by Aczel to study all the above notions of extensionality together.</p> <p>In particular, strong extensionality implies Scott extensionality, and the converse holds for well-founded relations. Thus, all forms of extensionality are equivalent for well-founded relations.</p> <h3 id="weak_extensionality_for_arbitrary_binary_relations">Weak extensionality for arbitrary binary relations</h3> <p>Given sets <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math>, let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≺</mo></mrow><annotation encoding="application/x-tex">\prec</annotation></semantics></math> be a binary relation 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> 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>, or equivalently, a <a class="existingWikiWord" href="/nlab/show/predicate">predicate</a> on the cartesian product <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 \times B</annotation></semantics></math>. Then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≺</mo></mrow><annotation encoding="application/x-tex">\prec</annotation></semantics></math> is (weakly) extensional if, given any elements <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> of <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>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><msub><mo>=</mo> <mi>B</mi></msub><mi>y</mi></mrow><annotation encoding="application/x-tex">x =_B y</annotation></semantics></math> whenever for all <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>t</mi><mo>:</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">t:A</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>t</mi><mo>≺</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">t \prec x</annotation></semantics></math> if and only if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>t</mi><mo>≺</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">t \prec y</annotation></semantics></math>.</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo>∀</mo><mi>x</mi><mo>:</mo><mi>B</mi><mo>.</mo><mo>∀</mo><mi>y</mi><mo>:</mo><mi>B</mi><mo>.</mo><mo stretchy="false">(</mo><mi>x</mi><msub><mo>=</mo> <mi>B</mi></msub><mi>y</mi><mo stretchy="false">)</mo><mo>⇔</mo><mo>∀</mo><mi>t</mi><mo>:</mo><mi>A</mi><mo>.</mo><mo stretchy="false">(</mo><mi>t</mi><mo>≺</mo><mi>x</mi><mo stretchy="false">)</mo><mo>⇔</mo><mo stretchy="false">(</mo><mi>t</mi><mo>≺</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\forall x:B.\forall y:B.(x =_B y) \iff \forall t:A.(t \prec x) \iff (t \prec y)</annotation></semantics></math></div> <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>, a relation is an <a class="existingWikiWord" href="/nlab/show/h-proposition">h-proposition</a>-valued <a class="existingWikiWord" href="/nlab/show/type+family">type family</a>. A binary 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">\prec</annotation></semantics></math> on a carrier type <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 <strong>weakly extensional</strong> if for all terms <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>:</mo><mi>S</mi></mrow><annotation encoding="application/x-tex">a:S</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi><mo>:</mo><mi>S</mi></mrow><annotation encoding="application/x-tex">b:S</annotation></semantics></math> the canonical function</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">idtoextcond</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><mo>:</mo><mo stretchy="false">(</mo><mi>a</mi><msub><mo>=</mo> <mi>S</mi></msub><mi>b</mi><mo stretchy="false">)</mo><mo>→</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo> <mrow><mi>c</mi><mo>:</mo><mi>S</mi></mrow></munder><mo stretchy="false">(</mo><mi>c</mi><mo>≺</mo><mi>a</mi><mo stretchy="false">)</mo><mo>≃</mo><mo stretchy="false">(</mo><mi>c</mi><mo>≺</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathrm{idtoextcond}(a, b):(a =_S b) \to \prod_{c:S} (c \prec a) \simeq (c \prec b)</annotation></semantics></math></div> <p>is an <a class="existingWikiWord" href="/nlab/show/equivalence+of+types">equivalence of types</a>. This implies that the type <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 an <a class="existingWikiWord" href="/nlab/show/h-set">h-set</a>.</p> <h2 id="examples">Examples</h2> <ul> <li> <p>The <a class="existingWikiWord" href="/nlab/show/axiom+of+extensionality">axiom of extensionality</a> in material <a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a> states membership is an extensional relation on the class of <a class="existingWikiWord" href="/nlab/show/pure+sets">pure sets</a>. (Note that the <a class="existingWikiWord" href="/nlab/show/axiom+of+foundation">axiom of foundation</a> states that membership is a well-founded relation, so one usually doesn't worry about the different notions of extensionality for ill-founded relations.) More generally, the membership relation on the <a class="existingWikiWord" href="/nlab/show/transitive+closure">transitive closure</a> or reflexive-transitive closure of a pure set is an extensional relation on a set.</p> </li> <li> <p>Conversely, one can <em>define</em> <a class="existingWikiWord" href="/nlab/show/pure+set">pure set</a>s in <em>structural</em> <a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a> in part as sets equipped with an extensional (and optionally well-founded) relation.</p> </li> <li> <p>In any <a class="existingWikiWord" href="/nlab/show/single-sorted+definition+of+a+category">single-sorted definition</a> of a <a class="existingWikiWord" href="/nlab/show/topos">topos</a>, there is a <a class="existingWikiWord" href="/nlab/show/terminal+object">terminal object</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>1</mn></mrow><annotation encoding="application/x-tex">1</annotation></semantics></math> (represented by the <a class="existingWikiWord" href="/nlab/show/identity+morphism">identity morphism</a> of the terminal object), one could define 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">\prec</annotation></semantics></math> on the set of morphisms <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> as</p> </li> </ul> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>≺</mo><mi>b</mi><mo>≔</mo><mi>s</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo><mo>=</mo><mn>1</mn><mo>∧</mo><mi>t</mi><mo stretchy="false">(</mo><mi>b</mi><mo stretchy="false">)</mo><mo>=</mo><mn>1</mn><mo>∧</mo><mi>t</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo><mo>=</mo><mi>s</mi><mo stretchy="false">(</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">a \prec b \coloneqq s(a) = 1 \wedge t(b) = 1 \wedge t(a) = s(b)</annotation></semantics></math></div> <p>Due to the <a class="existingWikiWord" href="/nlab/show/universal+property">universal property</a> of the <a class="existingWikiWord" href="/nlab/show/terminal+object">terminal object</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">\prec</annotation></semantics></math> is weakly extensional. However, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≺</mo></mrow><annotation encoding="application/x-tex">\prec</annotation></semantics></math> is not strongly extensional. 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">\sim</annotation></semantics></math> defined by equality on every pair of functions <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><mo>=</mo><mi>b</mi></mrow><annotation encoding="application/x-tex">a \sim b \coloneqq a = b</annotation></semantics></math>, and in addition, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi mathvariant="normal">id</mi> <mn>2</mn></msub><mo>∼</mo><mi mathvariant="normal">swap</mi></mrow><annotation encoding="application/x-tex">\mathrm{id}_2 \sim \mathrm{swap}</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">swap</mi><mo>∼</mo><msub><mi mathvariant="normal">id</mi> <mn>2</mn></msub></mrow><annotation encoding="application/x-tex">\mathrm{swap} \sim \mathrm{id}_2</annotation></semantics></math> for the identity function and the swap function on the set with two elements <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>2</mn></mrow><annotation encoding="application/x-tex">2</annotation></semantics></math>, is a bisimulation on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≺</mo></mrow><annotation encoding="application/x-tex">\prec</annotation></semantics></math>, but it is not true that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi mathvariant="normal">id</mi> <mn>2</mn></msub><mo>=</mo><mi mathvariant="normal">swap</mi></mrow><annotation encoding="application/x-tex">\mathrm{id}_2 = \mathrm{swap}</annotation></semantics></math>.</p> <ul> <li>In any <a class="existingWikiWord" href="/nlab/show/single-sorted+definition+of+a+category">single-sorted definition</a> of a <a class="existingWikiWord" href="/nlab/show/topos">topos</a>, there is also an <a class="existingWikiWord" href="/nlab/show/initial+object">initial object</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>0</mn></mrow><annotation encoding="application/x-tex">0</annotation></semantics></math> (represented by the <a class="existingWikiWord" href="/nlab/show/identity+morphism">identity morphism</a> of the initial object). One could define 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">\in</annotation></semantics></math> on the set of morphisms <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> as</li> </ul> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∈</mo><mi>b</mi><mo>≔</mo><mi>s</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo><mo>=</mo><mn>1</mn><mo>∧</mo><mi>s</mi><mo stretchy="false">(</mo><mi>b</mi><mo stretchy="false">)</mo><mo>=</mo><mn>0</mn><mo>∧</mo><mi>t</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo><mo>=</mo><mi>t</mi><mo stretchy="false">(</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">a \in b \coloneqq s(a) = 1 \wedge s(b) = 0 \wedge t(a) = t(b)</annotation></semantics></math></div> <p>Due to the <a class="existingWikiWord" href="/nlab/show/universal+property">universal property</a> of the <a class="existingWikiWord" href="/nlab/show/initial+object">initial object</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">\in</annotation></semantics></math> is weakly extensional. However, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∈</mo></mrow><annotation encoding="application/x-tex">\in</annotation></semantics></math> is not strongly extensional, for the same reason that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≺</mo></mrow><annotation encoding="application/x-tex">\prec</annotation></semantics></math> defined above is not strongly extensional.</p> <ul> <li> <p>A <a class="existingWikiWord" href="/nlab/show/well-order">well-order</a> is precisely a well-founded, <a class="existingWikiWord" href="/nlab/show/transitive+relation">transitive</a>, extensional relation. Removing well-foundedness here gives a theory of ill-founded <a class="existingWikiWord" href="/nlab/show/ordinal+number">ordinal number</a>s.</p> </li> <li> <p>On the set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mn>2</mn></mstyle><mo>=</mo><mo stretchy="false">{</mo><mn>0</mn><mo>,</mo><mn>1</mn><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\mathbf{2} = \{0,1\}</annotation></semantics></math>, now let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>0</mn><mo>≺</mo><mn>0</mn></mrow><annotation encoding="application/x-tex">0 \prec 0</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>0</mn><mo>≺</mo><mn>1</mn></mrow><annotation encoding="application/x-tex">0 \prec 1</annotation></semantics></math> (but no other relationships). This relation is not weakly extensional, although it does satisfy the other half of Finsler extensionality, since <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mn>2</mn></mstyle><msup><mo stretchy="false">↓</mo> <mo>*</mo></msup><mn>0</mn><mo>≇</mo><mstyle mathvariant="bold"><mn>2</mn></mstyle><msup><mo stretchy="false">↓</mo> <mo>*</mo></msup><mn>1</mn></mrow><annotation encoding="application/x-tex">\mathbf{2} \downarrow^* 0 \ncong \mathbf{2} \downarrow^* 1</annotation></semantics></math>. However, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mstyle mathvariant="bold"><mn>2</mn></mstyle><msup><mo stretchy="false">↓</mo> <mo>+</mo></msup><mn>0</mn><msup><mo stretchy="false">)</mo> <mo>⊤</mo></msup><mo>≅</mo><mo stretchy="false">(</mo><mstyle mathvariant="bold"><mn>2</mn></mstyle><msup><mo stretchy="false">↓</mo> <mo>+</mo></msup><mn>1</mn><msup><mo stretchy="false">)</mo> <mo>⊤</mo></msup></mrow><annotation encoding="application/x-tex">(\mathbf{2} \downarrow^+ 0)^\top \cong (\mathbf{2} \downarrow^+ 1)^\top</annotation></semantics></math>; this shows the necessity of defining Finsler extensionality as we do.</p> </li> <li> <p>On the set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mn>2</mn></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{2}</annotation></semantics></math> again, let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>0</mn><mo>≺</mo><mn>1</mn></mrow><annotation encoding="application/x-tex">0 \prec 1</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>1</mn><mo>≺</mo><mn>0</mn></mrow><annotation encoding="application/x-tex">1 \prec 0</annotation></semantics></math> (but <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>0</mn><mo>⊀</mo><mn>0</mn></mrow><annotation encoding="application/x-tex">0 \nprec 0</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>1</mn><mo>⊀</mo><mn>1</mn></mrow><annotation encoding="application/x-tex">1 \nprec 1</annotation></semantics></math>). This relation is weakly extensional but not Finsler-extensional, since <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mn>2</mn></mstyle><msup><mo stretchy="false">↓</mo> <mo>*</mo></msup><mn>0</mn><mo>≅</mo><mstyle mathvariant="bold"><mn>2</mn></mstyle><msup><mo stretchy="false">↓</mo> <mo>*</mo></msup><mn>1</mn></mrow><annotation encoding="application/x-tex">\mathbf{2} \downarrow^* 0 \cong \mathbf{2} \downarrow^* 1</annotation></semantics></math>. Yet <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>0</mn></mrow><annotation encoding="application/x-tex">0</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>1</mn></mrow><annotation encoding="application/x-tex">1</annotation></semantics></math> can hardly be distinguished by <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≺</mo></mrow><annotation encoding="application/x-tex">\prec</annotation></semantics></math> when there is an <a class="existingWikiWord" href="/nlab/show/automorphism">automorphism</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mstyle mathvariant="bold"><mn>2</mn></mstyle><mo>,</mo><mo>≺</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(\mathbf{2},\prec)</annotation></semantics></math> that swaps them; this and the other examples below motivate the stronger notions of extensionality.</p> </li> <li> <p>On the set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mn>3</mn></mstyle><mo>=</mo><mo stretchy="false">{</mo><mn>0</mn><mo>,</mo><mn>1</mn><mo>,</mo><mn>2</mn><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\mathbf{3} = \{0,1,2\}</annotation></semantics></math>, let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>2</mn><mo>⊀</mo><mn>0</mn></mrow><annotation encoding="application/x-tex">2 \nprec 0</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>i</mi><mo>⊀</mo><mi>i</mi></mrow><annotation encoding="application/x-tex">i \nprec i</annotation></semantics></math> but all other relationships hold. Then this relation is Finsler-extensional but not Scott-extensional, since <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>T</mi> <mn>2</mn></msub><mo>≅</mo><msub><mi>T</mi> <mn>1</mn></msub></mrow><annotation encoding="application/x-tex">T_2 \cong T_1</annotation></semantics></math>.</p> </li> <li> <p>Finally, on the set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mn>2</mn></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{2}</annotation></semantics></math> again, let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>1</mn><mo>⊀</mo><mn>0</mn></mrow><annotation encoding="application/x-tex">1 \nprec 0</annotation></semantics></math> but all other relationships hold. Then this relation is Scott-extensional but not strongly extensional, since <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>0</mn><mo>≈</mo><mn>1</mn></mrow><annotation encoding="application/x-tex">0 \approx 1</annotation></semantics></math>.</p> </li> </ul> <h2 id="extensional_quotients">Extensional quotients</h2> <p>Weak extensionality is a kind of <a class="existingWikiWord" href="/nlab/show/antisymmetric+relation">antisymmetry</a> condition: Let <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> mean that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>t</mi><mo>≺</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">t \prec y</annotation></semantics></math> whenever <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>t</mi><mo>≺</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">t \prec x</annotation></semantics></math>. Then <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 clearly a <a class="existingWikiWord" href="/nlab/show/preorder">preorder</a>, which is antisymmetric (so a <a class="existingWikiWord" href="/nlab/show/partial+order">partial order</a>) if and only if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≺</mo></mrow><annotation encoding="application/x-tex">\prec</annotation></semantics></math> is weakly extensional.</p> <p>Now suppose that if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>t</mi><mo>≺</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">t \prec x</annotation></semantics></math> if and only if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>t</mi><mo>≺</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">t \prec y</annotation></semantics></math> for all <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>t</mi></mrow><annotation encoding="application/x-tex">t</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>≺</mo><mi>z</mi></mrow><annotation encoding="application/x-tex">x \prec z</annotation></semantics></math> if and only if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>≺</mo><mi>z</mi></mrow><annotation encoding="application/x-tex">y \prec z</annotation></semantics></math> for all <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>z</mi></mrow><annotation encoding="application/x-tex">z</annotation></semantics></math>. Then if we define <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 \equiv y</annotation></semantics></math> to mean 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>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≡</mo></mrow><annotation encoding="application/x-tex">\equiv</annotation></semantics></math> is an equivalence relation such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≺</mo></mrow><annotation encoding="application/x-tex">\prec</annotation></semantics></math> descends to a weakly extensional relation on the <a class="existingWikiWord" href="/nlab/show/quotient+set">quotient set</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi><mo stretchy="false">/</mo><mo>≡</mo></mrow><annotation encoding="application/x-tex">S/{\equiv}</annotation></semantics></math>.</p> <p>Strongly extensional quotients are even easier to construct, although they do create additional relationships. It is easy to see that the union of any family of bisimulations is a bisimulation, and therefore there is a largest bisimulation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≈</mo></mrow><annotation encoding="application/x-tex">\approx</annotation></semantics></math> for any binary 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">\prec</annotation></semantics></math> on <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>. Moreover, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≈</mo></mrow><annotation encoding="application/x-tex">\approx</annotation></semantics></math> is an equivalence relation (though not every bisimulation need be so), and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≺</mo></mrow><annotation encoding="application/x-tex">\prec</annotation></semantics></math> descends to a strongly extensional relation on the quotient <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi><mo stretchy="false">/</mo><mo>≈</mo></mrow><annotation encoding="application/x-tex">S/\approx</annotation></semantics></math>.</p> <h2 id="simulations">Simulations</h2> <p>Given two sets <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> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi></mrow><annotation encoding="application/x-tex">T</annotation></semantics></math>, each equipped with a strongly extensional 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">\prec</annotation></semantics></math>, a <a class="existingWikiWord" href="/nlab/show/function">function</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo lspace="verythinmathspace">:</mo><mi>S</mi><mo>→</mo><mi>T</mi></mrow><annotation encoding="application/x-tex">f\colon S \to T</annotation></semantics></math> is a <strong><a class="existingWikiWord" href="/nlab/show/simulation">simulation</a></strong> of <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> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi></mrow><annotation encoding="application/x-tex">T</annotation></semantics></math> if</p> <ul> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>≺</mo><mi>f</mi><mo stretchy="false">(</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f(x) \prec f(y)</annotation></semantics></math> whenever <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 \prec y</annotation></semantics></math> and</li> <li>given <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>t</mi><mo>≺</mo><mi>f</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">t \prec f(x)</annotation></semantics></math>, there exists <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 \prec x</annotation></semantics></math> with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>t</mi><mo>=</mo><mi>f</mi><mo stretchy="false">(</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">t = f(y)</annotation></semantics></math>.</li> </ul> <p>Then sets so equipped form a <a class="existingWikiWord" href="/nlab/show/category">category</a> with simulations as <a class="existingWikiWord" href="/nlab/show/morphism">morphism</a>s.</p> <p>Note that there is at most one simulation from <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> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi></mrow><annotation encoding="application/x-tex">T</annotation></semantics></math>; in fact, strong extensionality for <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi></mrow><annotation encoding="application/x-tex">T</annotation></semantics></math> is equivalent to saying that any two simulations <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi><mo>⇉</mo><mi>T</mi></mrow><annotation encoding="application/x-tex">S \rightrightarrows T</annotation></semantics></math> are equal. Also, any simulation from <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> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi></mrow><annotation encoding="application/x-tex">T</annotation></semantics></math> must be an <a class="existingWikiWord" href="/nlab/show/injection">injection</a>; in fact, strong extensionality for <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 equivalent to saying that any simulation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi><mo>→</mo><mi>T</mi></mrow><annotation encoding="application/x-tex">S \to T</annotation></semantics></math> is injective.</p> <p>Thus, we have a (large) <a class="existingWikiWord" href="/nlab/show/poset">poset</a> of sets equipped with extensional relations, and we can consistently interpret the simulations as <a class="existingWikiWord" href="/nlab/show/subset">subset</a> inclusion. This leads to the model of sets equipped with extensional relations as <a class="existingWikiWord" href="/nlab/show/transitive+set">transitive set</a>s.</p> <h2 id="references">References</h2> <ul> <li>Peter Aczel; <a href="https://web.archive.org/web/20161020002632/https://standish.stanford.edu/pdf/00000056.pdf">Non-Well-Founded Sets</a>, especially Chapter 4.</li> </ul> <p>For extensional relations in <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a>, see</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/H%C3%A5kon+Robbestad+Gylterud">Håkon Robbestad Gylterud</a>, <a class="existingWikiWord" href="/nlab/show/Elisabeth+Bonnevier">Elisabeth Bonnevier</a>, <em>Non-wellfounded sets in HoTT</em> (<a href="https://arxiv.org/abs/2001.06696">arXiv:2001.06696</a>)</li> </ul> </body></html> </div> <div class="revisedby"> <p> Last revised on October 24, 2022 at 20:59:56. See the <a href="/nlab/history/extensional+relation" style="color: #005c19">history</a> of this page for a list of all contributions to it. </p> </div> <div class="navigation navfoot"> <a href="/nlab/edit/extensional+relation" accesskey="E" class="navlink" id="edit" rel="nofollow">Edit</a><a href="https://nforum.ncatlab.org/discussion/15297/#Item_7">Discuss</a><span class="backintime"><a href="/nlab/revision/extensional+relation/27" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/diff/extensional+relation" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Changes from previous revision</a><a href="/nlab/history/extensional+relation" accesskey="S" class="navlink" id="history" rel="nofollow">History (27 revisions)</a> <a href="/nlab/show/extensional+relation/cite" style="color: black">Cite</a> <a href="/nlab/print/extensional+relation" accesskey="p" id="view_print" rel="nofollow">Print</a> <a href="/nlab/source/extensional+relation" id="view_source" rel="nofollow">Source</a> </div> </div>  </div>  </body> </html>