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> structure (changes) in nLab </title> <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /> <meta name="robots" content="noindex,nofollow" /> <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> structure (changes) </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/diff/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/4103/#Item_33" 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"> <p class="show_diff"> Showing changes from revision #52 to #53: <ins class="diffins">Added</ins> | <del class="diffdel">Removed</del> | <del class="diffmod">Chan</del><ins class="diffmod">ged</ins> </p> <blockquote> <p>This entry is about a general concepts of “mathematical structure” such as formalized by <a class='existingWikiWord' href='/nlab/show/diff/category+theory'>category theory</a> and/or <a class='existingWikiWord' href='/nlab/show/diff/dependent+type+theory'>dependent type theory</a>. This subsumes but is more general than the concept of <a class='existingWikiWord' href='/nlab/show/diff/structure+in+model+theory'>structure in model theory</a>.</p> </blockquote> <div class='rightHandSide'> <div class='toc clickDown' tabindex='0'> <h3 id='context'>Context</h3> <h4 id='mathematics'>Mathematics</h4> <div class='hide'> <ul> <li> <p><strong><a class='existingWikiWord' href='/nlab/show/diff/mathematics'>mathematics</a></strong></p> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/mathematics+resources'>math resources</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/history+of+mathematics'>history of mathematics</a></p> </li> </ul> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/foundation+of+mathematics'>Structural Foundations</a></p> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/logic'>logic</a></p> <ul> <li><a class='existingWikiWord' href='/nlab/show/diff/internal+logic'>internal language</a></li> <li><a class='existingWikiWord' href='/nlab/show/diff/classical+mathematics'>classical mathematics</a></li> <li><a class='existingWikiWord' href='/nlab/show/diff/constructive+mathematics'>constructive mathematics</a></li> <li><a class='existingWikiWord' href='/nlab/show/diff/predicative+mathematics'>predicative mathematics</a></li> <li><a href='http://ncatlab.org/nlab/list/foundational+axiom'>category:foundational axiom</a></li> </ul> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/set+theory'>set theory</a></p> <ul> <li><a class='existingWikiWord' href='/nlab/show/diff/structural+set+theory'>structural set theory</a></li> </ul> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/category+theory'>category theory</a></p> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/Categories+and+Sheaves'>Categories and Sheaves</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/sheaf+and+topos+theory'>topos theory</a></p> <ul> <li><a class='existingWikiWord' href='/nlab/show/diff/Sheaves+in+Geometry+and+Logic'>Sheaves in Geometry and Logic</a></li> </ul> </li> </ul> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/higher+category+theory'>higher category theory</a></p> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/higher+topos+theory'>higher topos theory</a></p> <ul> <li><a class='existingWikiWord' href='/nlab/show/diff/Higher+Topos+Theory'>(∞,1)-topos theory</a> <ul> <li><a class='existingWikiWord' href='/nlab/show/diff/presentations+of+%28infinity%2C1%29-sheaf+%28infinity%2C1%29-toposes'>models for ∞-stack (∞,1)-toposes</a></li> <li><a class='existingWikiWord' href='/nlab/show/diff/cohomology'>cohomology</a></li> </ul> </li> </ul> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/homotopy+theory'>homotopy theory</a></p> <ul> <li><a class='existingWikiWord' href='/nlab/show/diff/stable+homotopy+theory'>stable homotopy theory</a></li> <li><a class='existingWikiWord' href='/nlab/show/diff/rational+homotopy+theory'>rational homotopy theory</a></li> </ul> </li> </ul> </li> </ul> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/topology+and+geometry'>Topology and Geometry</a></p> <ul> <li><a class='existingWikiWord' href='/nlab/show/diff/geometry'>geometry</a> (general list), <a class='existingWikiWord' href='/nlab/show/diff/topology'>topology</a> (general list)</li> <li><a class='existingWikiWord' href='/nlab/show/diff/general+topology'>general topology</a></li> <li><a class='existingWikiWord' href='/nlab/show/diff/differential+topology'>differential topology</a></li> <li><a class='existingWikiWord' href='/nlab/show/diff/differential+geometry'>differential geometry</a> <ul> <li><a class='existingWikiWord' href='/nlab/show/diff/synthetic+differential+geometry'>synthetic differential geometry</a></li> <li><a class='existingWikiWord' href='/nlab/show/diff/symplectic+geometry'>symplectic geometry</a></li> </ul> </li> <li><a class='existingWikiWord' href='/nlab/show/diff/algebraic+geometry'>algebraic geometry</a></li> <li><a class='existingWikiWord' href='/nlab/show/diff/noncommutative+algebraic+geometry'>noncommutative algebraic geometry</a></li> <li><a class='existingWikiWord' href='/nlab/show/diff/noncommutative+geometry'>noncommutative geometry</a> (general flavour)</li> <li><a class='existingWikiWord' href='/nlab/show/diff/higher+geometry'>higher geometry</a></li> </ul> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/algebra'>Algebra</a></p> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/universal+algebra'>universal algebra</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/higher+algebra'>higher algebra</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/homological+algebra'>homological algebra</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/group+theory'>group theory</a>, <a class='existingWikiWord' href='/nlab/show/diff/ring+theory'>ring theory</a></p> <ul> <li><a class='existingWikiWord' href='/nlab/show/diff/representation+theory'>representation theory</a></li> </ul> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/algebraic+approaches+to+differential+calculus'>algebraic approaches to differential calculus</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/counterexamples+in+algebra'>counterexamples in algebra</a></p> </li> </ul> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/analysis'>analysis</a></p> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/nonstandard+analysis'>nonstandard analysis</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/functional+analysis'>functional analysis</a></p> <ul> <li><a class='existingWikiWord' href='/nlab/show/diff/operator+algebra'>operator algebras</a></li> </ul> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/Fourier+transform'>Fourier transform</a></p> </li> </ul> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/Lie+theory'>Lie theory</a></p> <ul> <li><a class='existingWikiWord' href='/nlab/show/diff/infinity-Lie+theory+-+contents'>higher Lie theory</a></li> </ul> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/probability+theory'>probability theory</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/discrete+mathematics'>discrete mathematics</a></p> </li> </ul> </div> <h4 id='mathematics_2'>Mathematics</h4> <div class='hide'> <ul> <li> <p><strong><a class='existingWikiWord' href='/nlab/show/diff/mathematics'>mathematics</a></strong></p> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/mathematics+resources'>math resources</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/history+of+mathematics'>history of mathematics</a></p> </li> </ul> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/foundation+of+mathematics'>Structural Foundations</a></p> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/logic'>logic</a></p> <ul> <li><a class='existingWikiWord' href='/nlab/show/diff/internal+logic'>internal language</a></li> <li><a class='existingWikiWord' href='/nlab/show/diff/classical+mathematics'>classical mathematics</a></li> <li><a class='existingWikiWord' href='/nlab/show/diff/constructive+mathematics'>constructive mathematics</a></li> <li><a class='existingWikiWord' href='/nlab/show/diff/predicative+mathematics'>predicative mathematics</a></li> <li><a href='http://ncatlab.org/nlab/list/foundational+axiom'>category:foundational axiom</a></li> </ul> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/set+theory'>set theory</a></p> <ul> <li><a class='existingWikiWord' href='/nlab/show/diff/structural+set+theory'>structural set theory</a></li> </ul> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/category+theory'>category theory</a></p> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/Categories+and+Sheaves'>Categories and Sheaves</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/sheaf+and+topos+theory'>topos theory</a></p> <ul> <li><a class='existingWikiWord' href='/nlab/show/diff/Sheaves+in+Geometry+and+Logic'>Sheaves in Geometry and Logic</a></li> </ul> </li> </ul> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/higher+category+theory'>higher category theory</a></p> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/higher+topos+theory'>higher topos theory</a></p> <ul> <li><a class='existingWikiWord' href='/nlab/show/diff/Higher+Topos+Theory'>(∞,1)-topos theory</a> <ul> <li><a class='existingWikiWord' href='/nlab/show/diff/presentations+of+%28infinity%2C1%29-sheaf+%28infinity%2C1%29-toposes'>models for ∞-stack (∞,1)-toposes</a></li> <li><a class='existingWikiWord' href='/nlab/show/diff/cohomology'>cohomology</a></li> </ul> </li> </ul> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/homotopy+theory'>homotopy theory</a></p> <ul> <li><a class='existingWikiWord' href='/nlab/show/diff/stable+homotopy+theory'>stable homotopy theory</a></li> <li><a class='existingWikiWord' href='/nlab/show/diff/rational+homotopy+theory'>rational homotopy theory</a></li> </ul> </li> </ul> </li> </ul> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/topology+and+geometry'>Topology and Geometry</a></p> <ul> <li><a class='existingWikiWord' href='/nlab/show/diff/geometry'>geometry</a> (general list), <a class='existingWikiWord' href='/nlab/show/diff/topology'>topology</a> (general list)</li> <li><a class='existingWikiWord' href='/nlab/show/diff/general+topology'>general topology</a></li> <li><a class='existingWikiWord' href='/nlab/show/diff/differential+topology'>differential topology</a></li> <li><a class='existingWikiWord' href='/nlab/show/diff/differential+geometry'>differential geometry</a> <ul> <li><a class='existingWikiWord' href='/nlab/show/diff/synthetic+differential+geometry'>synthetic differential geometry</a></li> <li><a class='existingWikiWord' href='/nlab/show/diff/symplectic+geometry'>symplectic geometry</a></li> </ul> </li> <li><a class='existingWikiWord' href='/nlab/show/diff/algebraic+geometry'>algebraic geometry</a></li> <li><a class='existingWikiWord' href='/nlab/show/diff/noncommutative+algebraic+geometry'>noncommutative algebraic geometry</a></li> <li><a class='existingWikiWord' href='/nlab/show/diff/noncommutative+geometry'>noncommutative geometry</a> (general flavour)</li> <li><a class='existingWikiWord' href='/nlab/show/diff/higher+geometry'>higher geometry</a></li> </ul> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/algebra'>Algebra</a></p> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/universal+algebra'>universal algebra</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/higher+algebra'>higher algebra</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/homological+algebra'>homological algebra</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/group+theory'>group theory</a>, <a class='existingWikiWord' href='/nlab/show/diff/ring+theory'>ring theory</a></p> <ul> <li><a class='existingWikiWord' href='/nlab/show/diff/representation+theory'>representation theory</a></li> </ul> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/algebraic+approaches+to+differential+calculus'>algebraic approaches to differential calculus</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/counterexamples+in+algebra'>counterexamples in algebra</a></p> </li> </ul> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/analysis'>analysis</a></p> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/nonstandard+analysis'>nonstandard analysis</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/functional+analysis'>functional analysis</a></p> <ul> <li><a class='existingWikiWord' href='/nlab/show/diff/operator+algebra'>operator algebras</a></li> </ul> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/Fourier+transform'>Fourier transform</a></p> </li> </ul> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/Lie+theory'>Lie theory</a></p> <ul> <li><a class='existingWikiWord' href='/nlab/show/diff/infinity-Lie+theory+-+contents'>higher Lie theory</a></li> </ul> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/probability+theory'>probability theory</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/discrete+mathematics'>discrete mathematics</a></p> </li> </ul> </div> </div> </div> <h1 id='contents'>Contents</h1> <div class='maruku_toc'><ul><li><a href='#idea'>Idea</a></li><li><a href='#notions_of_structure'>Notions of structure</a></li><li><a href='#examples'>Examples</a></li><li><a href='#InDependentTypeTheory'>Structures in dependent type theory</a><ul><li><a href='#lensed_data_structure'>Lensed data structure</a></li><li><a href='#GroupDataStructure'>Group data structure</a></li><ins class='diffins'><li><a href='#GroupActionStructure'>Group action structure</a></li></ins><li><a href='#RingDataStructure'>Ring data structure</a></li><li><a href='#ModuleDataStructure'>Module data structure</a></li></ul></li><li><a href='#HigherStructuresInHoTT'>Higher structures in homotopy type theory</a><ul><li><a href='#delooping'>Delooping</a></li><li><a href='#higher_delooping'>Higher delooping</a></li></ul></li><li><a href='#related_entries'>Related entries</a></li><li><a href='#references'>References</a><ul><li><a href='#general'>General</a></li><li><a href='#ReferencesInDependentTypeTheory'>In dependent type theory</a></li></ul></li></ul></div> <h2 id='idea'>Idea</h2> <p>It is common in informal language to speak of mathematical objects “equipped with <a class='existingWikiWord' href='/nlab/show/diff/stuff%2C+structure%2C+property'>extra structure</a>” of some sort. The archetypical examples are <a class='existingWikiWord' href='/nlab/show/diff/algebra+over+a+Lawvere+theory'>algebras over a Lawvere theory</a> in <a class='existingWikiWord' href='/nlab/show/diff/Set'>Set</a>: these are <a class='existingWikiWord' href='/nlab/show/diff/set'>sets</a> equipped with the structure of certain algebraic operations. For instance a <a class='existingWikiWord' href='/nlab/show/diff/group'>group</a> <math class='maruku-mathml' display='inline' id='mathml_0b8e6d65960e5d2f2edb3977235800ac8dd17851_1' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>(</mo><mi>G</mi><mo>,</mo><mi>e</mi><mo>,</mo><mo>⋅</mo><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>(G, e, {\cdot})</annotation></semantics></math> is a <a class='existingWikiWord' href='/nlab/show/diff/set'>set</a> <math class='maruku-mathml' display='inline' id='mathml_0b8e6d65960e5d2f2edb3977235800ac8dd17851_2' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>G</mi></mrow><annotation encoding='application/x-tex'>G</annotation></semantics></math> equipped with a binary operation <math class='maruku-mathml' display='inline' id='mathml_0b8e6d65960e5d2f2edb3977235800ac8dd17851_3' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo>⋅</mo><mo>:</mo><mi>G</mi><mo>×</mo><mi>G</mi><mo>→</mo><mi>G</mi></mrow><annotation encoding='application/x-tex'>{\cdot} : G \times G \to G</annotation></semantics></math>, etc.</p> <p>One may formalize the notion of structure using the language of <a class='existingWikiWord' href='/nlab/show/diff/category+theory'>category theory</a>. This is discussed at <em><a class='existingWikiWord' href='/nlab/show/diff/stuff%2C+structure%2C+property'>stuff, structure, property</a></em>. In that formalization <a class='existingWikiWord' href='/nlab/show/diff/object'>objects</a> in some <a class='existingWikiWord' href='/nlab/show/diff/category'>category</a> <math class='maruku-mathml' display='inline' id='mathml_0b8e6d65960e5d2f2edb3977235800ac8dd17851_4' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>D</mi></mrow><annotation encoding='application/x-tex'>D</annotation></semantics></math> are objects in some category <math class='maruku-mathml' display='inline' id='mathml_0b8e6d65960e5d2f2edb3977235800ac8dd17851_5' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>C</mi></mrow><annotation encoding='application/x-tex'>C</annotation></semantics></math> <em>equipped with extra structure</em> if there is a <a class='existingWikiWord' href='/nlab/show/diff/functor'>functor</a> <math class='maruku-mathml' display='inline' id='mathml_0b8e6d65960e5d2f2edb3977235800ac8dd17851_6' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>p</mi><mo lspace='verythinmathspace'>:</mo><mi>D</mi><mo>→</mo><mi>C</mi></mrow><annotation encoding='application/x-tex'>p \colon D \to C</annotation></semantics></math> such that</p> <ul> <li><math class='maruku-mathml' display='inline' id='mathml_0b8e6d65960e5d2f2edb3977235800ac8dd17851_7' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>p</mi></mrow><annotation encoding='application/x-tex'>p</annotation></semantics></math> is a <a class='existingWikiWord' href='/nlab/show/diff/faithful+functor'>faithful functor</a>.</li> </ul> <p id='InCategoryTheory'> Depending on author and situation, more properties are required of this functor (<a href='#Ehresmann57'>Ehresmann 57</a>, <a href='#Ehresmann65'>Ehresmann 65</a>, <a href='#AdamekRosickyVitale'>Adamek-Rosicky-Vitale 09, remark 13.18</a>):</p> <ul> <li> <p><math class='maruku-mathml' display='inline' id='mathml_0b8e6d65960e5d2f2edb3977235800ac8dd17851_8' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>p</mi></mrow><annotation encoding='application/x-tex'>p</annotation></semantics></math> is an <a class='existingWikiWord' href='/nlab/show/diff/amnestic+functor'>amnestic functor</a> (<math class='maruku-mathml' display='inline' id='mathml_0b8e6d65960e5d2f2edb3977235800ac8dd17851_9' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>p</mi></mrow><annotation encoding='application/x-tex'>p</annotation></semantics></math>-vertical <a class='existingWikiWord' href='/nlab/show/diff/isomorphism'>isomorphisms</a> are <a class='existingWikiWord' href='/nlab/show/diff/identity'>identities</a>),</p> </li> <li> <p><math class='maruku-mathml' display='inline' id='mathml_0b8e6d65960e5d2f2edb3977235800ac8dd17851_10' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>p</mi></mrow><annotation encoding='application/x-tex'>p</annotation></semantics></math> is an <a class='existingWikiWord' href='/nlab/show/diff/isofibration'>isofibration</a> (isomorphisms can be lifted along <math class='maruku-mathml' display='inline' id='mathml_0b8e6d65960e5d2f2edb3977235800ac8dd17851_11' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>p</mi></mrow><annotation encoding='application/x-tex'>p</annotation></semantics></math>).</p> </li> </ul> <p id='StrictStructure'> However, notice that these two conditions violate the <a class='existingWikiWord' href='/nlab/show/diff/principle+of+equivalence'>principle of equivalence</a> for <a class='existingWikiWord' href='/nlab/show/diff/category'>categories</a>. In the terminology of <em><a class='existingWikiWord' href='/nlab/show/diff/strict+category'>strict categories</a></em> one might hence refer to these conditions as expressing “strict extra structure”.</p> <h2 id='notions_of_structure'>Notions of structure</h2> <p>A special class of examples of this is the notion of <a class='existingWikiWord' href='/nlab/show/diff/structure+in+model+theory'>structure in model theory</a>. In this case one defines a “language” <math class='maruku-mathml' display='inline' id='mathml_0b8e6d65960e5d2f2edb3977235800ac8dd17851_12' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>L</mi></mrow><annotation encoding='application/x-tex'>L</annotation></semantics></math> that describes the constants, functions (say operations) and relations with which we want to equip sets, and then sets equipped with those operations and relations are called <math class='maruku-mathml' display='inline' id='mathml_0b8e6d65960e5d2f2edb3977235800ac8dd17851_13' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>L</mi></mrow><annotation encoding='application/x-tex'>L</annotation></semantics></math>-<a class='existingWikiWord' href='/nlab/show/diff/structure+in+model+theory'>structures</a> for that language. (Equivalently one might say “sets with <math class='maruku-mathml' display='inline' id='mathml_0b8e6d65960e5d2f2edb3977235800ac8dd17851_14' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>L</mi></mrow><annotation encoding='application/x-tex'>L</annotation></semantics></math>-structure”. Or one might generally say “<math class='maruku-mathml' display='inline' id='mathml_0b8e6d65960e5d2f2edb3977235800ac8dd17851_15' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi></mrow><annotation encoding='application/x-tex'>X</annotation></semantics></math>-structure” for “set with <math class='maruku-mathml' display='inline' id='mathml_0b8e6d65960e5d2f2edb3977235800ac8dd17851_16' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>X</mi></mrow><annotation encoding='application/x-tex'>X</annotation></semantics></math>-structure”.) In this case there is a <a class='existingWikiWord' href='/nlab/show/diff/faithful+functor'>faithful functor</a> from <math class='maruku-mathml' display='inline' id='mathml_0b8e6d65960e5d2f2edb3977235800ac8dd17851_17' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>L</mi></mrow><annotation encoding='application/x-tex'>L</annotation></semantics></math>-structures to their underlying sets, and so this is a special case of the general definition.</p> <p>We instead say <a class='existingWikiWord' href='/nlab/show/diff/model'>model</a> of a <a class='existingWikiWord' href='/nlab/show/diff/theory'>theory</a> when we restrict to those structures which satisfy the axioms of a theory (in other words, satisfy <em>properties</em> specified by the axioms). In this case there is a full and faithful functor from the category of models of a theory <math class='maruku-mathml' display='inline' id='mathml_0b8e6d65960e5d2f2edb3977235800ac8dd17851_18' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>T</mi></mrow><annotation encoding='application/x-tex'>T</annotation></semantics></math> to the category of structures of the underlying language <math class='maruku-mathml' display='inline' id='mathml_0b8e6d65960e5d2f2edb3977235800ac8dd17851_19' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>L</mi><mo stretchy='false'>(</mo><mi>T</mi><mo stretchy='false'>)</mo></mrow><annotation encoding='application/x-tex'>L(T)</annotation></semantics></math>, while the composition of forgetful functors</p> <div class='maruku-equation'><math class='maruku-mathml' display='block' id='mathml_0b8e6d65960e5d2f2edb3977235800ac8dd17851_20' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>Mod</mi> <mi>T</mi></msub><mo>→</mo><msub><mi>Struct</mi> <mrow><mi>L</mi><mo stretchy='false'>(</mo><mi>T</mi><mo stretchy='false'>)</mo></mrow></msub><mo>→</mo><mi>Set</mi></mrow><annotation encoding='application/x-tex'>Mod_T \to Struct_{L(T)} \to Set</annotation></semantics></math></div> <p>is again faithful.</p> <div class='num_remark'> <h6 id='remarks'>Remarks</h6> <p>Thus, the English word “structure” is used in several slightly differing mathematical senses.</p> <ol> <li> <p>Within category theory itself, “structure” can function as a kind of mass noun, as in a phrase like “forgetting structure”. Here it refers to data comprising operations, relations, constants, and <em>also properties</em> borne by models of a theory or relative theory, considered abstractly (for example, the functor <math class='maruku-mathml' display='inline' id='mathml_0b8e6d65960e5d2f2edb3977235800ac8dd17851_21' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>Grp</mi><mo>→</mo><mi>Set</mi></mrow><annotation encoding='application/x-tex'>Grp \to Set</annotation></semantics></math> which forgets group structure, or the functor <math class='maruku-mathml' display='inline' id='mathml_0b8e6d65960e5d2f2edb3977235800ac8dd17851_22' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>Ring</mi><mo>→</mo><mi>Ab</mi></mrow><annotation encoding='application/x-tex'>Ring \to Ab</annotation></semantics></math> which forgets multiplicative structure). On the other hand, it can also operate in the singular, where one says for example “a topological group is a topological space equipped with a group structure, such that…”</p> </li> <li> <p>In model theory, however, the term <em>structure</em> is not a mass noun; it refers to a <em>particular</em> set (or “structures” for a family of sets) together with functions, relations, and elements that interpret the symbols of operations, predicates, and constants of a <em>language</em>. When one adds axioms to a language to make a <em>theory</em>, then a structure of the language where those axioms get interpreted as properties <em>satisfied</em> by the structure is called a <em>model</em> of the theory. Thus, in summary, the category theorist might refer to “the structure of a group” as consisting of a multiplication, a unit, etc., satisfying group axioms, while the model theorist would say that each particular group (like <math class='maruku-mathml' display='inline' id='mathml_0b8e6d65960e5d2f2edb3977235800ac8dd17851_23' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>ℤ</mi></mrow><annotation encoding='application/x-tex'>\mathbb{Z}</annotation></semantics></math>) is a model of a theory of groups. For a model theorist, being a model does entail being a structure for the language of groups, but she would also say that a structure for the language of groups need not satisfy any of the axioms of a group (like associativity or unitality).</p> </li> </ol> </div> <h2 id='examples'>Examples</h2> <p>There are gazillions of examples of objects equipped with extra structure. The most familiar is maybe</p> <ul> <li><a class='existingWikiWord' href='/nlab/show/diff/algebraic+structure'>algebraic structure</a>.</li> </ul> <p>Generally the <a class='existingWikiWord' href='/nlab/show/diff/forgetful+functor'>forgetful functor</a> from a category of algebras over an <a class='existingWikiWord' href='/nlab/show/diff/algebraic+theory'>algebraic theory</a> down to the base category exhibits the equipment with the corresponding algebraic structure.</p> <h2 id='InDependentTypeTheory'>Structures in dependent type theory</h2> <p>In <a class='existingWikiWord' href='/nlab/show/diff/dependent+type+theory'>dependent type theory</a> the notion of “mathematical structure” and/or <em>data structure</em> on a base <math class='maruku-mathml' display='inline' id='mathml_0b8e6d65960e5d2f2edb3977235800ac8dd17851_24' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>B</mi><mspace width='thinmathspace' /><mo lspace='verythinmathspace'>:</mo><mspace width='thinmathspace' /><mi>Type</mi></mrow><annotation encoding='application/x-tex'>B \,\colon\, Type</annotation></semantics></math> is given by iterated <a class='existingWikiWord' href='/nlab/show/diff/dependent+sum+type'>dependent pairings</a> (hence forming “<a class='existingWikiWord' href='/nlab/show/diff/type+telescope'>type telescopes</a>” also called “records” in <a class='existingWikiWord' href='/nlab/show/diff/Coq'>Coq</a>) with <math class='maruku-mathml' display='inline' id='mathml_0b8e6d65960e5d2f2edb3977235800ac8dd17851_25' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>B</mi></mrow><annotation encoding='application/x-tex'>B</annotation></semantics></math>-dependent types encoding operations on/with this type together with their behavioural specification.</p> <p>The following shows some examples, using the notation for <a class='existingWikiWord' href='/nlab/show/diff/dependent+sum+type'>dependent pairs</a> from <a class='existingWikiWord' href='/nlab/show/diff/dependent+functions+and+dependent+pairs+--+table'>here</a>.</p> <p id='StructureIdentityPrinciple'> Via the <a class='existingWikiWord' href='/nlab/show/diff/extension+%28semantics%29'>extensionality</a> principles for <a class='existingWikiWord' href='/nlab/show/diff/dependent+sum+type'>dependent pairs</a> (<a href='dependent+sum+type#ExtensionalityPrinciple'>here</a>) and for <a class='existingWikiWord' href='/nlab/show/diff/dependent+function'>dependent functions</a> (<a href='function+extensionality#StatementForDependentFunctions'>here</a>) such type theoretic structure automatically obey the <em><a class='existingWikiWord' href='/nlab/show/diff/structure+identity+principle'>structure identity principle</a></em>:</p> <p><img src='/nlab/files/DependentPairExtensionality-230121.jpg' width='600' /></p> <p><img src='/nlab/files/DependentFunctionExtensionality-230121.jpg' width='600' /></p> <p>In that any equivalence/identification between pairs of data of the following types are isomorphisms in the sense of bijective <a class='existingWikiWord' href='/nlab/show/diff/homomorphism'>homomorphisms</a>.</p> <h3 id='lensed_data_structure'>Lensed data structure</h3> <p>To say that a given data (base) type <math class='maruku-mathml' display='inline' id='mathml_0b8e6d65960e5d2f2edb3977235800ac8dd17851_26' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>B</mi><mspace width='thinmathspace' /><mo lspace='verythinmathspace'>:</mo><mspace width='thinmathspace' /><mi>Set</mi></mrow><annotation encoding='application/x-tex'>B \,\colon\, Set</annotation></semantics></math> is</p> <ol> <li> <p>equipped with</p> <ol> <li> <p>a <a class='existingWikiWord' href='/nlab/show/diff/function+type'>function</a> <math class='maruku-mathml' display='inline' id='mathml_0b8e6d65960e5d2f2edb3977235800ac8dd17851_27' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>read</mi> <mi>D</mi></msub><mspace width='thinmathspace' /><mo lspace='verythinmathspace'>:</mo><mspace width='thinmathspace' /><mi>B</mi><mo>→</mo><mi>D</mi></mrow><annotation encoding='application/x-tex'>read_D \,\colon\, B \to D </annotation></semantics></math> reading out <math class='maruku-mathml' display='inline' id='mathml_0b8e6d65960e5d2f2edb3977235800ac8dd17851_28' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>D</mi></mrow><annotation encoding='application/x-tex'>D</annotation></semantics></math>-data;</p> </li> <li> <p>a <a class='existingWikiWord' href='/nlab/show/diff/function+type'>function</a> <math class='maruku-mathml' display='inline' id='mathml_0b8e6d65960e5d2f2edb3977235800ac8dd17851_29' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msub><mi>write</mi> <mi>D</mi></msub><mspace width='thinmathspace' /><mo lspace='verythinmathspace'>:</mo><mspace width='thinmathspace' /><mi>D</mi><mo>×</mo><mi>B</mi><mo>→</mo><mi>B</mi></mrow><annotation encoding='application/x-tex'>write_D \,\colon\, D \times B \to B</annotation></semantics></math> (over-)writing <math class='maruku-mathml' display='inline' id='mathml_0b8e6d65960e5d2f2edb3977235800ac8dd17851_30' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>D</mi></mrow><annotation encoding='application/x-tex'>D</annotation></semantics></math>-data;</p> </li> </ol> </li> <li> <p>such that this does behave as expected, namely as a <a href='lens+in+computer+science#LensesAreCostateCoalgebras'>well-behaved</a> <math class='maruku-mathml' display='inline' id='mathml_0b8e6d65960e5d2f2edb3977235800ac8dd17851_31' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>D</mi></mrow><annotation encoding='application/x-tex'>D</annotation></semantics></math>-<a class='existingWikiWord' href='/nlab/show/diff/lens+%28in+computer+science%29'>lens</a>-structure on <math class='maruku-mathml' display='inline' id='mathml_0b8e6d65960e5d2f2edb3977235800ac8dd17851_32' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>B</mi></mrow><annotation encoding='application/x-tex'>B</annotation></semantics></math></p> </li> </ol> <p>means to declare it to be of the following iterated <a class='existingWikiWord' href='/nlab/show/diff/dependent+sum+type'>dependent pair</a>-<a class='existingWikiWord' href='/nlab/show/diff/type+telescope'>telescope</a> <a class='existingWikiWord' href='/nlab/show/diff/type'>type</a>:</p> <p><img src='/nlab/files/WellBehavedLensDataStructure-230130.jpg' width='740' /></p> <h3 id='GroupDataStructure'>Group data structure</h3> <p>The <a class='existingWikiWord' href='/nlab/show/diff/dependent+sum+type'>dependent pair</a>-<a class='existingWikiWord' href='/nlab/show/diff/type+telescope'>telescope</a> <a class='existingWikiWord' href='/nlab/show/diff/type'>type</a> declaration of <a class='existingWikiWord' href='/nlab/show/diff/group+object'>group structure</a>:</p> <p><img src='/nlab/files/GroupDataType-230130.jpg' width='710' /></p> <p>Further restriction to <a class='existingWikiWord' href='/nlab/show/diff/abelian+group'>abelian groups</a>:</p> <p><img src='/nlab/files/AbelianGroupData-230129.jpg' width='620' /></p> <p>Via the <a class='existingWikiWord' href='/nlab/show/diff/structure+identity+principle'>structure identity principle</a> (<a href='#StructureIdentityPrinciple'>above</a>), the <a class='existingWikiWord' href='/nlab/show/diff/identity+type'>identitifications</a>/<a class='existingWikiWord' href='/nlab/show/diff/equivalence+of+types'>equivalences</a> between such group data types are indeed bijective <a class='existingWikiWord' href='/nlab/show/diff/homomorphism'>group homomorphisms</a>, hence group-<a class='existingWikiWord' href='/nlab/show/diff/isomorphism'>isomorphisms</a>:</p> <p><img src='/nlab/files/GroupDataIsomorphism-230131.jpg' width='820' /></p> <p>The structure of <a class='existingWikiWord' href='/nlab/show/diff/subgroup'>subgroups</a> of a given group structure:</p> <p><img src='/nlab/files/SubgroupDataStructure-230201.jpg' width='900' /></p> <p>and their <a class='existingWikiWord' href='/nlab/show/diff/forgetful+functor'>underlying</a> abstract group structure:</p> <p><img src='/nlab/files/UnderlyingGroupOfSubgroupStructure-230201.jpg' width='900' /></p> <ins class='diffins'><h3 id='GroupActionStructure'>Group action structure</h3></ins><ins class='diffins'> </ins><ins class='diffins'><p>The <a class='existingWikiWord' href='/nlab/show/diff/dependent+sum+type'>dependent pair</a>-<a class='existingWikiWord' href='/nlab/show/diff/type+telescope'>telescope</a> <a class='existingWikiWord' href='/nlab/show/diff/type'>type</a> declaration of <a class='existingWikiWord' href='/nlab/show/diff/action'>group actions</a> on <a class='existingWikiWord' href='/nlab/show/diff/set'>sets</a> (<a class='existingWikiWord' href='/nlab/show/diff/G-set'>G-sets</a>):</p></ins><ins class='diffins'> </ins><ins class='diffins'><p><img src='/nlab/files/GroupActionDataStructure-230220.jpg' width='900' /></p></ins><ins class='diffins'> </ins><ins class='diffins'><p>Specialization to <a class='existingWikiWord' href='/nlab/show/diff/torsor'>torsors</a>:</p></ins><ins class='diffins'> </ins><ins class='diffins'><p><img src='/nlab/files/TorsorDataStructure-230220.jpg' width='900' /></p></ins><ins class='diffins'> </ins><h3 id='RingDataStructure'>Ring data structure</h3> <p>The <a class='existingWikiWord' href='/nlab/show/diff/dependent+sum+type'>dependent pair</a>-<a class='existingWikiWord' href='/nlab/show/diff/type+telescope'>telescope</a> <a class='existingWikiWord' href='/nlab/show/diff/type'>type</a> declaration of <a class='existingWikiWord' href='/nlab/show/diff/ring'>unital</a> <a class='existingWikiWord' href='/nlab/show/diff/ring+object'>ring structure</a>:</p> <p><img src='/nlab/files/RingDataStruture-230129.jpg' width='740' /></p> <p>For examples see at <em><a class='existingWikiWord' href='/nlab/show/diff/number'>numbers</a></em> – <em><a href='https://ncatlab.org/nlab/show/number#InDependentTypeTheory'>In dependent type theory</a></em>.</p> <h3 id='ModuleDataStructure'>Module data structure</h3> <p>Given a <a class='existingWikiWord' href='/nlab/show/diff/ring'>unital</a> <a class='existingWikiWord' href='/nlab/show/diff/ring'>ring</a> type <math class='maruku-mathml' display='inline' id='mathml_0b8e6d65960e5d2f2edb3977235800ac8dd17851_33' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>R</mi><mo lspace='verythinmathspace'>:</mo><mi>Ring</mi></mrow><annotation encoding='application/x-tex'>R \colon Ring</annotation></semantics></math> (as <a href='#RingDataStructure'>above</a>), the type of <math class='maruku-mathml' display='inline' id='mathml_0b8e6d65960e5d2f2edb3977235800ac8dd17851_34' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>R</mi></mrow><annotation encoding='application/x-tex'>R</annotation></semantics></math>-<a class='existingWikiWord' href='/nlab/show/diff/module+object'>module objects</a> is the following <a class='existingWikiWord' href='/nlab/show/diff/dependent+sum+type'>dependent pair</a>-<a class='existingWikiWord' href='/nlab/show/diff/type+telescope'>telescope</a>:</p> <p><img src='/nlab/files/ModuleDataStructure-230129.jpg' width='740' /></p> <h2 id='HigherStructuresInHoTT'>Higher structures in homotopy type theory</h2> <p>The <a href='#InDependentTypeTheory'>above</a> examples of structures formulated in dependent type theory all had data <a class='existingWikiWord' href='/nlab/show/diff/h-set'>sets</a> as their base, which is the classical situation. But in <a class='existingWikiWord' href='/nlab/show/diff/dependent+type+theory'>dependent type theory</a> with untruncated <a class='existingWikiWord' href='/nlab/show/diff/identity+type'>identification types</a>, hence in <a class='existingWikiWord' href='/nlab/show/diff/homotopy+type+theory'>homotopy type theory</a>, we may simply drop this constraint and consider structures whose base is any higher <a class='existingWikiWord' href='/nlab/show/diff/homotopy+type'>homotopy type</a>: This yields the notion of <em><a class='existingWikiWord' href='/nlab/show/diff/higher+structure'>higher structures</a></em>.</p> <h3 id='delooping'>Delooping</h3> <p>Given a set-based <a class='existingWikiWord' href='/nlab/show/diff/group+object'>group structure</a> (as <a href='#GroupDataStructure'>above</a>), <a class='existingWikiWord' href='/nlab/show/diff/delooping'>delooping</a> structure is</p> <p>(…)</p> <h3 id='higher_delooping'>Higher delooping</h3> <p>More generally, one may consider delooping of <a class='existingWikiWord' href='/nlab/show/diff/n-group'>$n$-groups</a>, but this is a lot of (higher) structure if spelled out in detail. Yet more generally and again more readily axiomatized there is the notion of deloopings of any <a class='existingWikiWord' href='/nlab/show/diff/pointed+object'> pointed</a> types (cf. <a href='delooping#Wärn23'>Wärn (2023, §2)</a>, <a href='delooping#BCFR23'>BCFR23</a>), which we may write as follows:</p> <p><img src='/nlab/files/PointedHigherDeloopingStructure-230131.jpg' width='700' /></p> <p>Similarly there is <a class='existingWikiWord' href='/nlab/show/diff/iterated+loop+space'>iterated delooping structure</a>:</p> <p><img src='/nlab/files/PointedIteratedDeloopingStructure-230131.jpg' width='740' /></p> <h2 id='related_entries'>Related entries</h2> <ul> <li> <p>Evident as the notion of <em>mathematical structure</em> may seem these days, it was at least not made explicit until the middle of the 20th century. Then it was the influence of the <em><a class='existingWikiWord' href='/nlab/show/diff/Bourbaki'>Bourbaki</a></em>-project (see there for more) and then later the development of <a class='existingWikiWord' href='/nlab/show/diff/category+theory'>category theory</a> which made the notion explicit and finally led to the above formalization.</p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/function'>functions</a> that preserves extra structure are called <em><a class='existingWikiWord' href='/nlab/show/diff/homomorphism'>homomorphisms</a></em>; <a class='existingWikiWord' href='/nlab/show/diff/relation'>relations</a> that preserve extra structure are called <a class='existingWikiWord' href='/nlab/show/diff/logical+relation'>logical relations</a>_</p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/Birkhoff%27s+HSP+theorem'>Birkhoff's HSP theorem</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/structuralism'>structuralism</a>, <a class='existingWikiWord' href='/nlab/show/diff/structure+identity+principle'>structure identity principle</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/exceptional+structure'>exceptional structure</a></p> </li> </ul> <h2 id='references'>References</h2> <h3 id='general'>General</h3> <p>On the history of the notion of “mathematical structure” with some focus on what <a class='existingWikiWord' href='/nlab/show/diff/Bourbaki'>Bourbaki</a> did and did not contribute to the subject:</p> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/Leo+Corry'>Leo Corry</a>, <em>Mathematical Structures from Hilbert to Bourbaki: The Evolution of an Image of Mathematics</em>, in: <em>Changing Images of Mathematics in History. From the French Revolution to the new Millenium</em> Harwood Academic Publishers (2001) 167-186 [[ISBN:9780415868273](https://www.routledge.com/Changing-Images-in-Mathematics-From-the-French-Revolution-to-the-New-Millennium/Bottazini-Dalmedico/p/book/9780415868273), <a href='https://www.leocorry.com/_files/ugd/e6fef7_15c7077b08ec4f249fb40eb961256ced.pdf'>pdf</a>]</p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/Leo+Corry'>Leo Corry</a>, <em>Modern Algebra and the Rise of Mathematical Structures</em>, Springer (2004) [[doi:10.1007/978-3-0348-7917-0](https://doi.org/10.1007/978-3-0348-7917-0)]</p> </li> </ul> <p>See also</p> <ul> <li> <p>Wikipedia, <em><a href='https://en.wikipedia.org/wiki/Mathematical_structure'>Mathematical structure</a></em></p> </li> <li> <p>Wikipedia, <em><a href='https://en.wikipedia.org/wiki/Structure_(mathematical_logic)'>Structure_(mathematical_logic)</a></em></p> </li> </ul> <p>Early proposal to grasp the notion of mathematical structures via <a class='existingWikiWord' href='/nlab/show/diff/category+theory'>category theory</a> (specifically via <a class='existingWikiWord' href='/nlab/show/diff/forgetful+functor'>forgetful functors</a> between <a class='existingWikiWord' href='/nlab/show/diff/groupoid'>groupoids</a>):</p> <ul> <li id='Ehresmann57'> <p><a class='existingWikiWord' href='/nlab/show/diff/Charles+Ehresmann'>Charles Ehresmann</a>, <em>Gattungen in Lokalen Strukturen</em>, Jahresbericht der Deutschen Mathematiker-Vereinigung <strong>60</strong> (1958) 49-77 [[dml:146434](https://eudml.org/doc/146434)]</p> </li> <li id='Ehresmann65'> <p><a class='existingWikiWord' href='/nlab/show/diff/Charles+Ehresmann'>Charles Ehresmann</a>, <em>Catégories et Structures</em>, Séminaire Ehresmann. Topologie et géométrie différentielle <strong>6</strong> (1964) 1-31 [[numdam:SE_1964__6__A8_0](http://www.numdam.org/item?id=SE_1964__6__A8_0), <a href='https://eudml.org/doc/112200'>dml:112200</a>]</p> </li> </ul> <p>For modern accounts on mathematical structures via <a class='existingWikiWord' href='/nlab/show/diff/categorical+algebra'>categorical algebra</a> see also at <em><a class='existingWikiWord' href='/nlab/show/diff/algebraic+theory'>algebraic theory</a></em>, <em><a class='existingWikiWord' href='/nlab/show/diff/monad'>monad</a></em>, <em><a class='existingWikiWord' href='/nlab/show/diff/sketch'>sketch</a></em>.</p> <h3 id='ReferencesInDependentTypeTheory'>In dependent type theory</h3> <p>Discussion of mathematical structures via <a class='existingWikiWord' href='/nlab/show/diff/dependent+type+theory'>dependent type theory</a>:</p> <p>the general idea of representing mathematical structures as <a class='existingWikiWord' href='/nlab/show/diff/type+telescope'>type telescopes</a>:</p> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/Jeffery+Zucker'>Jeffery Zucker</a>, <em>Formalization of Classical Mathematics in Automath</em>, Colloques Internationaux du Centre National de la Recherche Scientifique <strong>249</strong> (1975) 135-145 [[web](https://www.win.tue.nl/automath/archive/webversion/aut042/aut042.html), <a href='https://www.win.tue.nl/automath/archive/pdf/aut042.pdf'>pdf</a>]</p> <p>also in: Studies in Logic and the Foundations of Mathematics <strong>133</strong> (1994) 127-139 []</p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/Nicolaas+de+Bruijn'>Nicolaas de Bruijn</a>, <em>Telescopic mappings in typed lambda calculus</em>, Information and Computation <strong>91</strong> 2 (1991) 189-204 []</p> </li> </ul> <p>and with emphasis of the notion of <a class='existingWikiWord' href='/nlab/show/diff/isomorphism'>isomorphism</a> between such structures:</p> <ul> <li><a class='existingWikiWord' href='/nlab/show/diff/David+McAllester'>David McAllester</a>, <em>Dependent Type Theory as Related to the Bourbaki Notions of Structure and Isomorphism</em> [[arXiv:2104.08958](https://arxiv.org/abs/2104.08958)]</li> </ul> <p>in <a class='existingWikiWord' href='/nlab/show/diff/Coq'>Coq</a>:</p> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/Herman+Geuvers'>Herman Geuvers</a>, <a class='existingWikiWord' href='/nlab/show/diff/Randy+Pollack'>Randy Pollack</a>, <a class='existingWikiWord' href='/nlab/show/diff/Freek+Wiedijk'>Freek Wiedijk</a>, <a class='existingWikiWord' href='/nlab/show/diff/Jan+Zwanenburg'>Jan Zwanenburg</a>, <em>A Constructive Algebraic Hierarchy in Coq</em>, Journal of Symbolic Computation <strong>34</strong> 4 (2002) 271-286 [[doi:10.1006/jsco.2002.0552](https://doi.org/10.1006/jsco.2002.0552), <a href='http://www.cs.ru.nl/~herman/PUBS/JSC2002-GeuversPollackWiedijkZwanenburg-alghier1.pdf'>pdf</a>]</p> </li> <li> <p>Claudio Sacerdoti Coen, Enrico Tassi, <em>Working with Mathematical Structures in Type Theory</em>, in: <em>Types for Proofs and Programs. TYPES 2007</em>, Lecture Notes in Computer Science <strong>4941</strong> Springer (2008) [[doi:10.1007/978-3-540-68103-8_11](https://doi.org/10.1007/978-3-540-68103-8_11), <a href='https://www.cs.unibo.it/~sacerdot/PAPERS/types07.pdf'>pdf</a>]</p> </li> <li> <p>François Garillot, Georges Gonthier, Assia Mahboubi & Laurence Rideau, <em>Packaging Mathematical Structures</em>, in: <em>Theorem Proving in Higher Order Logics. TPHOLs 2009</em>, Lecture Notes in Computer Science <strong>5674</strong>, Springer (2009) [[doi:10.1007/978-3-642-03359-9_23](https://doi.org/10.1007/978-3-642-03359-9_23)]</p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/Bas+Spitters'>Bas Spitters</a>, Eelis van der Wegen <em>Type classes for mathematics in type theory</em>, Mathematical Structures in Computer Science <strong>21</strong> 4 “Interactive Theorem Proving and the Formalisation of Mathematics” (2011) 795-825 [[doi:10.1017/S0960129511000119](https://doi.org/10.1017/S0960129511000119), <a href='https://arxiv.org/abs/1102.1323'>arXiv:1102.1323</a>]</p> <blockquote> <p>(via <a class='existingWikiWord' href='/ufias2012/published/Type+classes' title='ufias2012'>Type classes</a>)</p> </blockquote> </li> <li> <p>Kazuhiko Sakaguchi, <em>Validating Mathematical Structures</em>, in <em>Automated Reasoning. IJCAR 2020</em>, Lecture Notes in Computer Science <strong>12167</strong>, Springer (2020) [[doi:10.1007/978-3-030-51054-1_8](https://doi.org/10.1007/978-3-030-51054-1_8)]</p> </li> </ul> <p>in <a class='existingWikiWord' href='/nlab/show/diff/Lean'>Lean</a>:</p> <ul> <li><a href='https://leanprover-community.github.io/mathlib-overview.html'>The mathlib Community</a>, §4 in: <em>The Lean mathematical library</em>, in <em>CPP 2020: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs</em> (2020) 367–381 [[arXiv:1910.09336](https://arxiv.org/abs/1910.09336), <a href='https://doi.org/10.1145/3372885.3373824'>doi:10.1145/3372885.3373824</a>]</li> </ul> <p>Discussion of classes of mathematical structures in <a class='existingWikiWord' href='/nlab/show/diff/univalence+axiom'>univalent</a> <a class='existingWikiWord' href='/nlab/show/diff/homotopy+type+theory'>homotopy type theory</a> (<a class='existingWikiWord' href='/nlab/show/diff/univalent+foundations+for+mathematics'>univalent foundations of mathematics</a>) which satisfy a <a class='existingWikiWord' href='/nlab/show/diff/structure+identity+principle'>structure identity principle</a>:</p> <ul> <li id='CoquandDanielsson13'> <p><a class='existingWikiWord' href='/nlab/show/diff/Thierry+Coquand'>Thierry Coquand</a>, <a class='existingWikiWord' href='/nlab/show/diff/Nils+A.+Danielsson'>Nils Anders Danielsson</a>, <em>Isomorphism is equality</em>, Indagationes Mathematicae <strong>24</strong> 4 (2013) 1105-1120 [[doi:10.1016/j.indag.2013.09.002](https://doi.org/10.1016/j.indag.2013.09.002)]</p> </li> <li id='UFP13'> <p><a class='existingWikiWord' href='/nlab/show/diff/UF-IAS-2012'>Univalent Foundations Project</a>, §9.8 but also §2 of: <em><a class='existingWikiWord' href='/nlab/show/diff/Homotopy+Type+Theory+--+Univalent+Foundations+of+Mathematics'>Homotopy Type Theory -- Univalent Foundations of Mathematics</a></em> (2013) [[web](http://homotopytypetheory.org/book/), <a href='http://hottheory.files.wordpress.com/2013/03/hott-online-323-g28e4374.pdf'>pdf</a>]</p> </li> <li id='Escardó19'> <p><a class='existingWikiWord' href='/nlab/show/diff/Mart%C3%ADn+Escard%C3%B3'>Martín Escardó</a>, <em><a href='https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html#sns'>A structure identity principle for a standard notion of structure</a></em>, §3.33.1 in: <em>Introduction to Univalent Foundations of Mathematics with Agda</em> [[arXiv:1911.00580](https://arxiv.org/abs/1911.00580), <a href='https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html'>webpage</a>]</p> <blockquote> <p>(formalized in the <a class='existingWikiWord' href='/nlab/show/diff/Agda'>Agda</a> <a class='existingWikiWord' href='/nlab/show/diff/proof+assistant'>proof assistant</a>)</p> </blockquote> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/diff/Benedikt+Ahrens'>Benedikt Ahrens</a>, <a class='existingWikiWord' href='/nlab/show/diff/Paige+Randall+North'>Paige Randall North</a>, <a class='existingWikiWord' href='/nlab/show/diff/Mike+Shulman'>Michael Shulman</a>, <a class='existingWikiWord' href='/nlab/show/diff/Dimitris+Tsementzis'>Dimitris Tsementzis</a>, <em>A Higher Structure Identity Principle</em>, LICS ‘20 (2020) 53–66 [[arXiv:2004.06572](https://arxiv.org/abs/2004.06572), <a href='https://doi.org/10.1145/3373718.3394755'>doi:10.1145/3373718.3394755</a>]</p> </li> </ul> <p>Discussion in the context of the <a class='existingWikiWord' href='/nlab/show/diff/philosophy'>philosophy</a> of <a class='existingWikiWord' href='/nlab/show/diff/structuralism'>structuralism</a>:</p> <ul> <li><a class='existingWikiWord' href='/nlab/show/diff/Dimitris+Tsementzis'>Dimitris Tsementzis</a>, §5.1 in: <em>Univalent foundations as structuralist foundations</em>, Synthese <strong>194</strong> 9 (2017) 3583–3617 [[jstor:26748765](https://www.jstor.org/stable/26748765), <a href='https://doi.org/10.1007/s11229-016-1109-x'>doi:10.1007/s11229-016-1109-x</a>, <a href='https://core.ac.uk/download/pdf/157866891.pdf'>pdf</a>]</li> </ul> <p>Expressions towards the notion that, thereby the notions of <em>mathematical structures</em> are <em>data structures</em> may be understood to coincide (just along the lines of <em><a class='existingWikiWord' href='/nlab/show/diff/type'>types</a></em> being <em><a class='existingWikiWord' href='/nlab/show/diff/data+type'>data types</a></em>):</p> <ul> <li><a class='existingWikiWord' href='/nlab/show/diff/Thomas+Kehrenberg'>Thomas Kehrenberg</a>, <em>Basic building blocks of dependent type theory</em> (Dec. 2022) [[post on LessWrong](https://www.lesswrong.com/posts/ccbsYSpTcTqXwukH8/basic-building-blocks-of-dependent-type-theory), <a href='https://tm.kehrenberg.net/a/type-theory1/'>post on personal blog</a>]</li> </ul> <blockquote> <p>“An example of a use case for non-binary sum types is the definition of mathematical “data structures” like a ring or a group. These data structures are usually defined as…”</p> </blockquote> <p> </p> <p> </p> </div> <div class="revisedby"> <p> Last revised on February 20, 2023 at 04:39:29. See the <a href="/nlab/history/structure" 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/structure" accesskey="E" class="navlink" id="edit" rel="nofollow">Edit</a><a href="https://nforum.ncatlab.org/discussion/4103/#Item_33">Discuss</a><span class="backintime"><a href="/nlab/revision/diff/structure/52" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/structure" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Hide changes</a><a href="/nlab/history/structure" accesskey="S" class="navlink" id="history" rel="nofollow">History (52 revisions)</a> <a href="/nlab/show/structure/cite" style="color: black">Cite</a> <a href="/nlab/print/structure" accesskey="p" id="view_print" rel="nofollow">Print</a> <a href="/nlab/source/structure" id="view_source" rel="nofollow">Source</a> </div> </div>  </div>  </body> </html>