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> equality 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> equality </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/3749/#Item_65" 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="equality_and_equivalence">Equality and Equivalence</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/equivalence">equivalence</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/equality">equality</a> (<a class="existingWikiWord" href="/nlab/show/definitional+equality">definitional</a>, <a class="existingWikiWord" href="/nlab/show/propositional+equality">propositional</a>, <a class="existingWikiWord" href="/nlab/show/computational+equality">computational</a>, <a class="existingWikiWord" href="/nlab/show/judgemental+equality">judgemental</a>, <a class="existingWikiWord" href="/nlab/show/extensional+equality">extensional</a>, <a class="existingWikiWord" href="/nlab/show/intensional+equality">intensional</a>, <a class="existingWikiWord" href="/nlab/show/decidable+equality">decidable</a>)</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/identity+type">identity type</a>, <a class="existingWikiWord" href="/nlab/show/equivalence+of+types">equivalence of types</a>, <a class="existingWikiWord" href="/nlab/show/definitional+isomorphism">definitional isomorphism</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/isomorphism">isomorphism</a>, <a class="existingWikiWord" href="/nlab/show/weak+equivalence">weak equivalence</a>, <a class="existingWikiWord" href="/nlab/show/homotopy+equivalence">homotopy equivalence</a>, <a class="existingWikiWord" href="/nlab/show/weak+homotopy+equivalence">weak homotopy equivalence</a>, <a class="existingWikiWord" href="/nlab/show/equivalence+in+an+%28%E2%88%9E%2C1%29-category">equivalence in an (∞,1)-category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/natural+equivalence">natural equivalence</a>, <a class="existingWikiWord" href="/nlab/show/natural+isomorphism">natural isomorphism</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/gauge+equivalence">gauge equivalence</a></p> </li> <li> <p><strong>Examples.</strong></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/equivalence+of+categories">equivalence of categories</a>, <a class="existingWikiWord" href="/nlab/show/adjoint+equivalence">adjoint equivalence</a>, <a class="existingWikiWord" href="/nlab/show/weak+equivalence+of+internal+categories">weak equivalence of internal categories</a>, <a class="existingWikiWord" href="/nlab/show/Morita+equivalence">Morita equivalence</a>, <a class="existingWikiWord" href="/nlab/show/equivalence+of+2-categories">equivalence of 2-categories</a>, <a class="existingWikiWord" href="/nlab/show/equivalence+of+%28%E2%88%9E%2C1%29-categories">equivalence of (∞,1)-categories</a></li> </ul> </li> </ul> <p><strong><a class="existingWikiWord" href="/nlab/show/principle+of+equivalence">principle of equivalence</a></strong></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/univalence">univalence</a></li> </ul> <p><strong><a class="existingWikiWord" href="/nlab/show/equation">equation</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/fiber+product">fiber product</a>, <a class="existingWikiWord" href="/nlab/show/pullback">pullback</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/homotopy+pullback">homotopy pullback</a></p> </li> <li> <p><strong>Examples.</strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/linear+equation">linear equation</a>, <a class="existingWikiWord" href="/nlab/show/differential+equation">differential equation</a>, <a class="existingWikiWord" href="/nlab/show/ordinary+differential+equation">ordinary differential equation</a>, <a class="existingWikiWord" href="/nlab/show/critical+locus">critical locus</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Euler-Lagrange+equation">Euler-Lagrange equation</a>, <a class="existingWikiWord" href="/nlab/show/Einstein+equation">Einstein equation</a>, <a class="existingWikiWord" href="/nlab/show/wave+equation">wave equation</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Schr%C3%B6dinger+equation">Schrödinger equation</a>, <a class="existingWikiWord" href="/nlab/show/Knizhnik-Zamolodchikov+equation">Knizhnik-Zamolodchikov equation</a>, <a class="existingWikiWord" href="/nlab/show/Maurer-Cartan+equation">Maurer-Cartan equation</a>, <a class="existingWikiWord" href="/nlab/show/quantum+master+equation">quantum master equation</a>, <a class="existingWikiWord" href="/nlab/show/Euler-Arnold+equation">Euler-Arnold equation</a>, <a class="existingWikiWord" href="/nlab/show/Fuchsian+equation">Fuchsian equation</a>, <a class="existingWikiWord" href="/nlab/show/Fokker-Planck+equation">Fokker-Planck equation</a>, <a class="existingWikiWord" href="/nlab/show/Lax+equation">Lax equation</a></p> </li> </ul> </li> </ul> <div> <p> <a href="/nlab/edit/equality+and+equivalence+-+contents">Edit this sidebar</a> </p> </div></div></div> <h4 id="foundations">Foundations</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/foundations">foundations</a></strong></p> <h2 id="the_basis_of_it_all">The basis of it all</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/mathematical+logic">mathematical logic</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/deduction+system">deduction system</a>, <a class="existingWikiWord" href="/nlab/show/natural+deduction">natural deduction</a>, <a class="existingWikiWord" href="/nlab/show/sequent+calculus">sequent calculus</a>, <a class="existingWikiWord" href="/nlab/show/lambda-calculus">lambda-calculus</a>, <a class="existingWikiWord" href="/nlab/show/judgment">judgment</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a>, <a class="existingWikiWord" href="/nlab/show/simple+type+theory">simple type theory</a>, <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/collection">collection</a>, <a class="existingWikiWord" href="/nlab/show/object">object</a>, <a class="existingWikiWord" href="/nlab/show/type">type</a>, <a class="existingWikiWord" href="/nlab/show/term">term</a>, <a class="existingWikiWord" href="/nlab/show/set">set</a>, <a class="existingWikiWord" href="/nlab/show/element">element</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/equality">equality</a>, <a class="existingWikiWord" href="/nlab/show/judgmental+equality">judgmental equality</a>, <a class="existingWikiWord" href="/nlab/show/typal+equality">typal equality</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/universe">universe</a>, <a class="existingWikiWord" href="/nlab/show/size+issues">size issues</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/higher-order+logic">higher-order logic</a></p> </li> </ul> <h2 id="set_theory"> Set theory</h2> <div> <p><strong><a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a></strong></p> <ul> <li>fundamentals of set theory <ul> <li><a class="existingWikiWord" href="/nlab/show/propositional+logic">propositional logic</a></li> <li><a class="existingWikiWord" href="/nlab/show/first-order+logic">first-order logic</a></li> <li><a class="existingWikiWord" href="/nlab/show/typed+predicate+logic">typed predicate logic</a></li> <li><a class="existingWikiWord" href="/nlab/show/membership+relation">membership relation</a></li> <li><a class="existingWikiWord" href="/nlab/show/propositional+equality">propositional equality</a></li> <li><a class="existingWikiWord" href="/nlab/show/set">set</a>, <a class="existingWikiWord" href="/nlab/show/element">element</a>, <a class="existingWikiWord" href="/nlab/show/function">function</a>, <a class="existingWikiWord" href="/nlab/show/relation">relation</a></li> <li><a class="existingWikiWord" href="/nlab/show/universe">universe</a>, <a class="existingWikiWord" href="/nlab/show/small+set">small set</a>, <a class="existingWikiWord" href="/nlab/show/large+set">large set</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/material+set+theory">material set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/membership+relation">membership relation</a>, <a class="existingWikiWord" href="/nlab/show/propositional+equality">propositional equality</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+extensionality">axiom of extensionality</a></li> <li><a class="existingWikiWord" href="/nlab/show/pairing+structure">pairing structure</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+pairing">axiom of pairing</a></li> <li><a class="existingWikiWord" href="/nlab/show/union+structure">union structure</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+union">axiom of union</a></li> <li><a class="existingWikiWord" href="/nlab/show/powerset+structure">powerset structure</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+power+sets">axiom of power sets</a></li> <li><a class="existingWikiWord" href="/nlab/show/natural+numbers+structure">natural numbers structure</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+infinity">axiom of infinity</a></li> </ul> </li> <li>presentations of set theory <ul> <li><a class="existingWikiWord" href="/nlab/show/first-order+set+theory">first-order set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/unsorted+set+theory">unsorted set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/simply+sorted+set+theory">simply sorted set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/one-sorted+set+theory">one-sorted set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/two-sorted+set+theory">two-sorted set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/three-sorted+set+theory">three-sorted set theory</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/dependently+sorted+set+theory">dependently sorted set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/structurally+presented+set+theory">structurally presented set theory</a></li> </ul> </li> <li>structuralism in set theory <ul> <li><a class="existingWikiWord" href="/nlab/show/material+set+theory">material set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/ZFC">ZFC</a></li> <li><a class="existingWikiWord" href="/nlab/show/ZFA">ZFA</a></li> <li><a class="existingWikiWord" href="/nlab/show/Mostowski+set+theory">Mostowski set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/New+Foundations">New Foundations</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/structural+set+theory">structural set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/categorical+set+theory">categorical set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/ETCS">ETCS</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/fully+formal+ETCS">fully formal ETCS</a></li> <li><a class="existingWikiWord" href="/nlab/show/ETCS+with+elements">ETCS with elements</a></li> <li><a class="existingWikiWord" href="/nlab/show/Trimble+on+ETCS+I">Trimble on ETCS I</a></li> <li><a class="existingWikiWord" href="/nlab/show/Trimble+on+ETCS+II">Trimble on ETCS II</a></li> <li><a class="existingWikiWord" href="/nlab/show/Trimble+on+ETCS+III">Trimble on ETCS III</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/structural+ZFC">structural ZFC</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/allegorical+set+theory">allegorical set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/SEAR">SEAR</a></li> </ul> </li> </ul> </li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/class-set+theory">class-set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/class">class</a>, <a class="existingWikiWord" href="/nlab/show/proper+class">proper class</a></li> <li><a class="existingWikiWord" href="/nlab/show/universal+class">universal class</a>, <a class="existingWikiWord" href="/nlab/show/universe">universe</a></li> <li><a class="existingWikiWord" href="/nlab/show/category+of+classes">category of classes</a></li> <li><a class="existingWikiWord" href="/nlab/show/category+with+class+structure">category with class structure</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/constructive+set+theory">constructive set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/algebraic+set+theory">algebraic set theory</a></li> </ul> </div> <h2 id="foundational_axioms">Foundational axioms</h2> <div> <p><strong><a class="existingWikiWord" href="/nlab/show/foundational+axiom">foundational</a> <a class="existingWikiWord" href="/nlab/show/axioms">axioms</a></strong></p> <ul> <li> <p>basic constructions:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+cartesian+products">axiom of cartesian products</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+disjoint+unions">axiom of disjoint unions</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+the+empty+set">axiom of the empty set</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+fullness">axiom of fullness</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+function+sets">axiom of function sets</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+power+sets">axiom of power sets</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+quotient+sets">axiom of quotient sets</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/material+set+theory">material axioms</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+extensionality">axiom of extensionality</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+foundation">axiom of foundation</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+anti-foundation">axiom of anti-foundation</a></li> <li><a class="existingWikiWord" href="/nlab/show/Mostowski%27s+axiom">Mostowski's axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+pairing">axiom of pairing</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+transitive+closure">axiom of transitive closure</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+union">axiom of union</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/structural+set+theory">structural axioms</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+materialization">axiom of materialization</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/type+theory">type theoretic axioms</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axioms+of+set+truncation">axioms of set truncation</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/uniqueness+of+identity+proofs">uniqueness of identity proofs</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+K">axiom K</a></li> <li><a class="existingWikiWord" href="/nlab/show/boundary+separation">boundary separation</a></li> <li><a class="existingWikiWord" href="/nlab/show/equality+reflection">equality reflection</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+circle+type+localization">axiom of circle type localization</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theoretic axioms</a>: <ul> <li><a class="existingWikiWord" href="/nlab/show/univalence+axiom">univalence axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/Whitehead%27s+principle">Whitehead's principle</a></li> </ul> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/axioms+of+choice">axioms of choice</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+countable+choice">axiom of countable choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+dependent+choice">axiom of dependent choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+excluded+middle">axiom of excluded middle</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+existence">axiom of existence</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+multiple+choice">axiom of multiple choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/Markov%27s+axiom">Markov's axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/presentation+axiom">presentation axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/small+cardinality+selection+axiom">small cardinality selection axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+small+violations+of+choice">axiom of small violations of choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+weakly+initial+sets+of+covers">axiom of weakly initial sets of covers</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/large+cardinal+axioms">large cardinal axioms</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+infinity">axiom of infinity</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+universes">axiom of universes</a></li> <li><a class="existingWikiWord" href="/nlab/show/regular+extension+axiom">regular extension axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/inaccessible+cardinal">inaccessible cardinal</a></li> <li><a class="existingWikiWord" href="/nlab/show/measurable+cardinal">measurable cardinal</a></li> <li><a class="existingWikiWord" href="/nlab/show/elementary+embedding">elementary embedding</a></li> <li><a class="existingWikiWord" href="/nlab/show/supercompact+cardinal">supercompact cardinal</a></li> <li><a class="existingWikiWord" href="/nlab/show/Vop%C4%9Bnka%27s+principle">Vopěnka's principle</a></li> </ul> </li> <li> <p>strong axioms</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+separation">axiom of separation</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+replacement">axiom of replacement</a></li> </ul> </li> <li> <p>further</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/reflection+principle">reflection principle</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/axiom+of+tight+apartness">axiom of tight apartness</a></p> </li> </ul> </div> <h2 id="removing_axioms">Removing axioms</h2> <ul> <li><a class="existingWikiWord" href="/nlab/show/constructive+mathematics">constructive mathematics</a></li> <li><a class="existingWikiWord" href="/nlab/show/predicative+mathematics">predicative mathematics</a></li> </ul> <div> <p> <a href="/nlab/edit/foundations+-+contents">Edit this sidebar</a> </p> </div></div></div> </div> </div> <h1 id="contents">Contents</h1> <div class='maruku_toc'> <ul> <li><a href='#idea'>Idea</a></li> <li><a href='#DifferentKinds'>Different kinds of equality</a></li> <li><a href='#notions_of_equality_in_type_theory'>Notions of equality in type theory</a></li> <ul> <li><a href='#judgmental_equality'>Judgmental equality</a></li> <li><a href='#propositional_equality'>Propositional equality</a></li> <li><a href='#typal_equality'>Typal equality</a></li> <li><a href='#comparison_of_equalities'>Comparison of equalities</a></li> </ul> <li><a href='#structural_rules_of_equalities'>Structural rules of equalities</a></li> <ul> <li><a href='#reflexivity'>Reflexivity</a></li> <li><a href='#symmetry'>Symmetry</a></li> <li><a href='#transitivity'>Transitivity</a></li> <li><a href='#principle_of_substituting_equals_for_equals'>Principle of substituting equals for equals</a></li> <li><a href='#variable_conversion'>Variable conversion</a></li> </ul> <li><a href='#usages_of_equality'>Usages of equality</a></li> <ul> <li><a href='#in_definitions_of_types_and_terms'>In definitions of types and terms</a></li> <li><a href='#in_conversion_rules_and_inductive_definitions'>In conversion rules and inductive definitions</a></li> </ul> <li><a href='#metaequalities'>Meta-equalities</a></li> <li><a href='#equality_in_constructive_and_classical_mathematics'>Equality in constructive and classical mathematics</a></li> <li><a href='#internal_equality_in_set_theory'>Internal equality in set theory</a></li> <li><a href='#related_concepts'>Related concepts</a></li> <li><a href='#references'>References</a></li> </ul> </div> <h2 id="idea">Idea</h2> <p>There is a lot of interesting stuff to be said about <em>equality</em> in <a class="existingWikiWord" href="/nlab/show/logic">logic</a>, <a class="existingWikiWord" href="/nlab/show/higher+category+theory">higher category theory</a>, and the <a class="existingWikiWord" href="/nlab/show/foundations">foundations</a> of mathematics, but it hasn't all been said here yet.</p> <h2 id="DifferentKinds">Different kinds of equality</h2> <p>Here is a list of distinctions between different notions of <em>equality</em>, in different contexts, where possibly all the following pairs of notions are, in turn, “the same”, just expressed in terms of different terminologies:</p> <ul> <li>the difference between <a class="existingWikiWord" href="/nlab/show/axiom">axiomatic</a> and <a class="existingWikiWord" href="/nlab/show/definition">defined</a> equality;</li> <li>the difference between identity and equality,</li> <li>the difference between intensional and extensional equality,</li> <li>the difference between equality <a class="existingWikiWord" href="/nlab/show/judgements">judgements</a>, equality <a class="existingWikiWord" href="/nlab/show/propositions">propositions</a>, and equality <a class="existingWikiWord" href="/nlab/show/types">types</a></li> <li>the difference between equality and <a class="existingWikiWord" href="/nlab/show/isomorphism">isomorphism</a>,</li> <li>the difference between equality and <a class="existingWikiWord" href="/nlab/show/equivalence">equivalence</a>,</li> <li>the possibility of operations that might not preserve equality.</li> </ul> <h2 id="notions_of_equality_in_type_theory">Notions of equality in type theory</h2> <p>In a formal language such as <a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a>, one distinguishes various different notions of <em>equality</em> or <em>equivalence</em> of the terms of the language.</p> <p>In <a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a>, there are broadly three different notions of equality which could be distinguished: <strong>judgmental equality</strong>, <strong>propositional equality</strong>, and <strong>typal equality</strong>. Judgmental equality is defined as a basic judgment in type theory. Propositional equality is defined as a proposition in any two-layered type theory with a layer of types and a layer of propositions. Typal equality is defined as a type in type theory.</p> <h3 id="judgmental_equality">Judgmental equality</h3> <p>The first notion of equality is <strong><a class="existingWikiWord" href="/nlab/show/judgmental+equality">judgmental equality</a></strong>, where we simply judge two elements to be equal to each other. Judgmental equality is expressed in type theory by a separate <a class="existingWikiWord" href="/nlab/show/judgment">judgment</a>: in addition to typing judgments <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>⊢</mo><mo stretchy="false">(</mo><mi>t</mi><mo>:</mo><mi>A</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\Gamma \vdash (t:A)</annotation></semantics></math>, we have equality judgments <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>⊢</mo><mo stretchy="false">(</mo><mi>t</mi><mo>=</mo><mi>t</mi><mo>′</mo><mo stretchy="false">)</mo><mo>:</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">\Gamma \vdash (t = t'): A</annotation></semantics></math>. The rules for manipulating such judgments then include reflexivity, symmetry, transitivity, making judgmental equality into a judgmental <a class="existingWikiWord" href="/nlab/show/equivalence+relation">equivalence relation</a>.</p> <p>However, not all type theories have judgmental equality; most <a class="existingWikiWord" href="/nlab/show/first-order+theories">first-order theories</a> use propositional equality in place of judgmental equality, and <a class="existingWikiWord" href="/nlab/show/objective+type+theories">objective type theories</a> use typal equality in place of judgmental equality.</p> <h3 id="propositional_equality">Propositional equality</h3> <p>In any two-layer type theory with a layer of <a class="existingWikiWord" href="/nlab/show/types">types</a> and a layer of <a class="existingWikiWord" href="/nlab/show/propositions">propositions</a>, or equivalently a <a class="existingWikiWord" href="/nlab/show/first+order+logic">first order logic</a> over <a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a> or a <a class="existingWikiWord" href="/nlab/show/first-order+theory">first-order theory</a>, every 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 a binary <a class="existingWikiWord" href="/nlab/show/relation">relation</a> according to which two 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>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> are related if and only if they are equal; in this case we write <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><msub><mo>=</mo> <mi>A</mi></msub><mi>y</mi></mrow><annotation encoding="application/x-tex">x =_A y</annotation></semantics></math>. Since relations are propositions in the context of a term variable judgment in the type layer, this is called <strong><a class="existingWikiWord" href="/nlab/show/propositional+equality">propositional equality</a></strong>. The formation and introduction rules for propositional equality is as follows</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mrow><mrow><mi>Γ</mi><mo>,</mo><mi>x</mi><mo>:</mo><mi>A</mi><mo>,</mo><mi>y</mi><mo>:</mo><mi>A</mi><mo>⊢</mo><mi>x</mi><msub><mo>=</mo> <mi>A</mi></msub><mi>y</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">prop</mi></mrow></mfrac><mspace width="1em"></mspace><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mrow><mrow><mi>Γ</mi><mo>,</mo><mi>x</mi><mo>:</mo><mi>A</mi><mo>⊢</mo><mi>x</mi><msub><mo>=</mo> <mi>A</mi></msub><mi>x</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">true</mi></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, x:A, y:A \vdash x =_A y \; \mathrm{prop}} \quad \frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, x:A \vdash x =_A x \; \mathrm{true}}</annotation></semantics></math></div> <p>Then we have the elimination rules for propositional equality:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>,</mo><mi>x</mi><mo>:</mo><mi>A</mi><mo>,</mo><mi>y</mi><mo>:</mo><mi>A</mi><mo>,</mo><mi>x</mi><msub><mo>=</mo> <mi>A</mi></msub><mi>y</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">true</mi><mo>⊢</mo><mi>P</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mspace width="thickmathspace"></mspace><mi mathvariant="normal">prop</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>,</mo><mi>x</mi><mo>:</mo><mi>A</mi><mo>⊢</mo><mi>P</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>x</mi><mo stretchy="false">)</mo><mspace width="thickmathspace"></mspace><mi mathvariant="normal">true</mi></mrow><mrow><mi>Γ</mi><mo>,</mo><mi>x</mi><mo>:</mo><mi>A</mi><mo>,</mo><mi>y</mi><mo>:</mo><mi>A</mi><mo>,</mo><mi>x</mi><msub><mo>=</mo> <mi>A</mi></msub><mi>y</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">true</mi><mo>⊢</mo><mi>P</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mspace width="thickmathspace"></mspace><mi mathvariant="normal">true</mi></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A, y:A, x =_A y \; \mathrm{true} \vdash P(x, y) \; \mathrm{prop} \quad \Gamma, x:A \vdash P(x, x) \; \mathrm{true}}{\Gamma, x:A, y:A, x =_A y \; \mathrm{true} \vdash P(x, y) \; \mathrm{true}}</annotation></semantics></math></div> <p>Propositional equality satisfies the <a class="existingWikiWord" href="/nlab/show/principle+of+substitution">principle of substitution</a> and the <a class="existingWikiWord" href="/nlab/show/identity+of+indiscernibles">identity of indiscernibles</a>:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>,</mo><mi>x</mi><mo>:</mo><mi>A</mi><mo>⊢</mo><mi>P</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mspace width="thickmathspace"></mspace><mi mathvariant="normal">prop</mi></mrow><mrow><mi>Γ</mi><mo>,</mo><mi>x</mi><mo>:</mo><mi>A</mi><mo>,</mo><mi>y</mi><mo>:</mo><mi>A</mi><mo>⊢</mo><mo stretchy="false">(</mo><mi>x</mi><msub><mo>=</mo> <mi>A</mi></msub><mi>y</mi><mo stretchy="false">)</mo><mo>⇒</mo><mo stretchy="false">(</mo><mi>P</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>⇔</mo><mi>P</mi><mo stretchy="false">(</mo><mi>y</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mspace width="thickmathspace"></mspace><mi mathvariant="normal">true</mi></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash P(x) \; \mathrm{prop}}{\Gamma, x:A, y:A \vdash (x =_A y) \implies (P(x) \iff P(y)) \; \mathrm{true}}</annotation></semantics></math></div> <p>In addition, one could have propositional equality between the types themselves, with formation and introduction rules</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>B</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mrow><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mo>=</mo><mi>B</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">prop</mi></mrow></mfrac><mspace width="2em"></mspace><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mrow><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mo>=</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">true</mi></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash A = B \; \mathrm{prop}} \qquad \frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash A = A \; \mathrm{true}}</annotation></semantics></math></div> <p>Notable examples of propositional equality include the equality in all flavors of <a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a>, such as <a class="existingWikiWord" href="/nlab/show/ZFC">ZFC</a> or <a class="existingWikiWord" href="/nlab/show/ETCS">ETCS</a>.</p> <p>The presence of propositional equality is part of the axiomatization of first-order theories, although this is usually swept under the rug by including propositional equality by default in all first-order theories. (It has to be made more explicit in a structural set theory such as <a class="existingWikiWord" href="/nlab/show/SEAR">SEAR</a>, where there is no propositional equality on sets themselves, only on elements of a particular set.) By contrast, in a first order theory without propositional equality, propositional equality is an <a class="existingWikiWord" href="/nlab/show/equivalence+relation">equivalence relation</a> which has to be put onto a <a class="existingWikiWord" href="/nlab/show/type">type</a> or <a class="existingWikiWord" href="/nlab/show/preset">preset</a>.</p> <h3 id="typal_equality">Typal equality</h3> <p>However, not all type theories are <a class="existingWikiWord" href="/nlab/show/first+order+logic">first order logic</a> over <a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a>, nor are they even two-layered type theories. In type theories with only one layer for types, equality is not a relation. Instead, we have what are called <strong><a class="existingWikiWord" href="/nlab/show/typal+equality">typal equality</a></strong>, as equality of both terms and types are represented by types. Typal equality of terms is also called the <strong>equality type</strong>, <strong>identity type</strong>, <strong>path type</strong>, or <strong>identification type</strong>, and the terms of typal equality are called <strong>equalities</strong>, <strong>identities</strong>, <strong>identifications</strong>, <strong>paths</strong>. Notable examples of typal equality of terms include the <a class="existingWikiWord" href="/nlab/show/identity+type">identity type</a> in <a class="existingWikiWord" href="/nlab/show/Martin-L%C3%B6f+type+theory">Martin-Löf type theory</a> and <a class="existingWikiWord" href="/nlab/show/higher+observational+type+theory">higher observational type theory</a>, and the <a class="existingWikiWord" href="/nlab/show/cubical+path+type">cubical path type</a> in <a class="existingWikiWord" href="/nlab/show/cubical+type+theory">cubical type theory</a>.</p> <p>Type theories with only typal equality are called <a class="existingWikiWord" href="/nlab/show/objective+type+theories">objective type theories</a>. In type theories with both typal equality and either judgmental equality or propositional equality, one could distinguish between <a class="existingWikiWord" href="/nlab/show/intensional+type+theories">intensional type theories</a> and <a class="existingWikiWord" href="/nlab/show/extensional+type+theories">extensional type theories</a>: extensional type theories are type theories with an equality reflection rule, where one could derive judgmental or propositional equality of terms from typal equality of terms:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>p</mi><mo>:</mo><mi>a</mi><msub><mo>=</mo> <mi>A</mi></msub><mi>b</mi></mrow><mrow><mi>Γ</mi><mo>⊢</mo><mi>a</mi><mo>≡</mo><mi>b</mi><mo>:</mo><mi>A</mi></mrow></mfrac><mspace width="2em"></mspace><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>p</mi><mo>:</mo><mi>a</mi><msub><mo>=</mo> <mi>A</mi></msub><mi>b</mi></mrow><mrow><mi>Γ</mi><mo>⊢</mo><mi>a</mi><msub><mo>≡</mo> <mi>A</mi></msub><mi>b</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">true</mi></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma \vdash p:a =_A b}{\Gamma \vdash a \equiv b:A} \qquad \frac{\Gamma \vdash p:a =_A b}{\Gamma \vdash a \equiv_A b \; \mathrm{true}}</annotation></semantics></math></div> <p>Intensional type theories are then type theories with typal equality and one of either judgmental or propositional equality without an equality reflection rule. Note that this notion of extensionality is different from the <a class="existingWikiWord" href="/nlab/show/axiom+of+extensionality">axiom of extensionality</a> or <a class="existingWikiWord" href="/nlab/show/function+extensionality">function extensionality</a>.</p> <h3 id="comparison_of_equalities">Comparison of equalities</h3> <p>This table gives the six different notions of equality found in type theory.</p> <table><thead><tr><th>Judgment</th><th>of types</th><th>of terms</th></tr></thead><tbody><tr><td style="text-align: left;">Judgmental equality</td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mo>=</mo><mi>B</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mrow><annotation encoding="application/x-tex">\Gamma \vdash A = B \; \mathrm{type}</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>⊢</mo><mi>a</mi><mo>=</mo><mi>b</mi><mo>:</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">\Gamma \vdash a = b:A</annotation></semantics></math></td></tr> <tr><td style="text-align: left;">Propositional equality</td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mo>=</mo><mi>B</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">true</mi></mrow><annotation encoding="application/x-tex">\Gamma \vdash A = B \; \mathrm{true}</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>⊢</mo><mi>a</mi><msub><mo>=</mo> <mi>A</mi></msub><mi>b</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">true</mi></mrow><annotation encoding="application/x-tex">\Gamma \vdash a =_A b \; \mathrm{true}</annotation></semantics></math></td></tr> <tr><td style="text-align: left;">Typal equality</td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>⊢</mo><mi>P</mi><mo>:</mo><mi>A</mi><mo>≃</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">\Gamma \vdash P:A \simeq B</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>⊢</mo><mi>p</mi><mo>:</mo><mi>a</mi><msub><mo>=</mo> <mi>A</mi></msub><mi>b</mi></mrow><annotation encoding="application/x-tex">\Gamma \vdash p:a =_A b</annotation></semantics></math></td></tr> </tbody></table> <h2 id="structural_rules_of_equalities">Structural rules of equalities</h2> <h3 id="reflexivity">Reflexivity</h3> <p>The reflexivity of equality is given by the following judgmental, propositional, and typal rules respectively:</p> <ul> <li>Reflexivity of judgmental equality</li> </ul> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mrow><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mo>=</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash A = A \; \mathrm{type}}</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>a</mi><mo>:</mo><mi>A</mi></mrow><mrow><mi>Γ</mi><mo>⊢</mo><mi>a</mi><mo>=</mo><mi>a</mi><mo>:</mo><mi>A</mi></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a:A}{\Gamma \vdash a = a:A}</annotation></semantics></math></div> <ul> <li> <p>Reflexivity of propositional equality</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mrow><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mo>=</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">true</mi></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash A = A \; \mathrm{true}}</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>a</mi><mo>:</mo><mi>A</mi></mrow><mrow><mi>Γ</mi><mo>⊢</mo><mi>a</mi><msub><mo>=</mo> <mi>A</mi></msub><mi>a</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">true</mi></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a:A}{\Gamma \vdash a =_A a \; \mathrm{true}}</annotation></semantics></math></div></li> <li> <p>Reflexitivity of typal equality (i.e. <a class="existingWikiWord" href="/nlab/show/identity+function">identity function</a> and identity <a class="existingWikiWord" href="/nlab/show/path">path</a>)</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mrow><mrow><mi>Γ</mi><mo>⊢</mo><msub><mi>id</mi> <mi>A</mi></msub><mo>:</mo><mi>A</mi><mo>≃</mo><mi>A</mi></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash id_{A}:A \simeq A}</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>a</mi><mo>:</mo><mi>A</mi></mrow><mrow><mi>Γ</mi><mo>⊢</mo><msub><mi mathvariant="normal">refl</mi> <mi>A</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo><mo>:</mo><mi>a</mi><msub><mo>=</mo> <mi>A</mi></msub><mi>a</mi></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a:A}{\Gamma \vdash \mathrm{refl}_{A}(a):a =_A a}</annotation></semantics></math></div></li> </ul> <h3 id="symmetry">Symmetry</h3> <p>The symmetry of equality is given by the following judgmental, propositional, and typal rules respectively:</p> <ul> <li> <p>Symmetry of judgmental equality</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mo>=</mo><mi>B</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mrow><mrow><mi>Γ</mi><mo>⊢</mo><mi>B</mi><mo>=</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma \vdash A = B \; \mathrm{type}}{\Gamma \vdash B = A \; \mathrm{type}}</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>a</mi><mo>=</mo><mi>b</mi><mo>:</mo><mi>A</mi></mrow><mrow><mi>Γ</mi><mo>⊢</mo><mi>b</mi><mo>=</mo><mi>a</mi><mo>:</mo><mi>A</mi></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a = b:A}{\Gamma \vdash b = a:A}</annotation></semantics></math></div></li> <li> <p>Symmetry of propositional equality</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>B</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mo>=</mo><mi>B</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">true</mi></mrow><mrow><mi>Γ</mi><mo>⊢</mo><mi>B</mi><mo>=</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">true</mi></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash A = B \; \mathrm{true}}{\Gamma \vdash B = A \; \mathrm{true}}</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>a</mi><mo>:</mo><mi>A</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>b</mi><mo>:</mo><mi>A</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>a</mi><msub><mo>=</mo> <mi>A</mi></msub><mi>b</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">true</mi></mrow><mrow><mi>Γ</mi><mo>⊢</mo><mi>b</mi><msub><mo>=</mo> <mi>A</mi></msub><mi>a</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">true</mi></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash a =_A b \; \mathrm{true}}{\Gamma \vdash b =_A a \; \mathrm{true}}</annotation></semantics></math></div></li> <li> <p>Symmetry of typal equality (i.e. <a class="existingWikiWord" href="/nlab/show/inverse+function">inverse function</a> and inverse path)</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>B</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>P</mi><mo>:</mo><mi>A</mi><mo>≃</mo><mi>B</mi></mrow><mrow><mi>Γ</mi><mo>⊢</mo><msup><mi>P</mi> <mrow><mo lspace="verythinmathspace" rspace="0em">−</mo><mn>1</mn></mrow></msup><mo>:</mo><mi>B</mi><mo>≃</mo><mi>A</mi></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash P:A \simeq B}{\Gamma \vdash P^{-1}:B \simeq A}</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>a</mi><mo>:</mo><mi>A</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>b</mi><mo>:</mo><mi>A</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>p</mi><mo>:</mo><mi>a</mi><msub><mo>=</mo> <mi>A</mi></msub><mi>b</mi></mrow><mrow><mi>Γ</mi><mo>⊢</mo><msup><mi>p</mi> <mrow><mo lspace="verythinmathspace" rspace="0em">−</mo><mn>1</mn></mrow></msup><mo>:</mo><mi>b</mi><msub><mo>=</mo> <mi>A</mi></msub><mi>a</mi></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:a =_A b}{\Gamma \vdash p^{-1}:b =_A a}</annotation></semantics></math></div></li> </ul> <h3 id="transitivity">Transitivity</h3> <p>The transitivity of equality is given by the following judgmental, propositional, and typal rules respectively:</p> <ul> <li> <p>Transitivity of judgmental equality</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mo>=</mo><mi>B</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>B</mi><mo>=</mo><mi>C</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mrow><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mo>=</mo><mi>C</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma \vdash A = B \; \mathrm{type} \quad \Gamma \vdash B = C \; \mathrm{type} }{\Gamma \vdash A = C \; \mathrm{type}}</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>a</mi><mo>=</mo><mi>b</mi><mo>:</mo><mi>A</mi><mspace width="1em"></mspace><mi>b</mi><mo>=</mo><mi>c</mi><mo>:</mo><mi>A</mi></mrow><mrow><mi>Γ</mi><mo>⊢</mo><mi>a</mi><mo>=</mo><mi>c</mi><mo>:</mo><mi>A</mi></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a = b:A \quad b = c:A }{\Gamma \vdash a = c:A}</annotation></semantics></math></div></li> <li> <p>Transitivity of propositional equality</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>B</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>C</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mo>=</mo><mi>B</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">true</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>B</mi><mo>=</mo><mi>C</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">true</mi></mrow><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mo>=</mo><mi>C</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">true</mi></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash A = B \; \mathrm{true} \quad \Gamma \vdash B = C \; \mathrm{true}}{\Gamma \vdash A = C \; \mathrm{true}}</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>a</mi><mo>:</mo><mi>A</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>b</mi><mo>:</mo><mi>A</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>c</mi><mo>:</mo><mi>A</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>a</mi><msub><mo>=</mo> <mi>A</mi></msub><mi>b</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">true</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>b</mi><msub><mo>=</mo> <mi>A</mi></msub><mi>c</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">true</mi></mrow><mrow><mi>Γ</mi><mo>⊢</mo><mi>a</mi><msub><mo>=</mo> <mi>A</mi></msub><mi>c</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">true</mi></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash c:A \quad \Gamma \vdash a =_A b \; \mathrm{true} \quad \Gamma \vdash b =_A c \; \mathrm{true}}{\Gamma \vdash a =_A c \; \mathrm{true}}</annotation></semantics></math></div></li> <li> <p>Transitivity of typal equality (i.e. <a class="existingWikiWord" href="/nlab/show/composition">composition</a> of functions and path concatenation)</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>B</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>C</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>P</mi><mo>:</mo><mi>A</mi><mo>≃</mo><mi>B</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>Q</mi><mo>:</mo><mi>B</mi><mo>≃</mo><mi>C</mi></mrow><mrow><mi>Γ</mi><mo>⊢</mo><mi>Q</mi><mo>∘</mo><mi>P</mi><mo>:</mo><mi>A</mi><mo>≃</mo><mi>C</mi></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash P:A \simeq B \quad \Gamma \vdash Q:B \simeq C}{\Gamma \vdash Q \circ P:A \simeq C}</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>a</mi><mo>:</mo><mi>A</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>b</mi><mo>:</mo><mi>A</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>c</mi><mo>:</mo><mi>A</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>p</mi><mo>:</mo><mi>a</mi><msub><mo>=</mo> <mi>A</mi></msub><mi>b</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>q</mi><mo>:</mo><mi>b</mi><msub><mo>=</mo> <mi>A</mi></msub><mi>c</mi></mrow><mrow><mi>Γ</mi><mo>⊢</mo><mi>p</mi><mo>•</mo><mi>q</mi><mo>:</mo><mi>a</mi><msub><mo>=</mo> <mi>A</mi></msub><mi>c</mi></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash c:A \quad \Gamma \vdash p:a =_A b \quad \Gamma \vdash q:b =_A c}{\Gamma \vdash p \bullet q:a =_A c}</annotation></semantics></math></div></li> </ul> <h3 id="principle_of_substituting_equals_for_equals">Principle of substituting equals for equals</h3> <p>The <a class="existingWikiWord" href="/nlab/show/principle+of+substituting+equals+for+equals">principle of substituting equals for equals</a> is given by the following judgmental, propositional, and typal rules respectively:</p> <ul> <li> <p>Substitution of judgmentally equal terms:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>a</mi><mo>=</mo><mi>b</mi><mo>:</mo><mi>A</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>,</mo><mi>x</mi><mo>:</mo><mi>A</mi><mo>,</mo><mi>Δ</mi><mo>⊢</mo><mi>B</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mrow><mrow><mi>Γ</mi><mo>,</mo><mi>Δ</mi><mo stretchy="false">[</mo><mi>b</mi><mo stretchy="false">/</mo><mi>x</mi><mo stretchy="false">]</mo><mo>⊢</mo><mi>B</mi><mo stretchy="false">[</mo><mi>a</mi><mo stretchy="false">/</mo><mi>x</mi><mo stretchy="false">]</mo><mo>=</mo><mi>B</mi><mo stretchy="false">[</mo><mi>b</mi><mo stretchy="false">/</mo><mi>x</mi><mo stretchy="false">]</mo><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a = b : A \quad \Gamma, x:A, \Delta \vdash B \; \mathrm{type}}{\Gamma, \Delta[b/x] \vdash B[a/x] = B[b/x] \; \mathrm{type}}</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>a</mi><mo>=</mo><mi>b</mi><mo>:</mo><mi>A</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>,</mo><mi>x</mi><mo>:</mo><mi>A</mi><mo>,</mo><mi>Δ</mi><mo>⊢</mo><mi>c</mi><mo>:</mo><mi>B</mi></mrow><mrow><mi>Γ</mi><mo>,</mo><mi>Δ</mi><mo stretchy="false">[</mo><mi>b</mi><mo stretchy="false">/</mo><mi>x</mi><mo stretchy="false">]</mo><mo>⊢</mo><mi>c</mi><mo stretchy="false">[</mo><mi>a</mi><mo stretchy="false">/</mo><mi>x</mi><mo stretchy="false">]</mo><mo>=</mo><mi>c</mi><mo stretchy="false">[</mo><mi>b</mi><mo stretchy="false">/</mo><mi>x</mi><mo stretchy="false">]</mo><mo>:</mo><mi>B</mi><mo stretchy="false">[</mo><mi>b</mi><mo stretchy="false">/</mo><mi>x</mi><mo stretchy="false">]</mo></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a = b : A \quad \Gamma, x:A, \Delta \vdash c:B}{\Gamma, \Delta[b/x] \vdash c[a/x] = c[b/x]: B[b/x]}</annotation></semantics></math></div></li> <li> <p>Substitution of propositionally equal terms:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>a</mi><mo>:</mo><mi>A</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>b</mi><mo>:</mo><mi>A</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>a</mi><msub><mo>=</mo> <mi>A</mi></msub><mi>b</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">true</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>,</mo><mi>x</mi><mo>:</mo><mi>A</mi><mo>,</mo><mi>Δ</mi><mo>⊢</mo><mi>B</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mrow><mrow><mi>Γ</mi><mo>,</mo><mi>Δ</mi><mo stretchy="false">[</mo><mi>b</mi><mo stretchy="false">/</mo><mi>x</mi><mo stretchy="false">]</mo><mo>⊢</mo><mi>B</mi><mo stretchy="false">[</mo><mi>a</mi><mo stretchy="false">/</mo><mi>x</mi><mo stretchy="false">]</mo><mo>=</mo><mi>B</mi><mo stretchy="false">[</mo><mi>b</mi><mo stretchy="false">/</mo><mi>x</mi><mo stretchy="false">]</mo><mspace width="thickmathspace"></mspace><mi mathvariant="normal">true</mi></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a : A \quad \Gamma \vdash b : A \quad \Gamma \vdash a =_A b \; \mathrm{true} \quad \Gamma, x:A, \Delta \vdash B \; \mathrm{type}}{\Gamma, \Delta[b/x] \vdash B[a/x] = B[b/x] \; \mathrm{true}}</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>a</mi><mo>:</mo><mi>A</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>b</mi><mo>:</mo><mi>A</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>a</mi><msub><mo>=</mo> <mi>A</mi></msub><mi>b</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">true</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>,</mo><mi>x</mi><mo>:</mo><mi>A</mi><mo>,</mo><mi>Δ</mi><mo>⊢</mo><mi>c</mi><mo>:</mo><mi>B</mi></mrow><mrow><mi>Γ</mi><mo>,</mo><mi>Δ</mi><mo stretchy="false">[</mo><mi>b</mi><mo stretchy="false">/</mo><mi>x</mi><mo stretchy="false">]</mo><mo>⊢</mo><mi>c</mi><mo stretchy="false">[</mo><mi>a</mi><mo stretchy="false">/</mo><mi>x</mi><mo stretchy="false">]</mo><msub><mo>=</mo> <mrow><mi>B</mi><mo stretchy="false">[</mo><mi>b</mi><mo stretchy="false">/</mo><mi>x</mi><mo stretchy="false">]</mo></mrow></msub><mi>c</mi><mo stretchy="false">[</mo><mi>b</mi><mo stretchy="false">/</mo><mi>x</mi><mo stretchy="false">]</mo><mspace width="thickmathspace"></mspace><mi mathvariant="normal">true</mi></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a : A \quad \Gamma \vdash b : A \quad \Gamma \vdash a =_A b \; \mathrm{true} \quad \Gamma, x:A, \Delta \vdash c:B}{\Gamma, \Delta[b/x] \vdash c[a/x] =_{B[b/x]} c[b/x] \; \mathrm{true}}</annotation></semantics></math></div></li> <li> <p>Substitution of typally equal terms (i.e. <a class="existingWikiWord" href="/nlab/show/transport">transport</a> and <a class="existingWikiWord" href="/nlab/show/action+on+identifications">action on identifications</a>):</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>a</mi><mo>:</mo><mi>A</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>b</mi><mo>:</mo><mi>A</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>p</mi><mo>:</mo><mi>a</mi><msub><mo>=</mo> <mi>A</mi></msub><mi>b</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>,</mo><mi>x</mi><mo>:</mo><mi>A</mi><mo>,</mo><mi>Δ</mi><mo>⊢</mo><mi>B</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mrow><mrow><mi>Γ</mi><mo>,</mo><mi>Δ</mi><mo stretchy="false">[</mo><mi>b</mi><mo stretchy="false">/</mo><mi>x</mi><mo stretchy="false">]</mo><mo>⊢</mo><mi mathvariant="normal">tr</mi><mo stretchy="false">(</mo><mi>x</mi><mo>.</mo><mi>B</mi><mo>,</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo>,</mo><mi>p</mi><mo stretchy="false">)</mo><mo>:</mo><mi>B</mi><mo stretchy="false">[</mo><mi>a</mi><mo stretchy="false">/</mo><mi>x</mi><mo stretchy="false">]</mo><mo>≃</mo><mi>B</mi><mo stretchy="false">[</mo><mi>b</mi><mo stretchy="false">/</mo><mi>x</mi><mo stretchy="false">]</mo></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:a =_A b \quad \Gamma, x:A, \Delta \vdash B \; \mathrm{type}}{\Gamma, \Delta[b/x] \vdash \mathrm{tr}(x.B, a, b, p):B[a/x] \simeq B[b/x]}</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>a</mi><mo>:</mo><mi>A</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>b</mi><mo>:</mo><mi>A</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>p</mi><mo>:</mo><mi>a</mi><msub><mo>=</mo> <mi>A</mi></msub><mi>b</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>,</mo><mi>x</mi><mo>:</mo><mi>A</mi><mo>,</mo><mi>Δ</mi><mo>⊢</mo><mi>c</mi><mo>:</mo><mi>B</mi></mrow><mrow><mi>Γ</mi><mo>,</mo><mi>Δ</mi><mo stretchy="false">[</mo><mi>b</mi><mo stretchy="false">/</mo><mi>x</mi><mo stretchy="false">]</mo><mo>⊢</mo><mi mathvariant="normal">ap</mi><mo stretchy="false">(</mo><mi>c</mi><mo>,</mo><mi>x</mi><mo>.</mo><mi>B</mi><mo>,</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo>,</mo><mi>p</mi><mo stretchy="false">)</mo><mo>:</mo><mi mathvariant="normal">tr</mi><mo stretchy="false">(</mo><mi>x</mi><mo>.</mo><mi>B</mi><mo>,</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo>,</mo><mi>p</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi>c</mi><mo stretchy="false">[</mo><mi>a</mi><mo stretchy="false">/</mo><mi>x</mi><mo stretchy="false">]</mo><mo stretchy="false">)</mo><msub><mo>=</mo> <mrow><mi>B</mi><mo stretchy="false">[</mo><mi>b</mi><mo stretchy="false">/</mo><mi>x</mi><mo stretchy="false">]</mo></mrow></msub><mi>c</mi><mo stretchy="false">[</mo><mi>b</mi><mo stretchy="false">/</mo><mi>x</mi><mo stretchy="false">]</mo></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:a =_A b \quad \Gamma, x:A, \Delta \vdash c:B}{\Gamma, \Delta[b/x] \vdash \mathrm{ap}(c, x.B, a, b, p):\mathrm{tr}(x.B, a, b, p)(c[a/x]) =_{B[b/x]} c[b/x]}</annotation></semantics></math></div></li> </ul> <h3 id="variable_conversion">Variable conversion</h3> <p>The variable conversion rule is given by the following judgmental, propositional, and typal rules respectively:</p> <ul> <li> <p>Judgmental variable conversion rule:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mo>=</mo><mi>B</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>,</mo><mi>x</mi><mo>:</mo><mi>A</mi><mo>,</mo><mi>Δ</mi><mo>⊢</mo><mi>𝒥</mi></mrow><mrow><mi>Γ</mi><mo>,</mo><mi>x</mi><mo>:</mo><mi>B</mi><mo>,</mo><mi>Δ</mi><mo>⊢</mo><mi>𝒥</mi></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma \vdash A = B \; \mathrm{type} \quad \Gamma, x:A, \Delta \vdash \mathcal{J}}{\Gamma, x:B, \Delta \vdash \mathcal{J}}</annotation></semantics></math></div></li> <li> <p>Propositional variable conversion rule:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>B</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mo>=</mo><mi>B</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">true</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>,</mo><mi>x</mi><mo>:</mo><mi>A</mi><mo>,</mo><mi>Δ</mi><mo>⊢</mo><mi>𝒥</mi></mrow><mrow><mi>Γ</mi><mo>,</mo><mi>x</mi><mo>:</mo><mi>B</mi><mo>,</mo><mi>Δ</mi><mo>⊢</mo><mi>𝒥</mi></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash A = B \; \mathrm{true} \quad \Gamma, x:A, \Delta \vdash \mathcal{J}}{\Gamma, x:B, \Delta \vdash \mathcal{J}}</annotation></semantics></math></div></li> <li> <p>Typal variable conversion rule:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>B</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>P</mi><mo>:</mo><mi>A</mi><mo>≃</mo><mi>B</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>,</mo><mi>x</mi><mo>:</mo><mi>A</mi><mo>,</mo><mi>Δ</mi><mo>⊢</mo><mi>𝒥</mi></mrow><mrow><mi>Γ</mi><mo>,</mo><mi>y</mi><mo>:</mo><mi>B</mi><mo>,</mo><mi>Δ</mi><mo stretchy="false">[</mo><msup><mi>P</mi> <mrow><mo lspace="verythinmathspace" rspace="0em">−</mo><mn>1</mn></mrow></msup><mo stretchy="false">(</mo><mi>y</mi><mo stretchy="false">)</mo><mo stretchy="false">/</mo><mi>x</mi><mo stretchy="false">]</mo><mo>⊢</mo><mi>𝒥</mi><mo stretchy="false">[</mo><msup><mi>P</mi> <mrow><mo lspace="verythinmathspace" rspace="0em">−</mo><mn>1</mn></mrow></msup><mo stretchy="false">(</mo><mi>y</mi><mo stretchy="false">)</mo><mo stretchy="false">/</mo><mi>x</mi><mo stretchy="false">]</mo></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash P:A \simeq B \quad \Gamma, x:A, \Delta \vdash \mathcal{J}}{\Gamma, y:B, \Delta[P^{-1}(y)/x] \vdash \mathcal{J}[P^{-1}(y)/x]}</annotation></semantics></math></div></li> </ul> <p><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>𝒥</mi></mrow><annotation encoding="application/x-tex">\mathcal{J}</annotation></semantics></math> is a generic judgment thesis.</p> <h2 id="usages_of_equality">Usages of equality</h2> <h3 id="in_definitions_of_types_and_terms">In definitions of types and terms</h3> <p>The three different notions of equality above could be used in <a class="existingWikiWord" href="/nlab/show/definitions">definitions</a> of <a class="existingWikiWord" href="/nlab/show/types">types</a> and <a class="existingWikiWord" href="/nlab/show/terms">terms</a>, as well as in the rules for the <a class="existingWikiWord" href="/nlab/show/single+assignment+operator">single assignment operator</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">\coloneqq</annotation></semantics></math>. In <a class="existingWikiWord" href="/nlab/show/Martin-L%C3%B6f+type+theory">Martin-Löf type theory</a> and <a class="existingWikiWord" href="/nlab/show/cubical+type+theory">cubical type theory</a>, judgmental equality is used for definitional equality. In <a class="existingWikiWord" href="/nlab/show/ZFC">ZFC</a> and <a class="existingWikiWord" href="/nlab/show/ETCS">ETCS</a>, propositional equality is used for definitional equality, and in <a class="existingWikiWord" href="/nlab/show/objective+type+theories">objective type theories</a>, typal equality is used for definitional equality.</p> <h3 id="in_conversion_rules_and_inductive_definitions">In conversion rules and inductive definitions</h3> <p>The three different notions of equality above could also be used in the <a class="existingWikiWord" href="/nlab/show/conversion+rules">conversion rules</a> for the various type formers, such as <a class="existingWikiWord" href="/nlab/show/beta+conversion">beta conversion</a> or <a class="existingWikiWord" href="/nlab/show/eta+conversion">eta conversion</a>, where the equality is called <strong><a class="existingWikiWord" href="/nlab/show/conversional+equality">conversional equality</a></strong> or <strong>computational equality</strong>. Computational equality is important because it is the equality used in <a class="existingWikiWord" href="/nlab/show/inductive+definitions">inductive definitions</a>. In <a class="existingWikiWord" href="/nlab/show/Martin-L%C3%B6f+type+theory">Martin-Löf type theory</a> and <a class="existingWikiWord" href="/nlab/show/cubical+type+theory">cubical type theory</a>, judgmental equality is used for computational equality, and in <a class="existingWikiWord" href="/nlab/show/objective+type+theories">objective type theories</a>, typal equality is used for computational equality.</p> <h2 id="metaequalities">Meta-equalities</h2> <p>There are also equalities in <a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a> which are not internal to the type theory itself, but rather equalities in the metatheory. These include <strong>syntactic equality</strong> of expressions, as well as <strong><a class="existingWikiWord" href="/nlab/show/alpha-equivalence">alpha-equivalence</a></strong> and <strong><a class="existingWikiWord" href="/nlab/show/definitional+equality">definitional equality</a></strong> of syntactical expressions. When using <a class="existingWikiWord" href="/nlab/show/de+Bruijn+indices">de Bruijn indices</a>, alpha-equivalence is the same as syntactic equality, but when using <a class="existingWikiWord" href="/nlab/show/variables">variables</a>, alpha-equivalence is different from syntactic equality: rather alpha-equivalence is equality up to the renaming of <a class="existingWikiWord" href="/nlab/show/bound+variables">bound variables</a>. All type theories, like <a class="existingWikiWord" href="/nlab/show/MLTT">MLTT</a>, <a class="existingWikiWord" href="/nlab/show/cubical+type+theory">cubical type theory</a>, <a class="existingWikiWord" href="/nlab/show/ZFC">ZFC</a>, and <a class="existingWikiWord" href="/nlab/show/ETCS">ETCS</a>, have syntactic equality, alpha-equivalence, and definitional equality of syntactical expressions, including the type theories which lack <a class="existingWikiWord" href="/nlab/show/judgmental+equality">judgmental equality</a> like <a class="existingWikiWord" href="/nlab/show/objective+type+theories">objective type theories</a>.</p> <h2 id="equality_in_constructive_and_classical_mathematics">Equality in constructive and classical mathematics</h2> <p>Constructive mathematics is mathematics in which the law of excluded middle does not necessarily hold for <a class="existingWikiWord" href="/nlab/show/propositions">propositions</a>, <a class="existingWikiWord" href="/nlab/show/subsingletons">subsingletons</a>, or <a class="existingWikiWord" href="/nlab/show/h-propositions">h-propositions</a>. Classical mathematics is mathematics in which the law of excluded middle does hold for <a class="existingWikiWord" href="/nlab/show/propositions">propositions</a>, <a class="existingWikiWord" href="/nlab/show/subsingletons">subsingletons</a>, or <a class="existingWikiWord" href="/nlab/show/h-propositions">h-propositions</a>. Here, we take equality to mean either typal or propositional equality, so that equality is a relation or a type family on a type or set.</p> <p>In classical mathematics, equality of sets is a <a class="existingWikiWord" href="/nlab/show/stable+relation">stable</a> <a class="existingWikiWord" href="/nlab/show/equivalence+relation">equivalence relation</a>, and <a class="existingWikiWord" href="/nlab/show/denial+inequality">denial inequality</a> of sets is a <a class="existingWikiWord" href="/nlab/show/tight+apartness+relation">tight apartness relation</a>. However, in constructive mathematics, equality cannot be proven to be stable for all sets, and denial inequality cannot be proven to be a tight apartness relation for all sets. Instead, one could distinguish between 4 different notions of equality and <a class="existingWikiWord" href="/nlab/show/inequality">inequality</a>:</p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/tight+apartness+relations">tight apartness relations</a>. However, not all sets have tight apartness relations.</p> </li> <li> <p>equality, which is an <a class="existingWikiWord" href="/nlab/show/equivalence+relation">equivalence relation</a>; set with <a class="existingWikiWord" href="/nlab/show/tight+apartness+relations">tight apartness relations</a> have <a class="existingWikiWord" href="/nlab/show/stable+equality">stable equality</a>.</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/denial+inequality">denial inequality</a>, which can only be proven to be a <a class="existingWikiWord" href="/nlab/show/weakly+tight">weakly tight</a> <a class="existingWikiWord" href="/nlab/show/irreflexive+symmetric+relation">irreflexive symmetric relation</a>. However, all statements in classical mathematics involving only denial inequalities hold in constructive mathematics, by the <a class="existingWikiWord" href="/nlab/show/double+negation+translation">double negation translation</a> and the property that for any proposition <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>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>¬</mo><mo>¬</mo><mo>¬</mo><mi>P</mi></mrow><annotation encoding="application/x-tex">\neg \neg \neg P</annotation></semantics></math> if and only if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>¬</mo><mi>P</mi></mrow><annotation encoding="application/x-tex">\neg P</annotation></semantics></math>.</p> </li> <li> <p>the <a class="existingWikiWord" href="/nlab/show/double+negation">double negation</a> of equality, which can only be proven to be a <a class="existingWikiWord" href="/nlab/show/stable+relation">stable</a> <a class="existingWikiWord" href="/nlab/show/reflexive+symmetric+relation">reflexive symmetric relation</a>. However, all statements in classical mathematics involving only equality hold in constructive mathematics with the equality replaced by its double negation, by the <a class="existingWikiWord" href="/nlab/show/double+negation+translation">double negation translation</a>.</p> </li> </ul> <p>The sets in which equality and inequality behaves as it does in <a class="existingWikiWord" href="/nlab/show/classical+mathematics">classical mathematics</a> are the sets with <a class="existingWikiWord" href="/nlab/show/decidable+equality">decidable equality</a>.</p> <p>As a result, in constructive mathematics, sometimes one takes sets with <a class="existingWikiWord" href="/nlab/show/tight+apartness+relations">tight apartness relations</a> instead of general <a class="existingWikiWord" href="/nlab/show/sets">sets</a> to be the foundational primitive concept. In classical mathematics, this is unnecessary, because every <a class="existingWikiWord" href="/nlab/show/set">set</a> has a <a class="existingWikiWord" href="/nlab/show/tight+apartness+relation">tight apartness relation</a>.</p> <h2 id="internal_equality_in_set_theory">Internal equality in set theory</h2> <p>Relations and equality could be <a class="existingWikiWord" href="/nlab/show/internal+logic+of+set+theory">internalized in any set theory</a>: the internal equality in set theory is the smallest internal <a class="existingWikiWord" href="/nlab/show/reflexive+relation">reflexive relation</a> 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>, and it is in fact an internal <a class="existingWikiWord" href="/nlab/show/equivalence+relation">equivalence relation</a>; it is the only internal equivalence relation 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> that is also a <a class="existingWikiWord" href="/nlab/show/partial+order">partial order</a> (although that fact is somewhat circular). This relation is often called the <strong>identity relation</strong> 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>, either because ‘identity’ can mean ‘equality’ or because it is the <a class="existingWikiWord" href="/nlab/show/identity">identity</a> for <a class="existingWikiWord" href="/nlab/show/composition">composition</a> of relations.</p> <p>In the <a class="existingWikiWord" href="/nlab/show/category">category</a> of reflexive relations 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>, the <a class="existingWikiWord" href="/nlab/show/equality+relation">equality relation</a> 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> is an <a class="existingWikiWord" href="/nlab/show/initial+object">initial reflexive relation</a>; when the equality relation is a <a class="existingWikiWord" href="/nlab/show/type+family">type family</a> instead of a family of propositions, then the equality relation is the initial type generated by reflexivity or the <a class="existingWikiWord" href="/nlab/show/first+law+of+thought">first law of thought</a>.</p> <p>As a <a class="existingWikiWord" href="/nlab/show/subset">subset</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi><mo>×</mo><mi>S</mi></mrow><annotation encoding="application/x-tex">S \times S</annotation></semantics></math>, the equality relation is often called the <strong><a class="existingWikiWord" href="/nlab/show/diagonal">diagonal</a></strong> and written <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Δ</mi> <mi>S</mi></msub></mrow><annotation encoding="application/x-tex">\Delta_S</annotation></semantics></math> or similarly. As an abstract set, this subset is <a class="existingWikiWord" href="/nlab/show/isomorphism">isomorphic</a> to <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, so one also sees the diagonal as a map, the <a class="existingWikiWord" href="/nlab/show/diagonal+function">diagonal function</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi><mover><mo>→</mo><mrow><msub><mi>Δ</mi> <mi>S</mi></msub></mrow></mover><mi>S</mi><mo>×</mo><mi>S</mi></mrow><annotation encoding="application/x-tex">S \overset{\Delta_S}\to S \times S</annotation></semantics></math>, which maps <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><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(x,x)</annotation></semantics></math>; note that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>=</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">x = x</annotation></semantics></math>. This is in <a class="existingWikiWord" href="/nlab/show/Set">Set</a>; analogous <a class="existingWikiWord" href="/nlab/show/diagonal+morphisms">diagonal morphisms</a> exist in any <a class="existingWikiWord" href="/nlab/show/cartesian+monoidal+category">cartesian monoidal category</a>.</p> <h2 id="related_concepts">Related concepts</h2> <ul> <li> <p><strong>equality</strong>, <a class="existingWikiWord" href="/nlab/show/equation">equation</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/alpha-equivalence">alpha-equivalence</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/definition">definition</a>, <a class="existingWikiWord" href="/nlab/show/assignment">assignment</a>, <a class="existingWikiWord" href="/nlab/show/equality">equality</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/identity+type">identity type</a>,</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/identity+of+indiscernibles">identity of indiscernibles</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/inequality">inequality</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/denial+inequality">denial inequality</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/apartness+relation">apartness relation</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/isomorphism">isomorphism</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/equivalence">equivalence</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/weak+equivalence">weak equivalence</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/homotopy+equivalence">homotopy equivalence</a>, <a class="existingWikiWord" href="/nlab/show/weak+homotopy+equivalence">weak homotopy equivalence</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/equivalence+in+an+%28%E2%88%9E%2C1%29-category">equivalence in an (∞,1)-category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/equivalence+of+%28%E2%88%9E%2C1%29-categories">equivalence of (∞,1)-categories</a></p> </li> </ul> <div> <table><thead><tr><th><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mo lspace="verythinmathspace" rspace="0em">−</mo></mphantom></mrow><annotation encoding="application/x-tex">\phantom{-}</annotation></semantics></math>symbol<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mo lspace="verythinmathspace" rspace="0em">−</mo></mphantom></mrow><annotation encoding="application/x-tex">\phantom{-}</annotation></semantics></math></th><th><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mo lspace="verythinmathspace" rspace="0em">−</mo></mphantom></mrow><annotation encoding="application/x-tex">\phantom{-}</annotation></semantics></math>in <a class="existingWikiWord" href="/nlab/show/logic">logic</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mo lspace="verythinmathspace" rspace="0em">−</mo></mphantom></mrow><annotation encoding="application/x-tex">\phantom{-}</annotation></semantics></math></th></tr></thead><tbody><tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><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></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/element">element</a> <a class="existingWikiWord" href="/nlab/show/relation">relation</a></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mspace width="thinmathspace"></mspace><mo>:</mo></mrow><annotation encoding="application/x-tex">\,:</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/type">typing</a> <a class="existingWikiWord" href="/nlab/show/relation">relation</a></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>=</mo></mrow><annotation encoding="application/x-tex">=</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/equality">equality</a></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊢</mo></mrow><annotation encoding="application/x-tex">\vdash</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/entailment">entailment</a> / <a class="existingWikiWord" href="/nlab/show/sequent">sequent</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><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><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/true">true</a> / <a class="existingWikiWord" href="/nlab/show/top">top</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊥</mo></mrow><annotation encoding="application/x-tex">\bot</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/false">false</a> / <a class="existingWikiWord" href="/nlab/show/bottom">bottom</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⇒</mo></mrow><annotation encoding="application/x-tex">\Rightarrow</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/implication">implication</a></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⇔</mo></mrow><annotation encoding="application/x-tex">\Leftrightarrow</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/logical+equivalence">logical equivalence</a></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>¬</mo></mrow><annotation encoding="application/x-tex">\not</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/negation">negation</a></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≠</mo></mrow><annotation encoding="application/x-tex">\neq</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/negation">negation</a> of <a class="existingWikiWord" href="/nlab/show/equality">equality</a> / <a class="existingWikiWord" href="/nlab/show/apartness">apartness</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∉</mo></mrow><annotation encoding="application/x-tex">\notin</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/negation">negation</a> of <a class="existingWikiWord" href="/nlab/show/element">element</a> <a class="existingWikiWord" href="/nlab/show/relation">relation</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>¬</mo><mo>¬</mo></mrow><annotation encoding="application/x-tex">\not \not</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/double+negation">negation of negation</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∃</mo></mrow><annotation encoding="application/x-tex">\exists</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/existential+quantification">existential quantification</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∀</mo></mrow><annotation encoding="application/x-tex">\forall</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/universal+quantification">universal quantification</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∧</mo></mrow><annotation encoding="application/x-tex">\wedge</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/logical+conjunction">logical conjunction</a></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∨</mo></mrow><annotation encoding="application/x-tex">\vee</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/logical+disjunction">logical disjunction</a></td></tr> <tr><td style="text-align: left;"></td><td style="text-align: left;"></td></tr> <tr><td style="text-align: left;"><strong>symbol</strong></td><td style="text-align: left;"><strong>in <a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a> (<a class="existingWikiWord" href="/nlab/show/propositions+as+types">propositions as types</a>)</strong></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><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></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/function+type">function type</a> (<a class="existingWikiWord" href="/nlab/show/implication">implication</a>)</td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>×</mo></mrow><annotation encoding="application/x-tex">\times</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/product+type">product type</a> (<a class="existingWikiWord" href="/nlab/show/conjunction">conjunction</a>)</td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo lspace="verythinmathspace" rspace="0em">+</mo></mrow><annotation encoding="application/x-tex">+</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/sum+type">sum type</a> (<a class="existingWikiWord" href="/nlab/show/disjunction">disjunction</a>)</td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><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></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/empty+type">empty type</a> (<a class="existingWikiWord" href="/nlab/show/false">false</a>)</td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><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></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/unit+type">unit type</a> (<a class="existingWikiWord" href="/nlab/show/true">true</a>)</td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>=</mo></mrow><annotation encoding="application/x-tex">=</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/identity+type">identity type</a> (<a class="existingWikiWord" href="/nlab/show/equality">equality</a>)</td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≃</mo></mrow><annotation encoding="application/x-tex">\simeq</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/equivalence+of+types">equivalence of types</a> (<a class="existingWikiWord" href="/nlab/show/logical+equivalence">logical equivalence</a>)</td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo></mrow><annotation encoding="application/x-tex">\sum</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/dependent+sum+type">dependent sum type</a> (<a class="existingWikiWord" href="/nlab/show/existential+quantifier">existential quantifier</a>)</td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo></mrow><annotation encoding="application/x-tex">\prod</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/dependent+product+type">dependent product type</a> (<a class="existingWikiWord" href="/nlab/show/universal+quantifier">universal quantifier</a>)</td></tr> <tr><td style="text-align: left;"></td><td style="text-align: left;"></td></tr> <tr><td style="text-align: left;"><strong>symbol</strong></td><td style="text-align: left;"><strong>in <a class="existingWikiWord" href="/nlab/show/linear+logic">linear logic</a></strong></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊸</mo></mrow><annotation encoding="application/x-tex">\multimap</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/linear+implication">linear implication</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊗</mo></mrow><annotation encoding="application/x-tex">\otimes</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/multiplicative+conjunction">multiplicative conjunction</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊕</mo></mrow><annotation encoding="application/x-tex">\oplus</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/additive+disjunction">additive disjunction</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>&</mi></mrow><annotation encoding="application/x-tex">\&</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/additive+conjunction">additive conjunction</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⅋</mo></mrow><annotation encoding="application/x-tex">\invamp</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/multiplicative+disjunction">multiplicative disjunction</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mspace width="thickmathspace"></mspace><mo>!</mo></mrow><annotation encoding="application/x-tex">\;!</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/exponential+conjunction">exponential conjunction</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mspace width="thickmathspace"></mspace><mo>?</mo></mrow><annotation encoding="application/x-tex">\;?</annotation></semantics></math><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/exponential+disjunction">exponential disjunction</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math></td></tr> </tbody></table> </div> <h2 id="references">References</h2> <p>In</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Georg+Hegel">Georg Hegel</a>, <em><a class="existingWikiWord" href="/nlab/show/Science+of+Logic">Science of Logic</a></em>, 1812</li> </ul> <p>equality is the subject of volume 1, book 2 “Die Lehre vom Wesen” (The doctrine of essence). As discussed at <em><a class="existingWikiWord" href="/nlab/show/Science+of+Logic">Science of Logic</a></em>, one can roughly identify in Hegel’s text there the notion of intensional identity and of the reflector term in <a class="existingWikiWord" href="/nlab/show/identity+types">identity types</a>.</p> <p>Texts on <a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a> typically deal with the subtleties of the notion of <em>equality</em>. For instance</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Per+Martin-L%C3%B6f">Per Martin-Löf</a>, <em>Intuitionistic type theory</em>, Lecture notes (1980)</li> </ul> <p>Besides</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Kurt+G%C3%B6del">Kurt Gödel</a>, <em>Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes</em>. Dialectica (1958), pp. 280–287,</li> </ul> <p>which might be the first paper to mention intensional equality (and the fact that it should be decidable), there is</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Nicolaas+de+Bruijn">Nicolaas de Bruijn</a>, <em><a class="existingWikiWord" href="/nlab/show/Automath">Automath</a></em>,</li> </ul> <p>where de Bruijn makes a distinction between definitional equality and “book” equality.</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Kevin+Buzzard">Kevin Buzzard</a>, <em>Grothendieck’s use of equality</em> (<a href="https://arxiv.org/abs/2405.10387">arXiv:2405.10387</a>)</li> </ul> </body></html> </div> <div class="revisedby"> <p> Last revised on March 28, 2025 at 13:34:37. See the <a href="/nlab/history/equality" 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/equality" accesskey="E" class="navlink" id="edit" rel="nofollow">Edit</a><a href="https://nforum.ncatlab.org/discussion/3749/#Item_65">Discuss</a><span class="backintime"><a href="/nlab/revision/equality/58" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/diff/equality" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Changes from previous revision</a><a href="/nlab/history/equality" accesskey="S" class="navlink" id="history" rel="nofollow">History (58 revisions)</a> <a href="/nlab/show/equality/cite" style="color: black">Cite</a> <a href="/nlab/print/equality" accesskey="p" id="view_print" rel="nofollow">Print</a> <a href="/nlab/source/equality" id="view_source" rel="nofollow">Source</a> </div> </div>  </div>  </body> </html>