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> principle of equivalence 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> principle of equivalence </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/4201/#Item_47" 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> </div> </div> <h1 id="contents">Contents</h1> <div class='maruku_toc'> <ul> <li><a href='#Idea'>Idea</a></li> <li><a href='#terminology'>Terminology</a></li> <li><a href='#motivation'>Motivation</a></li> <ul> <li><a href='#from_mathematical_practice'>From mathematical practice</a></li> <li><a href='#from_foundations_and_logic'>From foundations and logic</a></li> <li><a href='#from_philosophy'>From philosophy</a></li> </ul> <li><a href='#general_definition'>General definition</a></li> <li><a href='#examples'>Examples</a></li> <ul> <li><a href='#in_category_theory'>In category theory</a></li> <ul> <li><a href='#identityonobjects_functors'>Identity-on-objects functors</a></li> <li><a href='#daggers'>In the concept of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>†</mo></mrow><annotation encoding="application/x-tex">\dagger</annotation></semantics></math>-categories</a></li> <ul> <li><a href='#historical_comments'>Historical comments</a></li> </ul> <li><a href='#in_higher_category_theory'>In higher category theory</a></li> </ul> <li><a href='#in_physics'>In physics</a></li> <ul> <li><a href='#in_gauge_theory'>In gauge theory</a></li> <li><a href='#in_gravity'>In gravity</a></li> </ul> </ul> <li><a href='#Breaking'>How to break equivalence-invariance</a></li> <li><a href='#References'>References</a></li> </ul> </div> <h2 id="Idea">Idea</h2> <p>Sensible reasoning in <a class="existingWikiWord" href="/nlab/show/mathematics">mathematics</a> in general, and particularly in <a class="existingWikiWord" href="/nlab/show/higher+structures">higher structures</a>, such as (<a class="existingWikiWord" href="/nlab/show/higher+category+theory">higher</a>) <a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a>, <a class="existingWikiWord" href="/nlab/show/homotopy+theory">homotopy theory</a>, <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a>, etc., should be suitably <a class="existingWikiWord" href="/nlab/show/invariant">invariant</a> under the respective notion of <em><a class="existingWikiWord" href="/nlab/show/equivalence">equivalence</a></em>. This is a common issue whenever some structure is <em><a class="existingWikiWord" href="/nlab/show/generators+and+relations">presented</a></em> by other structures, since the notion of equivalence of the presentation can be finer than that of the notion being presented.</p> <p>For instance, a <a class="existingWikiWord" href="/nlab/show/category">category</a> can be presented by a <a class="existingWikiWord" href="/nlab/show/simplicial+set">simplicial set</a> (the <a class="existingWikiWord" href="/nlab/show/nerve">nerve</a> of a corresponding <a class="existingWikiWord" href="/nlab/show/strict+category">strict category</a>, see <a href="nerve#NerveOfACategory">there</a>), but <a class="existingWikiWord" href="/nlab/show/isomorphism">isomorphism</a> of simplicial sets is much finer than <a class="existingWikiWord" href="/nlab/show/equivalence+of+categories">equivalences</a> of their corresponding categories. It is generally a <em>mistake</em> to mix up these two levels and, for instance, assign to a category properties that are shared only by <em>some</em> of the simplicial sets representing it, say, by distinguishing between <a class="existingWikiWord" href="/nlab/show/isomorphism">isomorphic</a> <a class="existingWikiWord" href="/nlab/show/objects">objects</a>. This <em>breaks the equivalence invariance</em>. (However, see <a href="#Breaking">below</a>.)</p> <p>The ideas here generalize in many directions. For example, not only properties, but also constructions involving categories and functors, can fail to preserve equivalences.</p> <h2 id="terminology">Terminology</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Michael+Makkai">Michael Makkai</a> proposed the <em>Principle of Isomorphism</em>, “all grammatically correct properties of objects of a fixed category are to be invariant under isomorphism”, in his <a href="https://projecteuclid.org/ebooks/lecture-notes-in-logic/Logic%20Colloquium%20'95:%20Proceedings%20of%20the%20Annual%20European%20Summer%20Meeting%20of%20the%20Association%20of%20Symbolic%20Logic,%20held%20in%20Haifa,%20Israel,%20August%209-18,%201995/chapter/Towards%20a%20Categorical%20Foundation%20of%20Mathematics/lnl/1235415906">paper</a></p> <p>“Towards a categorical foundation of mathematics”, in Johann A. Makowsky, Elena V. Ravve, eds., Logic Colloquium ‘95: Proceedings of the Annual European Summer Meeting of the Association of Symbolic Logic, held in Haifa, Israel, August 9-18, 1995 (Berlin: Springer-Verlag, 1998), 153-190.</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Peter+Aczel">Peter Aczel</a> mentioned a similar concept, the <em><a class="existingWikiWord" href="/nlab/show/structure+identity+principle">Structure Identity Principle</a></em>, “isomorphic structures have the same structural properties” in Oberwolfach <a href="http://www.mfo.de/document/1145/OWR_2011_52.pdf">report 52/2011</a>. This seems a priori a little weaker to <a class="existingWikiWord" href="/nlab/show/David+Roberts">me</a>, but if we demand that objects should be seen as only having structural properties (as opposed to the category of <a class="existingWikiWord" href="/nlab/show/ZF">ZF</a>-<a class="existingWikiWord" href="/nlab/show/sets">sets</a>), then we look like we get back the Principle of Isomorphism.</p> </li> <li> <p>A very precise way of stating this idea is encapsulated in <a class="existingWikiWord" href="/nlab/show/Vladimir+Voevodsky">Vladimir Voevodsky</a>‘s <a class="existingWikiWord" href="/nlab/show/univalence+axiom">univalence axiom</a>, which is a fundamental part of <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a> as a <a class="existingWikiWord" href="/nlab/show/foundation">foundation</a> for mathematics. By identifying equivalences/isomorphisms with inhabitants of an <a class="existingWikiWord" href="/nlab/show/identity+type">identity type</a>, it ensures that all properties and structure which can be expressed within the formal <a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a> are invariant under such (see <a href="#AhrensNorth18">AhrensNorth18</a>).</p> </li> <li id="evil"> <p>Floating around the web (and maybe the <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>n</mi></mrow><annotation encoding="application/x-tex">n</annotation></semantics></math>Lab) is the idea of half-jokingly referring to a breaking of equivalence invariance as “evil”. This is probably meant as a pedagogical way of amplifying that it is to be avoided.</p> </li> </ul> <h2 id="motivation">Motivation</h2> <h3 id="from_mathematical_practice">From mathematical practice</h3> <p>…</p> <blockquote> <p>Draw an analogy with vector spaces (maybe just finite-dimensional ones?). We can <em>use</em> a basis to study a vector space, but the basis is not <em>part of</em> the vector space. Even if we use a foundation of mathematics in which the basis literally is part of the vector space (which arguably was the case for 18th-century linear algebra, which studied only Cartesian spaces; and is still the case today if we study finite-dimensional vector spaces using a foundational type theory with propositions as types, but probably this is too obscure), anything that we consider to be a property <em>of the vector space</em> should be independent of the basis. We can make this precise by comparing the groupoids <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Vect</mi> <mo>∼</mo></msub></mrow><annotation encoding="application/x-tex">Vect_\sim</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Vect</mi> <mi>b</mi></msub></mrow><annotation encoding="application/x-tex">Vect_b</annotation></semantics></math>.</p> </blockquote> <p>…</p> <h3 id="from_foundations_and_logic">From foundations and logic</h3> <p>In <a class="existingWikiWord" href="/nlab/show/material+set+theory">material set theory</a> based on <a class="existingWikiWord" href="/nlab/show/ZFC">ZFC</a>, any two objects are <a class="existingWikiWord" href="/nlab/show/pure+sets">pure sets</a> and can be compared for <a class="existingWikiWord" href="/nlab/show/equality">equality</a>. Yet this is often mathematical nonsense which depends on precisely how one writes definitions; for example, the <a class="existingWikiWord" href="/nlab/show/ordered+pair">ordered pair</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mn>0</mn><mo>,</mo><mn>0</mn><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(0,0)</annotation></semantics></math> is equal to the <a class="existingWikiWord" href="/nlab/show/natural+number">natural number</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>1</mn></mrow><annotation encoding="application/x-tex">1</annotation></semantics></math> by some standards and equal to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>2</mn></mrow><annotation encoding="application/x-tex">2</annotation></semantics></math> by other standards (while <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mn>1</mn><mo>,</mo><mn>1</mn><mo stretchy="false">)</mo><mo>=</mo><mn>2</mn></mrow><annotation encoding="application/x-tex">(1,1) = 2</annotation></semantics></math> by yet other standards), but this makes no difference mathematically. In contrast, <a class="existingWikiWord" href="/nlab/show/structural+set+theory">structural set theory</a> either implicitly (as in <a class="existingWikiWord" href="/nlab/show/ETCS">ETCS</a>) or explicitly (as in <a class="existingWikiWord" href="/nlab/show/SEAR">SEAR</a> or <a class="existingWikiWord" href="/nlab/show/ETCS+with+elements">ETCS with elements</a>) considers only equality between <a class="existingWikiWord" href="/nlab/show/elements">elements</a> of a given <a class="existingWikiWord" href="/nlab/show/set">set</a> (or <a class="existingWikiWord" href="/nlab/show/functions">functions</a> or <a class="existingWikiWord" href="/nlab/show/binary+relations">binary relations</a> between two given sets, etc). This can be built into the <a class="existingWikiWord" href="/nlab/show/logic">logic</a> using <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a> (which can serve as a foundation all by itself). The result is that, depending on precisely how one writes definitions, it may or may not be possible to compare two things for equality. For example, the ordered pair <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mn>1</mn><mo>,</mo><mn>1</mn><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(1, 1)</annotation></semantics></math> is equal to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>2</mn></mrow><annotation encoding="application/x-tex">2</annotation></semantics></math> under triangular encoding, equal to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>3</mn></mrow><annotation encoding="application/x-tex">3</annotation></semantics></math> under binary encoding, and equal to <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> under Chinese Remainder encoding. But if we take ordered pairs as primitive, it makes no sense to compare <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mn>1</mn><mo>,</mo><mn>1</mn><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(1, 1)</annotation></semantics></math> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>2</mn></mrow><annotation encoding="application/x-tex">2</annotation></semantics></math>. (Of course, we could do this in material set theory as well; but allowing non-set primitives there would defeat the traditional attraction of the theory.)</p> <p>Does it make sense, then, to ask whether two arbitrary <em>sets</em> are equal? In material set theory, of course it does; two sets are equal if they have the same elements (by the <a class="existingWikiWord" href="/nlab/show/axiom+of+extensionality">axiom of extensionality</a>). But structurally, this definition is meaningless. All the same, a structural set theory built on <a class="existingWikiWord" href="/nlab/show/first-order+logic">first-order logic</a> with equality automatically gives this question (whether two arbitrary sets are equal) a meaning, as do the most common forms of foundational type theory, but this is again never used in mathematics. (<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>SEAR</mi></mrow><annotation encoding="application/x-tex">SEAR</annotation></semantics></math>, which is based on first-order logic without equality, does not give this question a meaning and does not suffer for it.) So just as we don't need to ask whether <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mn>0</mn><mo>,</mo><mn>0</mn><mo stretchy="false">)</mo><mo>=</mo><mn>2</mn></mrow><annotation encoding="application/x-tex">(0,0) = 2</annotation></semantics></math>, we don't need to ask whether <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">{</mo><mo stretchy="false">(</mo><mn>0</mn><mo>,</mo><mn>0</mn><mo stretchy="false">)</mo><mo stretchy="false">}</mo><mo>=</mo><mo stretchy="false">{</mo><mn>2</mn><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\{(0,0)\} = \{2\}</annotation></semantics></math> as sets. (Note that this is a completely different question, structurally, from whether, say, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">{</mo><mo stretchy="false">(</mo><mn>0</mn><mo>,</mo><mn>0</mn><mo stretchy="false">)</mo><mo stretchy="false">}</mo><mo>=</mo><mo stretchy="false">{</mo><mn>2</mn><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\{(0,0)\} = \{2\}</annotation></semantics></math> as <em><a class="existingWikiWord" href="/nlab/show/subsets">subsets</a></em> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℕ</mi><mo lspace="thinmathspace" rspace="thinmathspace">∐</mo><mo stretchy="false">(</mo><mi>ℕ</mi><mo>×</mo><mi>ℕ</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathbb{N} \coprod (\mathbb{N} \times \mathbb{N})</annotation></semantics></math>.)</p> <p>Now let us move from the foundations of <a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a> to those of <a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a>. Usually, category theory is founded on set theory, or something very much like it; if the <a class="existingWikiWord" href="/nlab/show/objects">objects</a> of a category don't form a set, then this is only because of <a class="existingWikiWord" href="/nlab/show/size+issues">size issues</a>, and they still form a <a class="existingWikiWord" href="/nlab/show/proper+class">proper class</a>. Accordingly, it makes sense to compare them for equality. However, if the <a class="existingWikiWord" href="/nlab/show/category+of+sets">category of sets</a> is itself an example of a category, then by the previous paragraph, it does <em>not</em> have to make sense (and is mathematically meaningless) to test the objects of this category for equality. So we get the idea that we cannot compare objects of a given category for equality in general (although this may make sense for particular categories). In other words, a <a class="existingWikiWord" href="/nlab/show/category">category</a> is not by default a <a class="existingWikiWord" href="/nlab/show/strict+category">strict category</a> (a category equipped with the <a class="existingWikiWord" href="/nlab/show/extra+stuff">extra stuff</a> of an explicit equality predicate on its objects).</p> <p>We can found mathematics on type theory without identity types, and then it is literally true that (in general) it makes no sense to compare objects of a given type for equality; one has to <em>define</em> a relevant equality predicate when there is one. From the other direction, we can found mathematics on (weak) <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>∞</mn></mrow><annotation encoding="application/x-tex">\infty</annotation></semantics></math>-<a class="existingWikiWord" href="/nlab/show/infinity-groupoid">infinity-groupoid</a> theory, i.e. <a class="existingWikiWord" href="/nlab/show/homotopy+theory">homotopy theory</a> (as in <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a>), where the automatic notion of equality between object of a category is actually only isomorphism.</p> <p>However, these are not commonly used foundations. Therefore, category theory is usually written in a language in which it does literally make sense to ask whether two objects of a given category are equal (meaning something stronger than that they are isomorphic), whether two functors between two given categories are equal, etc. If we want these definitions to make sense in the general mathematical situation (where <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> is an example of a category, even though comparing two arbitrary sets for equality makes no mathematical sense), then we need to check that our definitions are compatible with the principle of equivalence.</p> <p>(Strictly speaking, it does not even make sense to ask if two arbitrary sets are isomorphic; going back to our earlier example, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">{</mo><mo stretchy="false">(</mo><mn>0</mn><mo>,</mo><mn>0</mn><mo stretchy="false">)</mo><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\{(0,0)\}</annotation></semantics></math> is isomorphic to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">{</mo><mn>2</mn><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\{2\}</annotation></semantics></math> as objects of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> because they are both singletons, but they are not isomorphic as objects of the poset of subsets of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℕ</mi><mo>+</mo><mi>ℕ</mi><mo>×</mo><mi>ℕ</mi></mrow><annotation encoding="application/x-tex">\mathbb{N} + \mathbb{N}\times \mathbb{N}</annotation></semantics></math>, because neither is a subset of the other.)</p> <h3 id="from_philosophy">From philosophy</h3> <p>In <a class="existingWikiWord" href="/nlab/show/Tractatus+Logico-Philosophicus">Tractatus Logico-Philosophicus</a>, 2.02331, <a class="existingWikiWord" href="/nlab/show/Wittgenstein">Wittgenstein</a> writes</p> <blockquote> <p>Either a thing has properties that nothing else has, in which case we can immediately use a description to distinguish it from the others and refer to it; or, on the other hand, there are several things that have the whole set of their properties in common, in which case it is quite impossible to indicate one of them. For if there is nothing to distinguish a thing, I cannot distinguish it, since otherwise it would be distinguished after all.</p> </blockquote> <p>Given that a main theme of the Tractatus is on the limits of language, it is tempting to consider this as a description not just for ‘the world’ (as in <em>Tractatus</em> 1.), but for any given language and the objects about which one reasons in that language. This seems to encapsulate Makkai’s motivation alluded to above.</p> <h2 id="general_definition">General definition</h2> <p>If <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> is an <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>∞</mn></mrow><annotation encoding="application/x-tex">\infty</annotation></semantics></math>-<a class="existingWikiWord" href="/nlab/show/infinity-groupoid">groupoid</a>, then a property <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> of objects of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> is <em>compatible with equivalence</em> if, whenever <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">P(a)</annotation></semantics></math> holds for an object <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> of <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>b</mi></mrow><annotation encoding="application/x-tex">b</annotation></semantics></math> is <a class="existingWikiWord" href="/nlab/show/equivalence">equivalent</a> (as an object of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math>) to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi></mrow><annotation encoding="application/x-tex">a</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo stretchy="false">(</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">P(b)</annotation></semantics></math> holds. Alternatively, an operation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi></mrow><annotation encoding="application/x-tex">f</annotation></semantics></math> from objects of <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 objects of (another <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>∞</mn></mrow><annotation encoding="application/x-tex">\infty</annotation></semantics></math>-groupoid) <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> is <strong>compatible with equivalence</strong> if, whenever <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi></mrow><annotation encoding="application/x-tex">a</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi></mrow><annotation encoding="application/x-tex">b</annotation></semantics></math> are equivalent objects of <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>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f(a)</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo stretchy="false">(</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f(b)</annotation></semantics></math> are equivalent objects of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Y</mi></mrow><annotation encoding="application/x-tex">Y</annotation></semantics></math>.</p> <p>(Note that everything is an object of some <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>∞</mn></mrow><annotation encoding="application/x-tex">\infty</annotation></semantics></math>-groupoid. For example, a <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>2</mn></mrow><annotation encoding="application/x-tex">2</annotation></semantics></math>-morphism in some random <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>5</mn></mrow><annotation encoding="application/x-tex">5</annotation></semantics></math>-category is an object of a hom-<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>3</mn></mrow><annotation encoding="application/x-tex">3</annotation></semantics></math>-category, which has an <a class="existingWikiWord" href="/nlab/show/core">underlying</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>3</mn></mrow><annotation encoding="application/x-tex">3</annotation></semantics></math>-groupoid, which is a special kind of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>∞</mn></mrow><annotation encoding="application/x-tex">\infty</annotation></semantics></math>-groupoid. For some purposes, this <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>2</mn></mrow><annotation encoding="application/x-tex">2</annotation></semantics></math>-morphism may instead need to be seen as an object in a <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>2</mn></mrow><annotation encoding="application/x-tex">2</annotation></semantics></math>-arrow <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>5</mn></mrow><annotation encoding="application/x-tex">5</annotation></semantics></math>-category, which has an underlying <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>∞</mn></mrow><annotation encoding="application/x-tex">\infty</annotation></semantics></math>-groupoid as well; exactly which <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>∞</mn></mrow><annotation encoding="application/x-tex">\infty</annotation></semantics></math>-groupoid is relevant depends on the <a class="existingWikiWord" href="/nlab/show/context">context</a>. Also note that we really do need <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>∞</mn></mrow><annotation encoding="application/x-tex">\infty</annotation></semantics></math>-groupoids here, rather than <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>∞</mn></mrow><annotation encoding="application/x-tex">\infty</annotation></semantics></math>-categories, since dualities do respect equivalences.)</p> <p>The operation-version of the principle of equivalence gives the property-version if you think of a property as an operation taking values in the <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>∞</mn></mrow><annotation encoding="application/x-tex">\infty</annotation></semantics></math>-groupoid (in fact a <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>0</mn></mrow><annotation encoding="application/x-tex">0</annotation></semantics></math>-groupoid, or <a class="existingWikiWord" href="/nlab/show/set">set</a>) of <a class="existingWikiWord" href="/nlab/show/truth+value">truth values</a>. (The property-version also gives the operation-version, although that is a little more involved.) An operation will obey the principle of equivalence if it is given (as the object-operation) by a <a class="existingWikiWord" href="/nlab/show/functor">functor</a> (’<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>∞</mn></mrow><annotation encoding="application/x-tex">\infty</annotation></semantics></math>-functor’, if you prefer). A property adheres to the principle of equivalence precisely if it's a functor to the <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>∞</mn></mrow><annotation encoding="application/x-tex">\infty</annotation></semantics></math>-groupoid of truth values.</p> <p>This definition should be the conclusion of a theorem that using certain language (including avoiding equations between objects of a category) makes it impossible to say anything that violates the principle of equivalence. <a class="existingWikiWord" href="/nlab/show/Michael+Makkai">Michael Makkai</a> works on such a language, <a class="existingWikiWord" href="/nlab/show/FOLDS">FOLDS</a> (‘first-order logic with dependent sorts’), which does not include an axiomatic notion of <a class="existingWikiWord" href="/nlab/show/equality">equality</a> at all. This pertains to the <a href="foundations#MFCT">mathematical foundations of category theory</a>. To learn more, see his paper <em><a href="http://www.math.mcgill.ca/makkai/">First Order Logic with Dependent Sorts, with Applications to Category Theory</a></em>.</p> <h2 id="examples">Examples</h2> <h3 id="in_category_theory">In category theory</h3> <p>A common misconception in category theory is that <a class="existingWikiWord" href="/nlab/show/strict+categories">strict categories</a> violate the principle of equivalence. However, this is not true; strict categories are the mathematical structures in which the equivalence of objects are precisely equality on objects: important examples of strict categories which do not violate the principle of equivalence include <a class="existingWikiWord" href="/nlab/show/posets">posets</a> and the <a class="existingWikiWord" href="/nlab/show/walking+parallel+pair">walking parallel pair</a>. In fact, every strict category is equivalent to a <a class="existingWikiWord" href="/nlab/show/setoid">setoid</a>-valued <a class="existingWikiWord" href="/nlab/show/presheaf">presheaf</a> on the <a class="existingWikiWord" href="/nlab/show/simplex+category">simplex category</a> or the full subcategory of the <a class="existingWikiWord" href="/nlab/show/arrow+category">arrow category</a> of the <a class="existingWikiWord" href="/nlab/show/%282%2C1%29-category">(2,1)-category</a> of <a class="existingWikiWord" href="/nlab/show/weak+categories">weak categories</a>, consisting of <a class="existingWikiWord" href="/nlab/show/essentially+surjective+functors">essentially surjective functors</a> whose <a class="existingWikiWord" href="/nlab/show/domain">domain</a> is a <a class="existingWikiWord" href="/nlab/show/setoid">setoid</a>.</p> <p>Instead, what does break the principle of equivalence is to say that certain <a class="existingWikiWord" href="/nlab/show/concrete+categories">concrete categories</a> with non-trivial <a class="existingWikiWord" href="/nlab/show/automorphisms">automorphisms</a> such as <a class="existingWikiWord" href="/nlab/show/Set">Set</a> or <a class="existingWikiWord" href="/nlab/show/Grp">Grp</a> are strict categories, as the objects of the categories are <a class="existingWikiWord" href="/nlab/show/sets">sets</a>, and equality of objects is equality of sets. In this case, one has to instead say that they are <a class="existingWikiWord" href="/nlab/show/isomorphism">isomorphic</a> and then (usually) impose some <a class="existingWikiWord" href="/nlab/show/coherence+relation">coherence relation</a> on the relevant family of isomorphisms. But of course, this is more complicated!</p> <h4 id="identityonobjects_functors">Identity-on-objects functors</h4> <p>The concept of an <a class="existingWikiWord" href="/nlab/show/identity-on-objects+functor">identity-on-objects functor</a> appears in category theory as well, particularly when defining <a class="existingWikiWord" href="/nlab/show/Freyd+categories">Freyd categories</a> and <a class="existingWikiWord" href="/nlab/show/dagger+categories">dagger categories</a>. The traditional definition goes as follows:</p> <p> <div class='num_defn'> <h6>Definition</h6> <p>An <strong>identity-on-objects <a class="existingWikiWord" href="/nlab/show/functor">functor</a></strong> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi><mo>:</mo><mi>A</mi><mo>→</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">F: A\to B</annotation></semantics></math> between <a class="existingWikiWord" href="/nlab/show/categories">categories</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math> is a functor between categories with the same collection of <a class="existingWikiWord" href="/nlab/show/objects">objects</a>, and has as its underlying object function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>F</mi> <mi>ob</mi></msub></mrow><annotation encoding="application/x-tex">F_{ob}</annotation></semantics></math> the <a class="existingWikiWord" href="/nlab/show/identity+function">identity function</a> on the collection of objects.</p> </div> </p> <p>However, in <a class="existingWikiWord" href="/nlab/show/material+set+theories">material set theories</a> or material class theories, “having the same collection of objects” is sometimes defined as <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Ob</mi><mo>=</mo><mi>ob</mi><mo stretchy="false">(</mo><mi>A</mi><mo stretchy="false">)</mo><mo>=</mo><mi>ob</mi><mo stretchy="false">(</mo><mi>B</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Ob = ob(A) = ob(B)</annotation></semantics></math>. This definition involves equality of sets, which violates the principle of equality.</p> <p>Instead, what category theorists usually mean by two categories having the same objects is actually having a single <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>Set</mi><mo>×</mo><mi>Set</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(Set \times Set)</annotation></semantics></math>-<a class="existingWikiWord" href="/nlab/show/enriched+category">enriched category</a>, where morphisms are in families of sets of pairs <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>f</mi><mo>,</mo><mi>g</mi><mo stretchy="false">)</mo><mo>:</mo><mi>A</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo>×</mo><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(f,g):A(x,y) \times B(x,y))</annotation></semantics></math> for objects <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>, and composition is composition of pairs of morphisms <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>h</mi><mo>,</mo><mi>k</mi><mo stretchy="false">)</mo><mo>∘</mo><mo stretchy="false">(</mo><mi>f</mi><mo>,</mo><mi>g</mi><mo stretchy="false">)</mo><mo>=</mo><mo stretchy="false">(</mo><mi>h</mi><mo>∘</mo><mi>f</mi><mo>,</mo><mi>k</mi><mo>∘</mo><mi>g</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(h,k)\circ(f,g) = (h \circ f,k \circ g)</annotation></semantics></math> for <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><mi>A</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f:A(x,y)</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>g</mi><mo>:</mo><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">g:B(x,y)</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>h</mi><mo>:</mo><mi>A</mi><mo stretchy="false">(</mo><mi>y</mi><mo>,</mo><mi>z</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">h:A(y,z)</annotation></semantics></math>, and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>k</mi><mo>:</mo><mi>B</mi><mo stretchy="false">(</mo><mi>y</mi><mo>,</mo><mi>z</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">k:B(y,z)</annotation></semantics></math>.</p> <p>Another problem occurs in <a class="existingWikiWord" href="/nlab/show/set+theories">set theories</a> with certain <a class="existingWikiWord" href="/nlab/show/concrete+categories">concrete categories</a> like <a class="existingWikiWord" href="/nlab/show/Rel">Rel</a>, <a class="existingWikiWord" href="/nlab/show/Hilb">Hilb</a>, and the <a class="existingWikiWord" href="/nlab/show/permutation+category">permutation category</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℙ</mi></mrow><annotation encoding="application/x-tex">\mathbb{P}</annotation></semantics></math>: the objects of the categories are sets, and so saying that the underlying function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>F</mi> <mi>ob</mi></msub></mrow><annotation encoding="application/x-tex">F_ob</annotation></semantics></math> on the objects is the identity function violates the principle of equality, because by definition <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>F</mi> <mi>ob</mi></msub><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>=</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">F_ob(x) = x</annotation></semantics></math> for all objects <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 because objects are sets, one is talking about equality of sets.</p> <p>Instead, when category theorists are talking about two categories with the same collection of objects and and identity-on-objects functor, what they really are talking about is an <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>Set</mi> <mi>I</mi></msup></mrow><annotation encoding="application/x-tex">Set^I</annotation></semantics></math>-enriched category, where <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>Set</mi> <mi>I</mi></msup></mrow><annotation encoding="application/x-tex">Set^I</annotation></semantics></math> is the <a class="existingWikiWord" href="/nlab/show/arrow+category">arrow category</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math>.</p> <h4 id="daggers">In the concept of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>†</mo></mrow><annotation encoding="application/x-tex">\dagger</annotation></semantics></math>-categories</h4> <p>A <strong><a class="existingWikiWord" href="/nlab/show/%E2%80%A0-category">†-category</a></strong> is a <a class="existingWikiWord" href="/nlab/show/category">category</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> with a function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><msup><mo stretchy="false">)</mo> <mo>†</mo></msup><mo>:</mo><msub><mi>Hom</mi> <mi>C</mi></msub><mo stretchy="false">(</mo><mi>A</mi><mo>,</mo><mi>B</mi><mo stretchy="false">)</mo><mo>→</mo><msub><mi>hom</mi> <mi>C</mi></msub><mo stretchy="false">(</mo><mi>B</mi><mo>,</mo><mi>A</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(-)^\dagger: Hom_C(A,B) \to hom_C(B,A)</annotation></semantics></math> for every object <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>,</mo><mi>B</mi><mo>∈</mo><mi>Ob</mi><mo stretchy="false">(</mo><mi>C</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">A,B \in Ob(C)</annotation></semantics></math>, such that</p> <ul> <li>For every <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>∈</mo><mi>Ob</mi><mo stretchy="false">(</mo><mi>C</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">A \in Ob(C)</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><msub><mn>1</mn> <mi>A</mi></msub><msup><mo stretchy="false">)</mo> <mo>†</mo></msup><mo>=</mo><msub><mn>1</mn> <mi>A</mi></msub></mrow><annotation encoding="application/x-tex">(1_A)^\dagger = 1_A</annotation></semantics></math></li> <li>For every <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>,</mo><mi>B</mi><mo>∈</mo><mi>Ob</mi><mo stretchy="false">(</mo><mi>C</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">A,B \in Ob(C)</annotation></semantics></math> and every <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>∈</mo><msub><mi>Hom</mi> <mi>C</mi></msub><mo stretchy="false">(</mo><mi>A</mi><mo>,</mo><mi>B</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f \in Hom_C(A,B)</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>g</mi><mo>∈</mo><msub><mi>Hom</mi> <mi>C</mi></msub><mo stretchy="false">(</mo><mi>B</mi><mo>,</mo><mi>C</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">g \in Hom_C(B,C)</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>g</mi><mo>∘</mo><mi>f</mi><msup><mo stretchy="false">)</mo> <mo>†</mo></msup><mo>=</mo><msup><mi>f</mi> <mo>†</mo></msup><mo>∘</mo><msup><mi>g</mi> <mo>†</mo></msup></mrow><annotation encoding="application/x-tex">(g \circ f)^\dagger = f^\dagger \circ g^\dagger</annotation></semantics></math></li> <li>For every <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>,</mo><mi>B</mi><mo>∈</mo><mi>Ob</mi><mo stretchy="false">(</mo><mi>C</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">A,B \in Ob(C)</annotation></semantics></math> and every <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>∈</mo><msub><mi>Hom</mi> <mi>C</mi></msub><mo stretchy="false">(</mo><mi>A</mi><mo>,</mo><mi>B</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f \in Hom_C(A,B)</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mo stretchy="false">(</mo><mi>f</mi><msup><mo stretchy="false">)</mo> <mo>†</mo></msup><msup><mo stretchy="false">)</mo> <mo>†</mo></msup><mo>=</mo><mi>f</mi></mrow><annotation encoding="application/x-tex">((f)^\dagger)^\dagger = f</annotation></semantics></math>.</li> </ul> <p>However, there is another definition of a †-category, as a category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> with a functor</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>F</mi><mo lspace="verythinmathspace">:</mo><mi>C</mi><mo>→</mo><msup><mi>C</mi> <mi>op</mi></msup></mrow><annotation encoding="application/x-tex">F\colon C \to C^{op} </annotation></semantics></math></div> <p>which is the identity on objects and has <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>F</mi> <mn>2</mn></msup><mo>=</mo><mn>1</mn></mrow><annotation encoding="application/x-tex">F^2 = 1</annotation></semantics></math>.</p> <p>This second definition break equivalence-invariance: it imposes equations between objects, so we cannot transport a dagger-category structure along an equivalence of categories.</p> <h5 id="historical_comments">Historical comments</h5> <p>It was once believed that there was no known way to express the idea without equations between objects. This stemmed from the fact that category theorists were using functors to define the dagger. It was only later that it was recognized that one could include the dagger in the definition of dagger categories in the same way that one includes composition of morphisms in the definition of category, which resulted in a definition of dagger category that doesn’t violate the principle of equivalence.</p> <p>A discussion about this is <a href="https://nforum.ncatlab.org/discussion/4201/principle-of-equivalence/?Focus=101442#Comment_101442">archived on the nForum</a>.</p> <h4 id="in_higher_category_theory">In higher category theory</h4> <p>It violates the principle of equivalence to state that two morphisms in a <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>2</mn></mrow><annotation encoding="application/x-tex">2</annotation></semantics></math>-<a class="existingWikiWord" href="/nlab/show/2-category">category</a> are equal, because these morphisms are objects in a <a class="existingWikiWord" href="/nlab/show/hom-category">hom-category</a>, but does not violate the principle of equivalence to state that that two <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>2</mn></mrow><annotation encoding="application/x-tex">2</annotation></semantics></math>-morphisms are equal, given a common source and target. And so on. In an <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>∞</mn></mrow><annotation encoding="application/x-tex">\infty</annotation></semantics></math>-<a class="existingWikiWord" href="/nlab/show/infinity-category">category</a>, <em>every</em> claim of equality break equivalence-invariance.</p> <p>Defining higher categorial structures using such equalities tends to lead to <em>strict</em> concepts; avoiding them and imposing coherence relations leads to <em>weak</em> concepts. Sometimes there is a <a class="existingWikiWord" href="/nlab/show/coherence+theorem">coherence theorem</a> showing that every weak concept can be strictified, which justifies using equality as a figure of speech. See <a class="existingWikiWord" href="/nlab/show/bicategory">bicategory</a>, <a class="existingWikiWord" href="/nlab/show/Gray-category">Gray-category</a>, and <a class="existingWikiWord" href="/nlab/show/model+category">model category</a> for examples of this in action.</p> <h3 id="in_physics">In physics</h3> <p>Since <a class="existingWikiWord" href="/nlab/show/Hilb">Hilb</a> and <a class="existingWikiWord" href="/nlab/show/nCob">nCob</a> are <a class="existingWikiWord" href="/nlab/show/dagger-categories">dagger-categories</a>, the discussion <a href="#daggers">above</a> is relevant, particularly for <a class="existingWikiWord" href="/nlab/show/TQFT">TQFT</a>.</p> <h4 id="in_gauge_theory">In gauge theory</h4> <p>See at</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/gauge+transformation">gauge transformation</a>, <a class="existingWikiWord" href="/nlab/show/gauge+equivalence">gauge equivalence</a>, <a class="existingWikiWord" href="/nlab/show/gauge+invariance">gauge invariance</a></li> </ul> <h4 id="in_gravity">In gravity</h4> <p>The principle of equivalence in <a class="existingWikiWord" href="/nlab/show/general+relativity">general relativity</a> (see <a class="existingWikiWord" href="/nlab/show/equivalence+principle+%28physics%29">equivalence principle (physics)</a>) is a special case of this principle of equivalence; the objects of the <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>∞</mn></mrow><annotation encoding="application/x-tex">\infty</annotation></semantics></math>-groupoid are physical “fields” (not to be confused with algebraic fields!), and the isomorphisms are <a class="existingWikiWord" href="/nlab/show/coordinate+transformation">coordinate transformation</a>s. So physical properties and operations should not depend on the choice of coordinate system, and this is enforced by allowing only functorial operations, which are specifically taken to be generated by <a class="existingWikiWord" href="/nlab/show/trace">trace</a>s, <a class="existingWikiWord" href="/nlab/show/tensor+product">tensor product</a>s, and linear operations acting on the <a class="existingWikiWord" href="/nlab/show/pseudo-Riemannian+metric">pseudo-Riemannian metric</a>, and the <a class="existingWikiWord" href="/nlab/show/covariant+derivative">covariant derivative</a>.</p> <p>See at</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/general+covariance">general covariance</a></li> </ul> <h2 id="Breaking">How to break equivalence-invariance</h2> <p>Just as we can make use of <a class="existingWikiWord" href="/nlab/show/basis">bases</a> in <a class="existingWikiWord" href="/nlab/show/linear+algebra">linear algebra</a>, so we may make use of <a class="existingWikiWord" href="/nlab/show/strict+categories">strict categories</a> to discuss <a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a>. Philosophically, the concept of strict category is not in itself a breaking of equivalence-invariance; what does break equivalence-invariance is to say that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> (and other well-known categories such as <a class="existingWikiWord" href="/nlab/show/Grp">Grp</a>, etc) <em>are</em> strict categories. Mathematically, strict categories form a <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>1</mn></mrow><annotation encoding="application/x-tex">1</annotation></semantics></math>-<a class="existingWikiWord" href="/nlab/show/1-groupoid">groupoid</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Str</mi><msub><mi>Cat</mi> <mo>∼</mo></msub></mrow><annotation encoding="application/x-tex">Str Cat_\sim</annotation></semantics></math> that is different from the <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>2</mn></mrow><annotation encoding="application/x-tex">2</annotation></semantics></math>-<a class="existingWikiWord" href="/nlab/show/2-groupoid">groupoid</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Cat</mi> <mo>∼</mo></msub></mrow><annotation encoding="application/x-tex">Cat_\sim</annotation></semantics></math>, but there is still a canonical <a class="existingWikiWord" href="/nlab/show/pseudo+functor">pseudo functor</a> from <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Str</mi><msub><mi>Cat</mi> <mo>∼</mo></msub></mrow><annotation encoding="application/x-tex">Str Cat_\sim</annotation></semantics></math> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Cat</mi> <mo>∼</mo></msub></mrow><annotation encoding="application/x-tex">Cat_\sim</annotation></semantics></math> that we may find useful.</p> <p>Much as the <a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a> tells us that every vector space has a basis, so the global axiom of choice tells us that every category may be given the structure of a strict category. Then we can use this extra structure (in either case), as long as we prove that the result is independent of the structure chosen. Even if we don't wish to accept the axiom of choice, we can still prove a theorem about those vector spaces that have bases or those categories that can be given a strict structure.</p> <p>Perhaps the extreme case of this is using <a class="existingWikiWord" href="/nlab/show/model+categories">model categories</a> to study <a class="existingWikiWord" href="/nlab/show/homotopy+theory">homotopy theory</a>, which is (from the <a class="existingWikiWord" href="/nlab/show/nPOV">nPOV</a>) really about <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mn>∞</mn><mo>,</mo><mn>1</mn><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(\infty,1)</annotation></semantics></math>-<a class="existingWikiWord" href="/nlab/show/%28infinity%2C1%29-category">categories</a>. Even if model categories are not taken to be strict categories, they still form a <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>2</mn></mrow><annotation encoding="application/x-tex">2</annotation></semantics></math>-groupoid and thus are still far more strict than <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mn>∞</mn><mo>,</mo><mn>1</mn><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(\infty,1)</annotation></semantics></math>-categories, which only form an <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>∞</mn></mrow><annotation encoding="application/x-tex">\infty</annotation></semantics></math>-<a class="existingWikiWord" href="/nlab/show/infinity-groupoid">groupoid</a>. Nevertheless, they are quite useful (at least assuming the axiom of choice?).</p> <h2 id="References">References</h2> <p>A discussion of the principle of equivalence in the very <a class="existingWikiWord" href="/nlab/show/foundations">foundations</a> of mathematics by replacing <a class="existingWikiWord" href="/nlab/show/ZFC">ZFC</a> by <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a> is in</p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Vladimir+Voevodsky">Vladimir Voevodsky</a>, <em>Foundations/formalization of mathematics and homotopy theory</em>, talk at IAS (<a href="http://video.ias.edu/node/68">video</a>)</p> </li> <li id="CoquandDanielsson"> <p><a class="existingWikiWord" href="/nlab/show/Thierry+Coquand">Thierry Coquand</a>, Nils Anders Danielsson, <em>Isomorphism is equality</em> (<a href="http://www.cse.chalmers.se/~nad/publications/coquand-danielsson-isomorphism-is-equality.pdf">pdf</a>)</p> </li> <li id="Awodey14"> <p><a class="existingWikiWord" href="/nlab/show/Steve+Awodey">Steve Awodey</a>, <em>Structuralism, Invariance, and Univalence</em> (2014) (<a href="https://www.andrew.cmu.edu/user/awodey/preprints/siu.pdf">pdf</a>)</p> </li> <li id="AhrensNorth18"> <p><a class="existingWikiWord" href="/nlab/show/Benedikt+Ahrens">Benedikt Ahrens</a>, <a class="existingWikiWord" href="/nlab/show/Paige+Randall+North">Paige Randall North</a>, <em>Univalent foundations and the equivalence principle</em>, (<a href="https://paigenorth.github.io/ep.pdf">pdf</a>)</p> </li> </ul> </body></html> </div> <div class="revisedby"> <p> Last revised on July 28, 2023 at 14:39:26. See the <a href="/nlab/history/principle+of+equivalence" 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/principle+of+equivalence" accesskey="E" class="navlink" id="edit" rel="nofollow">Edit</a><a href="https://nforum.ncatlab.org/discussion/4201/#Item_47">Discuss</a><span class="backintime"><a href="/nlab/revision/principle+of+equivalence/106" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/diff/principle+of+equivalence" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Changes from previous revision</a><a href="/nlab/history/principle+of+equivalence" accesskey="S" class="navlink" id="history" rel="nofollow">History (106 revisions)</a> <a href="/nlab/show/principle+of+equivalence/cite" style="color: black">Cite</a> <a href="/nlab/print/principle+of+equivalence" accesskey="p" id="view_print" rel="nofollow">Print</a> <a href="/nlab/source/principle+of+equivalence" id="view_source" rel="nofollow">Source</a> </div> </div>  </div>  </body> </html>