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> set 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> set </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/15973/#Item_1" 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>Sets</title></head> <body> <div class="rightHandSide"> <div class="toc clickDown" tabindex="0"> <h3 id="context">Context</h3> <h4 id="foundations">Foundations</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/foundations">foundations</a></strong></p> <h2 id="the_basis_of_it_all">The basis of it all</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/mathematical+logic">mathematical logic</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/deduction+system">deduction system</a>, <a class="existingWikiWord" href="/nlab/show/natural+deduction">natural deduction</a>, <a class="existingWikiWord" href="/nlab/show/sequent+calculus">sequent calculus</a>, <a class="existingWikiWord" href="/nlab/show/lambda-calculus">lambda-calculus</a>, <a class="existingWikiWord" href="/nlab/show/judgment">judgment</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a>, <a class="existingWikiWord" href="/nlab/show/simple+type+theory">simple type theory</a>, <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/collection">collection</a>, <a class="existingWikiWord" href="/nlab/show/object">object</a>, <a class="existingWikiWord" href="/nlab/show/type">type</a>, <a class="existingWikiWord" href="/nlab/show/term">term</a>, <a class="existingWikiWord" href="/nlab/show/set">set</a>, <a class="existingWikiWord" href="/nlab/show/element">element</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/equality">equality</a>, <a class="existingWikiWord" href="/nlab/show/judgmental+equality">judgmental equality</a>, <a class="existingWikiWord" href="/nlab/show/typal+equality">typal equality</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/universe">universe</a>, <a class="existingWikiWord" href="/nlab/show/size+issues">size issues</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/higher-order+logic">higher-order logic</a></p> </li> </ul> <h2 id="set_theory"> Set theory</h2> <div> <p><strong><a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a></strong></p> <ul> <li>fundamentals of set theory <ul> <li><a class="existingWikiWord" href="/nlab/show/propositional+logic">propositional logic</a></li> <li><a class="existingWikiWord" href="/nlab/show/first-order+logic">first-order logic</a></li> <li><a class="existingWikiWord" href="/nlab/show/typed+predicate+logic">typed predicate logic</a></li> <li><a class="existingWikiWord" href="/nlab/show/membership+relation">membership relation</a></li> <li><a class="existingWikiWord" href="/nlab/show/propositional+equality">propositional equality</a></li> <li><a class="existingWikiWord" href="/nlab/show/set">set</a>, <a class="existingWikiWord" href="/nlab/show/element">element</a>, <a class="existingWikiWord" href="/nlab/show/function">function</a>, <a class="existingWikiWord" href="/nlab/show/relation">relation</a></li> <li><a class="existingWikiWord" href="/nlab/show/universe">universe</a>, <a class="existingWikiWord" href="/nlab/show/small+set">small set</a>, <a class="existingWikiWord" href="/nlab/show/large+set">large set</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/material+set+theory">material set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/membership+relation">membership relation</a>, <a class="existingWikiWord" href="/nlab/show/propositional+equality">propositional equality</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+extensionality">axiom of extensionality</a></li> <li><a class="existingWikiWord" href="/nlab/show/pairing+structure">pairing structure</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+pairing">axiom of pairing</a></li> <li><a class="existingWikiWord" href="/nlab/show/union+structure">union structure</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+union">axiom of union</a></li> <li><a class="existingWikiWord" href="/nlab/show/powerset+structure">powerset structure</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+power+sets">axiom of power sets</a></li> <li><a class="existingWikiWord" href="/nlab/show/natural+numbers+structure">natural numbers structure</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+infinity">axiom of infinity</a></li> </ul> </li> <li>presentations of set theory <ul> <li><a class="existingWikiWord" href="/nlab/show/first-order+set+theory">first-order set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/unsorted+set+theory">unsorted set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/simply+sorted+set+theory">simply sorted set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/one-sorted+set+theory">one-sorted set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/two-sorted+set+theory">two-sorted set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/three-sorted+set+theory">three-sorted set theory</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/dependently+sorted+set+theory">dependently sorted set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/structurally+presented+set+theory">structurally presented set theory</a></li> </ul> </li> <li>structuralism in set theory <ul> <li><a class="existingWikiWord" href="/nlab/show/material+set+theory">material set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/ZFC">ZFC</a></li> <li><a class="existingWikiWord" href="/nlab/show/ZFA">ZFA</a></li> <li><a class="existingWikiWord" href="/nlab/show/Mostowski+set+theory">Mostowski set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/New+Foundations">New Foundations</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/structural+set+theory">structural set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/categorical+set+theory">categorical set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/ETCS">ETCS</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/fully+formal+ETCS">fully formal ETCS</a></li> <li><a class="existingWikiWord" href="/nlab/show/ETCS+with+elements">ETCS with elements</a></li> <li><a class="existingWikiWord" href="/nlab/show/Trimble+on+ETCS+I">Trimble on ETCS I</a></li> <li><a class="existingWikiWord" href="/nlab/show/Trimble+on+ETCS+II">Trimble on ETCS II</a></li> <li><a class="existingWikiWord" href="/nlab/show/Trimble+on+ETCS+III">Trimble on ETCS III</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/structural+ZFC">structural ZFC</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/allegorical+set+theory">allegorical set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/SEAR">SEAR</a></li> </ul> </li> </ul> </li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/class-set+theory">class-set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/class">class</a>, <a class="existingWikiWord" href="/nlab/show/proper+class">proper class</a></li> <li><a class="existingWikiWord" href="/nlab/show/universal+class">universal class</a>, <a class="existingWikiWord" href="/nlab/show/universe">universe</a></li> <li><a class="existingWikiWord" href="/nlab/show/category+of+classes">category of classes</a></li> <li><a class="existingWikiWord" href="/nlab/show/category+with+class+structure">category with class structure</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/constructive+set+theory">constructive set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/algebraic+set+theory">algebraic set theory</a></li> </ul> </div> <h2 id="foundational_axioms">Foundational axioms</h2> <div> <p><strong><a class="existingWikiWord" href="/nlab/show/foundational+axiom">foundational</a> <a class="existingWikiWord" href="/nlab/show/axioms">axioms</a></strong></p> <ul> <li> <p>basic constructions:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+cartesian+products">axiom of cartesian products</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+disjoint+unions">axiom of disjoint unions</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+the+empty+set">axiom of the empty set</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+fullness">axiom of fullness</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+function+sets">axiom of function sets</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+power+sets">axiom of power sets</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+quotient+sets">axiom of quotient sets</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/material+set+theory">material axioms</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+extensionality">axiom of extensionality</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+foundation">axiom of foundation</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+anti-foundation">axiom of anti-foundation</a></li> <li><a class="existingWikiWord" href="/nlab/show/Mostowski%27s+axiom">Mostowski's axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+pairing">axiom of pairing</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+transitive+closure">axiom of transitive closure</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+union">axiom of union</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/structural+set+theory">structural axioms</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+materialization">axiom of materialization</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/type+theory">type theoretic axioms</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axioms+of+set+truncation">axioms of set truncation</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/uniqueness+of+identity+proofs">uniqueness of identity proofs</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+K">axiom K</a></li> <li><a class="existingWikiWord" href="/nlab/show/boundary+separation">boundary separation</a></li> <li><a class="existingWikiWord" href="/nlab/show/equality+reflection">equality reflection</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+circle+type+localization">axiom of circle type localization</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theoretic axioms</a>: <ul> <li><a class="existingWikiWord" href="/nlab/show/univalence+axiom">univalence axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/Whitehead%27s+principle">Whitehead's principle</a></li> </ul> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/axioms+of+choice">axioms of choice</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+countable+choice">axiom of countable choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+dependent+choice">axiom of dependent choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+excluded+middle">axiom of excluded middle</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+existence">axiom of existence</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+multiple+choice">axiom of multiple choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/Markov%27s+axiom">Markov's axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/presentation+axiom">presentation axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/small+cardinality+selection+axiom">small cardinality selection axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+small+violations+of+choice">axiom of small violations of choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+weakly+initial+sets+of+covers">axiom of weakly initial sets of covers</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/large+cardinal+axioms">large cardinal axioms</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+infinity">axiom of infinity</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+universes">axiom of universes</a></li> <li><a class="existingWikiWord" href="/nlab/show/regular+extension+axiom">regular extension axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/inaccessible+cardinal">inaccessible cardinal</a></li> <li><a class="existingWikiWord" href="/nlab/show/measurable+cardinal">measurable cardinal</a></li> <li><a class="existingWikiWord" href="/nlab/show/elementary+embedding">elementary embedding</a></li> <li><a class="existingWikiWord" href="/nlab/show/supercompact+cardinal">supercompact cardinal</a></li> <li><a class="existingWikiWord" href="/nlab/show/Vop%C4%9Bnka%27s+principle">Vopěnka's principle</a></li> </ul> </li> <li> <p>strong axioms</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+separation">axiom of separation</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+replacement">axiom of replacement</a></li> </ul> </li> <li> <p>further</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/reflection+principle">reflection principle</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/axiom+of+tight+apartness">axiom of tight apartness</a></p> </li> </ul> </div> <h2 id="removing_axioms">Removing axioms</h2> <ul> <li><a class="existingWikiWord" href="/nlab/show/constructive+mathematics">constructive mathematics</a></li> <li><a class="existingWikiWord" href="/nlab/show/predicative+mathematics">predicative mathematics</a></li> </ul> <div> <p> <a href="/nlab/edit/foundations+-+contents">Edit this sidebar</a> </p> </div></div></div> <h4 id="category_theory">Category theory</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a></strong></p> <h2 id="sidebar_concepts">Concepts</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/category">category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/functor">functor</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/natural+transformation">natural transformation</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Cat">Cat</a></p> </li> </ul> <h2 id="sidebar_universal_constructions">Universal constructions</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/universal+construction">universal construction</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/representable+functor">representable functor</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/adjoint+functor">adjoint functor</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/limit">limit</a>/<a class="existingWikiWord" href="/nlab/show/colimit">colimit</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/weighted+limit">weighted limit</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/end">end</a>/<a class="existingWikiWord" href="/nlab/show/coend">coend</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Kan+extension">Kan extension</a></p> </li> </ul> </li> </ul> <h2 id="sidebar_theorems">Theorems</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Yoneda+lemma">Yoneda lemma</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Isbell+duality">Isbell duality</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Grothendieck+construction">Grothendieck construction</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/adjoint+functor+theorem">adjoint functor theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/monadicity+theorem">monadicity theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/adjoint+lifting+theorem">adjoint lifting theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Tannaka+duality">Tannaka duality</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Gabriel-Ulmer+duality">Gabriel-Ulmer duality</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/small+object+argument">small object argument</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Freyd-Mitchell+embedding+theorem">Freyd-Mitchell embedding theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/relation+between+type+theory+and+category+theory">relation between type theory and category theory</a></p> </li> </ul> <h2 id="sidebar_extensions">Extensions</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/sheaf+and+topos+theory">sheaf and topos theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/enriched+category+theory">enriched category theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/higher+category+theory">higher category theory</a></p> </li> </ul> <h2 id="sidebar_applications">Applications</h2> <ul> <li><a class="existingWikiWord" href="/nlab/show/applications+of+%28higher%29+category+theory">applications of (higher) category theory</a></li> </ul> <div> <p> <a href="/nlab/edit/category+theory+-+contents">Edit this sidebar</a> </p> </div></div></div> <h4 id="mathematics">Mathematics</h4> <div class="hide"><div> <ul> <li> <p><strong><a class="existingWikiWord" href="/nlab/show/mathematics">mathematics</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/math+resources">math resources</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/history+of+mathematics">history of mathematics</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/foundations">Structural Foundations</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/logic">logic</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/internal+language">internal language</a></li> <li><a class="existingWikiWord" href="/nlab/show/classical+mathematics">classical mathematics</a></li> <li><a class="existingWikiWord" href="/nlab/show/constructive+mathematics">constructive mathematics</a></li> <li><a class="existingWikiWord" href="/nlab/show/predicative+mathematics">predicative mathematics</a></li> <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/set+theory">set theory</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/structural+set+theory">structural set theory</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Categories+and+Sheaves">Categories and Sheaves</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/topos+theory">topos theory</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Sheaves+in+Geometry+and+Logic">Sheaves in Geometry and Logic</a></li> </ul> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/higher+category+theory">higher category theory</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/higher+topos+theory">higher topos theory</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Higher+Topos+Theory">(∞,1)-topos theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/models+for+%E2%88%9E-stack+%28%E2%88%9E%2C1%29-toposes">models for ∞-stack (∞,1)-toposes</a></li> <li><a class="existingWikiWord" href="/nlab/show/cohomology">cohomology</a></li> </ul> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/homotopy+theory">homotopy theory</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/stable+homotopy+theory">stable homotopy theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/rational+homotopy+theory">rational homotopy theory</a></li> </ul> </li> </ul> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/topology+and+geometry">Topology and Geometry</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/geometry">geometry</a> (general list), <a class="existingWikiWord" href="/nlab/show/topology">topology</a> (general list)</li> <li><a class="existingWikiWord" href="/nlab/show/general+topology">general topology</a></li> <li><a class="existingWikiWord" href="/nlab/show/differential+topology">differential topology</a></li> <li><a class="existingWikiWord" href="/nlab/show/differential+geometry">differential geometry</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/synthetic+differential+geometry">synthetic differential geometry</a></li> <li><a class="existingWikiWord" href="/nlab/show/symplectic+geometry">symplectic geometry</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/algebraic+geometry">algebraic geometry</a></li> <li><a class="existingWikiWord" href="/nlab/show/noncommutative+algebraic+geometry">noncommutative algebraic geometry</a></li> <li><a class="existingWikiWord" href="/nlab/show/noncommutative+geometry">noncommutative geometry</a> (general flavour)</li> <li><a class="existingWikiWord" href="/nlab/show/higher+geometry">higher geometry</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/algebra">Algebra</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/universal+algebra">universal algebra</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/higher+algebra">higher algebra</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/homological+algebra">homological algebra</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/group+theory">group theory</a>, <a class="existingWikiWord" href="/nlab/show/ring+theory">ring theory</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/representation+theory">representation theory</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/algebraic+approaches+to+differential+calculus">algebraic approaches to differential calculus</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/counterexamples+in+algebra">counterexamples in algebra</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/analysis">analysis</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/nonstandard+analysis">nonstandard analysis</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/functional+analysis">functional analysis</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/operator+algebras">operator algebras</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Fourier+transform">Fourier transform</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Lie+theory">Lie theory</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/infinity-Lie+theory+-+contents">higher Lie theory</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/probability+theory">probability theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/discrete+mathematics">discrete mathematics</a></p> </li> </ul> </div></div> </div> </div> <h1 id="sets">Sets</h1> <div class='maruku_toc'> <ul> <li><a href='#what_should_a_set_be'>What should a set be?</a></li> <li><a href='#what_is_a_set'>What is a set?</a></li> <ul> <li><a href='#in_category_theory'>In category theory</a></li> <li><a href='#InHoTT'>In homotopy type theory</a></li> </ul> <li><a href='#related_concepts'>Related concepts</a></li> <li><a href='#references'>References</a></li> <ul> <li><a href='#general'>General</a></li> <li><a href='#history'>History</a></li> </ul> </ul> </div> <h2 id="what_should_a_set_be">What should a set be?</h2> <p>The concept of <em>set</em> appears in several different guises in <a class="existingWikiWord" href="/nlab/show/mathematics">mathematics</a>, and particularly in <a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a>.</p> <p>It is common to use <a class="existingWikiWord" href="/nlab/show/foundations+of+mathematics">foundations of mathematics</a> in which ‘set’ is an undefined term; this is <a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a> as a foundation. In a <a class="existingWikiWord" href="/nlab/show/pure+set">pure</a> <a class="existingWikiWord" href="/nlab/show/material+set+theory">material set theory</a> like <a class="existingWikiWord" href="/nlab/show/ZFC">ZFC</a>, every object is a set. Even in a <a class="existingWikiWord" href="/nlab/show/structural+set+theory">structural approach</a> such as <a class="existingWikiWord" href="/nlab/show/ETCS">ETCS</a>, it is common for every object to be a <a class="existingWikiWord" href="/nlab/show/structured+set">structured set</a> in some way or another.</p> <p>Even if sets are not at the bottom of your foundations, still they are probably close. For instance, in <a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a> sometimes sets are defined as <a class="existingWikiWord" href="/nlab/show/predicates">predicates</a> on <a class="existingWikiWord" href="/nlab/show/types">types</a>, or as <a class="existingWikiWord" href="/nlab/show/setoids">setoids</a>. In <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a>, sets are defined as <a class="existingWikiWord" href="/nlab/show/truncated+object">0-truncated</a> homotopy types; see below.</p> <p>Material set theory conflates two notions of sets, which were elegantly (but not first) described by <a class="existingWikiWord" href="/nlab/show/Mathieu+Dupont">Mathieu Dupont</a> in <a href="http://math.breckes.org/2009/03/the-two-meanings-of-the-word-%E2%80%9Cset%E2%80%9D-in-mathematics/">a blog post</a> as ‘set¹’ and ‘set²’, which we will here call ‘abstract set’ and ‘concrete set’. In the latter case (set²), we have some fixed <a class="existingWikiWord" href="/nlab/show/universe+of+discourse">universe of discourse</a> (say, consisting of all real numbers), and a <strong>concrete set</strong> is a set of elements of this universe (so a set of real numbers, such as <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">{</mo><mn>5</mn><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\{5\}</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">{</mo><mi>x</mi><mo stretchy="false">|</mo><mi>x</mi><mo>></mo><mn>2</mn><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\{ x | x \gt 2 \}</annotation></semantics></math>, or <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>∅</mi></mrow><annotation encoding="application/x-tex">\empty</annotation></semantics></math>). In the former case (set¹), an <strong>abstract set</strong> is a purely abstract concept, an unstructured (except perhaps for the <a class="existingWikiWord" href="/nlab/show/equality+relation">equality relation</a>) collection of unlabelled elements. Arguably (this argument goes back at least to <a class="existingWikiWord" href="/nlab/show/Bill+Lawvere">Lawvere</a>), <a class="existingWikiWord" href="/nlab/show/Georg+Cantor">Cantor</a>'s original concept of <a class="existingWikiWord" href="/nlab/show/cardinal+number">cardinal number</a> (Kardinalzahl) was the abstraction from a concrete set to its underlying abstract set.</p> <p>Here we adopt a structural approach, in which a <strong>set</strong> is an abstract set, a (mostly) unstructured <a class="existingWikiWord" href="/nlab/show/collection">collection</a>. For concrete sets, see <a class="existingWikiWord" href="/nlab/show/subset">subset</a>; if the fixed universe of discourse is an abstract set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math>, then a concrete set will be a subset of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math>. In material set theory (as usually conceived), the fixed universe of discourse is an abstract set (or <a class="existingWikiWord" href="/nlab/show/proper+class">proper class</a>) <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>V</mi></mrow><annotation encoding="application/x-tex">V</annotation></semantics></math>, an abstract set (internal to the theory) is an element of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>V</mi></mrow><annotation encoding="application/x-tex">V</annotation></semantics></math>, and a concrete set is a sufficiently <a class="existingWikiWord" href="/nlab/show/small+set">small</a> subset of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>V</mi></mrow><annotation encoding="application/x-tex">V</annotation></semantics></math>; the concepts may be identified because <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>V</mi></mrow><annotation encoding="application/x-tex">V</annotation></semantics></math> comes with an <a class="existingWikiWord" href="/nlab/show/bijection">isomorphism</a> to its class of small subsets.</p> <h2 id="what_is_a_set">What is a set?</h2> <p>We still need to clarify exactly what sort of collection a set is. Although most foundations leave this unspecified, we may (perhaps circularly, and perhaps controversially) define it in various ways, as follows:</p> <h3 id="in_category_theory">In category theory</h3> <div class="un_defn" id="AsCategory"> <h6 id="definition">Definition</h6> <p>A <strong>set</strong> is a <a class="existingWikiWord" href="/nlab/show/category">category</a> (or instead 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> or even 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>) that is <a class="existingWikiWord" href="/nlab/show/small+category">small</a>, <a class="existingWikiWord" href="/nlab/show/discrete+category">discrete</a>, and <a class="existingWikiWord" href="/nlab/show/skeletal+category">skeletal</a>. (This definition needs explanation since it seems to be recursive, as “smallness” refers to what a set is.)</p> </div> <p>Each of these three adjectives describes a different aspect of what makes something a ‘set’, and they serve different purposes, which should not be conflated.</p> <p>That a set is (in the category-theoretic sense) <a class="existingWikiWord" href="/nlab/show/discrete+category">discrete</a> is the most important point; nobody would call a category a ‘set’ merely because it is small and skeletal. (This clause is also the reason why it makes no difference whether we start from categories, <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>-groupois, or <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; discreteness immediately limits us to <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>-<a class="existingWikiWord" href="/nlab/show/0-groupoid">groupoids</a>.) The discreteness of a set reflects its lack of internal structure; while a category may have much structure relating its objects, the only structure remaining in a discrete category is whether any two given objects are <a class="existingWikiWord" href="/nlab/show/isomorphism">isomorphic</a> (and the fact that isomorphism is an <a class="existingWikiWord" href="/nlab/show/equivalence+relation">equivalence relation</a>); if (and only if) they are, then they are considered <strong><a class="existingWikiWord" href="/nlab/show/equality">equal</a></strong> as elements of the set.</p> <p>That a set is <a class="existingWikiWord" href="/nlab/show/small+category">small</a> allows there to be a collection of ‘all’ sets; this collection is not itself small, but we still have a <a class="existingWikiWord" href="/nlab/show/large+category">large category</a> of all sets, <a class="existingWikiWord" href="/nlab/show/Set">Set</a>. A category that is merely discrete and skeletal may be called a <strong><a class="existingWikiWord" href="/nlab/show/class">class</a></strong> instead. But notice that the difference between a set and a class is a rather technical one; a class is just like a set, only (possibly) larger. Indeed, not everyone would agree with the requirement that a set must be small; although that is probably the most common way of talking to deal with size issues, it is not the only way. Another way, used by no less an authority than <em><a class="existingWikiWord" href="/nlab/show/Categories+Work">Categories Work</a></em>, is to posit the existence of a strongly <a class="existingWikiWord" href="/nlab/show/inaccessible+cardinal">inaccessible cardinal</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">\kappa</annotation></semantics></math> and define a <strong><a class="existingWikiWord" href="/nlab/show/small+set">small set</a></strong> to be a set whose <a class="existingWikiWord" href="/nlab/show/cardinality">cardinality</a> is less than <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>κ</mi></mrow><annotation encoding="application/x-tex">\kappa</annotation></semantics></math>.</p> <p>That a set is <a class="existingWikiWord" href="/nlab/show/skeletal+category">skeletal</a> is arguably the least important requirement; in fact, it violates the <a class="existingWikiWord" href="/nlab/show/principle+of+equivalence">principle of equivalence</a>. A category that is merely small and discrete may be called a <strong><a class="existingWikiWord" href="/nlab/show/setoid">setoid</a></strong> instead. However, if you forbid yourself from referring to <a class="existingWikiWord" href="/nlab/show/equality">equality</a> of elements of the setoid (which are the objects of the small discrete category) — or, equivalently, interpret “equality” to mean “isomorphism” therein — then you cannot distinguish the setoid from a set; each is merely a (small) collection of elements with an equivalence relation (called ‘equivalence’ in the setoid and ‘equality’ in the set, in both cases corresponding to isomorphism in a small discrete category). While <a class="existingWikiWord" href="/nlab/show/size+issues">size issues</a> are real and cannot be ignored completely, it is possible to adopt foundations in which the issue of skeletality simply does not appear.</p> <h3 id="InHoTT">In homotopy type theory</h3> <p>As <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a> may be viewed as a theory 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>-<a class="existingWikiWord" href="/nlab/show/infinity-groupoid">groupoids</a>, it falls under the preceding section; but since the language of HoTT is important to learn, let us look at it explicitly:</p> <div class="num_defn"> <h6 id="definition_2">Definition</h6> <p>A <strong>set</strong> is a <a class="existingWikiWord" href="/nlab/show/type">type</a> in which there is an operation connecting any two parallel <a class="existingWikiWord" href="/nlab/show/identity+type">paths</a> by a 2-path:</p> <pre><code>Definition is_set A := forall (x y : A) (p q : x == y), p == q</code></pre> <p>(There are numerous other equivalent definitions; see <a class="existingWikiWord" href="/nlab/show/h-set">h-set</a>.)</p> </div> <p>Because this operation is defined internally, it acts on paths as well as points and implies that, for any two points of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>, the <a class="existingWikiWord" href="/nlab/show/identity+type">type of paths</a> between them is <a class="existingWikiWord" href="/nlab/show/contractible+space">contractible</a> as soon as it is <a class="existingWikiWord" href="/nlab/show/inhabited">inhabited</a>.</p> <p>Regarding types as <a class="existingWikiWord" href="/nlab/show/%E2%88%9E-groupoids">∞-groupoids</a>, this definition takes care only of the discreteness requirement. Regarding smallness, HoTT is usually formulated in <a class="existingWikiWord" href="/nlab/show/Martin-L%C3%B6f+type+theory">Martin-Löf type theory</a> with <a class="existingWikiWord" href="/nlab/show/universes">universes</a> (<a class="existingWikiWord" href="/nlab/show/type+of+types">type of types</a>). If we have chosen one particular universe as the universe of “small” things, then “setness” could be restricted to types belonging to that universe.</p> <p>Finally, skeletality is mostly meaningless in HoTT because paths are the only notion of (propositional) <a class="existingWikiWord" href="/nlab/show/equality">equality</a> which we have to reason with. (There is also the notion of “definitional” equality, but as we cannot assert or prove statements of the form “<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi></mrow><annotation encoding="application/x-tex">y</annotation></semantics></math> are definitionally equal” inside the theory, this is mostly not relevant for the purposes of setness.)</p> <h2 id="related_concepts">Related concepts</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Set">Set</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/classical+set">classical set</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Bishop+set">Bishop set</a>, <a class="existingWikiWord" href="/nlab/show/setoid">setoid</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/definable+set">definable set</a>, <a class="existingWikiWord" href="/nlab/show/constructible+set">constructible set</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/recursive+subset">recursive subset</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/finite+set">finite set</a>, <a class="existingWikiWord" href="/nlab/show/hereditarily+finite+set">hereditarily finite set</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/quantum+set">quantum set</a></p> </li> </ul> <div> <table><thead><tr><th><a class="existingWikiWord" href="/nlab/show/algebra">algebraic</a> <a class="existingWikiWord" href="/nlab/show/mathematical+structure">structure</a></th><th><a class="existingWikiWord" href="/nlab/show/oidification">oidification</a></th></tr></thead><tbody><tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/magma">magma</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/magmoid">magmoid</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/pointed+set">pointed</a> <a class="existingWikiWord" href="/nlab/show/magma">magma</a> with an <a class="existingWikiWord" href="/nlab/show/endofunction">endofunction</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/setoid">setoid</a>/<a class="existingWikiWord" href="/nlab/show/Bishop+set">Bishop set</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/unital+magma">unital magma</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/unital+magmoid">unital magmoid</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/quasigroup">quasigroup</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/quasigroupoid">quasigroupoid</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/loop+%28algebra%29">loop</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/loopoid">loopoid</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/semigroup">semigroup</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/semicategory">semicategory</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/monoid">monoid</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/category">category</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/anti-involution">anti-involutive</a> <a class="existingWikiWord" href="/nlab/show/monoid">monoid</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/dagger+category">dagger category</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/associative+quasigroup">associative quasigroup</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/associative+quasigroupoid">associative quasigroupoid</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/group">group</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/groupoid">groupoid</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/flexible+magma">flexible magma</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/flexible+magmoid">flexible magmoid</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/alternative+magma">alternative magma</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/alternative+magmoid">alternative magmoid</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/absorption+monoid">absorption monoid</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/absorption+category">absorption category</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/cancellative+monoid">cancellative monoid</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/cancellative+category">cancellative category</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/rig">rig</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/CMon">CMon</a>-<a class="existingWikiWord" href="/nlab/show/enriched+category">enriched category</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/nonunital+ring">nonunital ring</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/Ab">Ab</a>-<a class="existingWikiWord" href="/nlab/show/enriched+magmoid">enriched</a> <a class="existingWikiWord" href="/nlab/show/semicategory">semicategory</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/nonassociative+ring">nonassociative ring</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/Ab">Ab</a>-<a class="existingWikiWord" href="/nlab/show/enriched+magmoid">enriched</a> <a class="existingWikiWord" href="/nlab/show/unital+magmoid">unital magmoid</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/ring">ring</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/ringoid">ringoid</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/nonassociative+algebra">nonassociative algebra</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/linear+magmoid">linear magmoid</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/nonassociative+algebra">nonassociative unital algebra</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/unital+magmoid">unital</a> <a class="existingWikiWord" href="/nlab/show/linear+magmoid">linear magmoid</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/nonunital+algebra">nonunital algebra</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/linear+magmoid">linear</a> <a class="existingWikiWord" href="/nlab/show/semicategory">semicategory</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/associative+unital+algebra">associative unital algebra</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/linear+category">linear category</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/C-star+algebra">C-star algebra</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/C-star+category">C-star category</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/differential+algebra">differential algebra</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/differential+algebroid">differential algebroid</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/flexible+algebra">flexible algebra</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/flexible+magmoid">flexible</a> <a class="existingWikiWord" href="/nlab/show/linear+magmoid">linear magmoid</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/alternative+algebra">alternative algebra</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/alternative+magmoid">alternative</a> <a class="existingWikiWord" href="/nlab/show/linear+magmoid">linear magmoid</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/Lie+algebra">Lie algebra</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/Lie+algebroid">Lie algebroid</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/monoidal+poset">monoidal poset</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/2-poset">2-poset</a></td></tr> <tr><td style="text-align: left;"><span class="newWikiWord">strict monoidal groupoid<a href="/nlab/new/strict+monoidal+groupoid">?</a></span></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/strict+%282%2C1%29-category">strict (2,1)-category</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/strict+2-group">strict 2-group</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/strict+2-groupoid">strict 2-groupoid</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/strict+monoidal+category">strict monoidal category</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/strict+2-category">strict 2-category</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/monoidal+groupoid">monoidal groupoid</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/%282%2C1%29-category">(2,1)-category</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/2-group">2-group</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/2-groupoid">2-groupoid</a>/<a class="existingWikiWord" href="/nlab/show/bigroupoid">bigroupoid</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/monoidal+category">monoidal category</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/2-category">2-category</a>/<a class="existingWikiWord" href="/nlab/show/bicategory">bicategory</a></td></tr> </tbody></table> </div><div> <table><thead><tr><th><a class="existingWikiWord" href="/nlab/show/homotopy+level">homotopy level</a></th><th><a class="existingWikiWord" href="/nlab/show/n-truncated+object+in+an+%28infinity%2C1%29-category">n-truncation</a></th><th><a class="existingWikiWord" href="/nlab/show/homotopy+theory">homotopy theory</a></th><th><a class="existingWikiWord" href="/nlab/show/higher+category+theory">higher category theory</a></th><th><a class="existingWikiWord" href="/nlab/show/%28infinity%2C1%29-topos+theory">higher topos theory</a></th><th><a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a></th></tr></thead><tbody><tr><td style="text-align: left;">h-level 0</td><td style="text-align: left;">(-2)-truncated</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/contractible+space">contractible space</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/%28-2%29-groupoid">(-2)-groupoid</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/true">true</a>/<a class="existingWikiWord" href="/nlab/show/unit+type">unit type</a>/<a class="existingWikiWord" href="/nlab/show/contractible+type">contractible type</a></td></tr> <tr><td style="text-align: left;">h-level 1</td><td style="text-align: left;">(-1)-truncated</td><td style="text-align: left;">contractible-if-<a class="existingWikiWord" href="/nlab/show/inhabited+space">inhabited</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/%28-1%29-groupoid">(-1)-groupoid</a>/<a class="existingWikiWord" href="/nlab/show/truth+value">truth value</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/%280%2C1%29-sheaf">(0,1)-sheaf</a>/<a class="existingWikiWord" href="/nlab/show/ideal">ideal</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/mere+proposition">mere proposition</a>/<a class="existingWikiWord" href="/nlab/show/h-proposition">h-proposition</a></td></tr> <tr><td style="text-align: left;">h-level 2</td><td style="text-align: left;">0-truncated</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/homotopy+0-type">homotopy 0-type</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/0-groupoid">0-groupoid</a>/<a class="existingWikiWord" href="/nlab/show/set">set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/sheaf">sheaf</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/h-set">h-set</a></td></tr> <tr><td style="text-align: left;">h-level 3</td><td style="text-align: left;">1-truncated</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/homotopy+1-type">homotopy 1-type</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/1-groupoid">1-groupoid</a>/<a class="existingWikiWord" href="/nlab/show/groupoid">groupoid</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/%282%2C1%29-sheaf">(2,1)-sheaf</a>/<a class="existingWikiWord" href="/nlab/show/stack">stack</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/h-groupoid">h-groupoid</a></td></tr> <tr><td style="text-align: left;">h-level 4</td><td style="text-align: left;">2-truncated</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/homotopy+2-type">homotopy 2-type</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/2-groupoid">2-groupoid</a></td><td style="text-align: left;">(3,1)-sheaf/2-stack</td><td style="text-align: left;">h-2-groupoid</td></tr> <tr><td style="text-align: left;">h-level 5</td><td style="text-align: left;">3-truncated</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/homotopy+3-type">homotopy 3-type</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/3-groupoid">3-groupoid</a></td><td style="text-align: left;">(4,1)-sheaf/3-stack</td><td style="text-align: left;">h-3-groupoid</td></tr> <tr><td style="text-align: left;">h-level <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>n</mi><mo>+</mo><mn>2</mn></mrow><annotation encoding="application/x-tex">n+2</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>n</mi></mrow><annotation encoding="application/x-tex">n</annotation></semantics></math>-truncated</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/homotopy+n-type">homotopy n-type</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/n-groupoid">n-groupoid</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/%28n%2B1%2C1%29-sheaf">(n+1,1)-sheaf</a>/<a class="existingWikiWord" href="/nlab/show/n-stack">n-stack</a></td><td style="text-align: left;">h-<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>-groupoid</td></tr> <tr><td style="text-align: left;">h-level <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></td><td style="text-align: left;">untruncated</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/homotopy+type">homotopy type</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/%E2%88%9E-groupoid">∞-groupoid</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2C1%29-sheaf">(∞,1)-sheaf</a>/<a class="existingWikiWord" href="/nlab/show/%E2%88%9E-stack">∞-stack</a></td><td style="text-align: left;">h-<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</td></tr> </tbody></table> </div> <h2 id="references">References</h2> <h3 id="general">General</h3> <p>Formalization of sets in <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a> (via <a class="existingWikiWord" href="/nlab/show/h-sets">h-sets</a>):</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Egbert+Rijke">Egbert Rijke</a>, <a class="existingWikiWord" href="/nlab/show/Bas+Spitters">Bas Spitters</a>, <em>Sets in homotopy type theory</em>, Mathematical Structures in Computer Science <strong>25</strong> 5 “From type theory and homotopy theory to Univalent Foundations of Mathematics” (2015) 1172-1202 <p>[<a href="https://doi.org/10.1017/S0960129514000553">doi:10.1017/S0960129514000553</a>, <a href="http://arxiv.org/abs/1305.3835">arXiv:1305.3835</a>]</p> </li> </ul> <h3 id="history">History</h3> <p>An early definition of “set” appears in</p> <ul> <li>Bernard Bolzano, <em>Paradoxien des Unendlichen</em> (1847)</li> </ul> <p>where in section 4 it says in translation</p> <blockquote> <p>There are wholes which, although they contain the same parts A, B, C, D, …, nevertheless present themselves as different when seen from our point of view or conception (this kind of difference we call ‘essential’), e.g. a complete and a broken glass viewed as a drinking vessel. [] A whole whose basic conception renders the arrangement of its parts a matter of indifference (and whose rearrangement therefore changes nothing essential from our point of view, if only that changes), I call a set.</p> </blockquote> </body></html> </div> <div class="revisedby"> <p> Last revised on August 20, 2024 at 19:33:18. See the <a href="/nlab/history/set" 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/set" accesskey="E" class="navlink" id="edit" rel="nofollow">Edit</a><a href="https://nforum.ncatlab.org/discussion/15973/#Item_1">Discuss</a><span class="backintime"><a href="/nlab/revision/set/34" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/diff/set" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Changes from previous revision</a><a href="/nlab/history/set" accesskey="S" class="navlink" id="history" rel="nofollow">History (34 revisions)</a> <a href="/nlab/show/set/cite" style="color: black">Cite</a> <a href="/nlab/print/set" accesskey="p" id="view_print" rel="nofollow">Print</a> <a href="/nlab/source/set" id="view_source" rel="nofollow">Source</a> </div> </div>  </div>  </body> </html>