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/824/#Item_18" 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>The category of sets</title></head> <body> <div class="rightHandSide"> <div class="toc clickDown" tabindex="0"> <h3 id="context">Context</h3> <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="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+inequality+spaces">axiom of inequality spaces</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="categories_of_categories">Categories of categories</h4> <div class="hide"><div> <p><strong><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>n</mi><mo>+</mo><mn>1</mn><mo>,</mo><mi>r</mi><mo>+</mo><mn>1</mn><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(n+1,r+1)</annotation></semantics></math>-categories of <a class="existingWikiWord" href="/nlab/show/%28n%2Cr%29-categories">(n,r)-categories</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Pos">Pos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Set">Set</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Rel">Rel</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Grpd">Grpd</a>, <a class="existingWikiWord" href="/nlab/show/%E2%88%9EGrpd">∞Grpd</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Cat">Cat</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Ho%28Cat%29">Ho(Cat)</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/AccCat">AccCat</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/PrCat">PrCat</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/LexCat">LexCat</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/MonCat">MonCat</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/VCat">VCat</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/CatAdj">CatAdj</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Prof">Prof</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Operad">Operad</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/2Cat">2Cat</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/ModCat">ModCat</a>, <a class="existingWikiWord" href="/nlab/show/CombModCat">CombModCat</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2C1%29Cat">(∞,1)Cat</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Pr%28%E2%88%9E%2C1%29Cat">Pr(∞,1)Cat</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2C1%29Operad">(∞,1)Operad</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2Cn%29Cat">(∞,n)Cat</a></p> </li> </ul> </div></div> </div> </div> <h1 id="the_category_of_sets">The category of sets</h1> <div class='maruku_toc'> <ul> <li><a href='#definition'>Definition</a></li> <li><a href='#properties'>Properties</a></li> <ul> <li><a href='#characterization'>Characterization</a></li> <li><a href='#size'>Size</a></li> <li><a href='#OppositeCategory'>Opposite category and Boolean algebras</a></li> </ul> <li><a href='#related_categories'>Related categories</a></li> <li><a href='#references'>References</a></li> </ul> </div> <h2 id="definition">Definition</h2> <p><strong><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math></strong> is the (or a) <a class="existingWikiWord" href="/nlab/show/category">category</a> with <a class="existingWikiWord" href="/nlab/show/sets">sets</a> as <a class="existingWikiWord" href="/nlab/show/objects">objects</a> and <a class="existingWikiWord" href="/nlab/show/functions">functions</a> between sets as <a class="existingWikiWord" href="/nlab/show/morphisms">morphisms</a>.</p> <p>This definition is somewhat vague by design. Rather than canonize a fixed set of principles, the nLab adopts a ‘pluralist’ point of view which recognizes different needs and foundational assumptions among mathematicians who use set theory. Thus, there are various axes to consider when formulating categorical properties one thinks <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> should satisfy, including</p> <ul> <li> <p>first-order vs. higher-order logic</p> </li> <li> <p>impredicative vs. <a class="existingWikiWord" href="/nlab/show/predicative+mathematics">predicative mathematics</a></p> </li> <li> <p>‘variability’ vs. ‘constancy’ (Lawvere)</p> </li> <li> <p>classical logic vs. intuitionistic logic</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/image+factorizations">image factorizations</a> and <a class="existingWikiWord" href="/nlab/show/quotient+sets">quotient sets</a>, i.e. <a class="existingWikiWord" href="/nlab/show/sets">sets</a> vs <a class="existingWikiWord" href="/nlab/show/setoids">setoids</a>.</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/initial+object">initial</a> and <a class="existingWikiWord" href="/nlab/show/free+object">free</a> structures, i.e. <a class="existingWikiWord" href="/nlab/show/transfinite+construction+of+free+algebras">transfinite construction of free algebras</a>/<a class="existingWikiWord" href="/nlab/show/quotient+inductive+types">quotient inductive types</a></p> </li> <li> <p>choice principles</p> </li> <li> <p>replacement or collection principles</p> </li> <li> <p>smallness structures</p> </li> </ul> <p>just to name a few. Quite a bit of axiomatic fine-tuning can enter when one considers the panoply of hypotheses that might appeal to one or another school of intuitionism or constructivism, or various combinatorial or cardinal hypotheses one might attach to ZFC, etc.</p> <h2 id="properties">Properties</h2> <h3 id="characterization">Characterization</h3> <p>The category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> has many marvelous properties, which make it a common choice for serving as a ‘<a class="existingWikiWord" href="/nlab/show/foundations">foundation</a>’ of mathematics. For instance:</p> <ul> <li> <p>It is a <a class="existingWikiWord" href="/nlab/show/well-pointed+category">well-pointed</a> <a class="existingWikiWord" href="/nlab/show/topos">topos</a>,</p> <p>So in particular it is <a class="existingWikiWord" href="/nlab/show/locally+cartesian+closed+category">locally cartesian closed</a>.</p> </li> <li> <p>It is <a class="existingWikiWord" href="/nlab/show/locally+small">locally small</a>.</p> </li> <li> <p>It is <a class="existingWikiWord" href="/nlab/show/complete+category">complete</a> and <a class="existingWikiWord" href="/nlab/show/cocomplete+category">cocomplete</a> (in fact, <span class="newWikiWord">locally finitely presentable<a href="/nlab/new/locally+finitely+presentable">?</a></span>), and therefore <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/extensive+category">extensive</a> (as is any cocomplete topos).</p> </li> </ul> <p>At least assuming <a class="existingWikiWord" href="/nlab/show/classical+logic">classical logic</a>, these properties suffice to characterize <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> uniquely up to equivalence among all categories; see <a class="existingWikiWord" href="/nlab/show/cocomplete+well-pointed+topos">cocomplete well-pointed topos</a>. Note, however, that the definitions of “locally small” and “(co)complete” presuppose a notion of <em>small</em> and therefore a knowledge of what a <em>set</em> (as opposed to a <a class="existingWikiWord" href="/nlab/show/proper+class">proper class</a>) is.</p> <p>The <a class="existingWikiWord" href="/nlab/show/core+groupoid">core groupoid</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> (whose <a class="existingWikiWord" href="/nlab/show/morphisms">morphisms</a> are the <a class="existingWikiWord" href="/nlab/show/bijections">bijections</a>) is characterized by the fact that</p> <ul> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Core</mi><mo stretchy="false">(</mo><mi>Set</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Core(Set)</annotation></semantics></math> is the <a class="existingWikiWord" href="/nlab/show/discrete+object+classifier">discrete object classifier</a> in the category <a class="existingWikiWord" href="/nlab/show/Grpd">Grpd</a> of <a class="existingWikiWord" href="/nlab/show/groupoids">groupoids</a> and <a class="existingWikiWord" href="/nlab/show/functors">functors</a>, playing a similar role in classifying discrete groupoids in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Grpd</mi></mrow><annotation encoding="application/x-tex">Grpd</annotation></semantics></math> that the set of truth values <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Ω</mi></mrow><annotation encoding="application/x-tex">\Omega</annotation></semantics></math> does in classifying subsets in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math>. The morphism <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi><mo>:</mo><mi>I</mi><mo>→</mo><mi>Set</mi></mrow><annotation encoding="application/x-tex">F:I \rightarrow Set</annotation></semantics></math> is an <a class="existingWikiWord" href="/nlab/show/indexed+family">indexed family</a> of sets and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>I</mi></mrow><annotation encoding="application/x-tex">I</annotation></semantics></math> is an index groupoid.</li> </ul> <p>As a <a class="existingWikiWord" href="/nlab/show/topos">topos</a>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> is also characterized by the fact that</p> <ul> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> is the <a class="existingWikiWord" href="/nlab/show/terminal+object">terminal object</a> in the <a class="existingWikiWord" href="/nlab/show/category">category</a> of <a class="existingWikiWord" href="/nlab/show/Grothendieck+toposes">Grothendieck toposes</a> and <a class="existingWikiWord" href="/nlab/show/geometric+morphism">geometric morphism</a>s. The terminal morphism <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo lspace="verythinmathspace">:</mo><mi>E</mi><mo>→</mo><mi>Set</mi></mrow><annotation encoding="application/x-tex">\Gamma\colon E \to Set</annotation></semantics></math> from any other topos <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>E</mi></mrow><annotation encoding="application/x-tex">E</annotation></semantics></math> is the <a class="existingWikiWord" href="/nlab/show/global+section">global section</a>s functor.</li> </ul> <p>It is usually assumed that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> satisfies the <a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a> and has a <a class="existingWikiWord" href="/nlab/show/natural+numbers+object">natural numbers object</a>. In Lawvere’s theory <a class="existingWikiWord" href="/nlab/show/ETCS">ETCS</a>, which can serve as a foundation for much of mathematics, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> is asserted to be a well-pointed topos that satisfies the axiom of choice and has a natural numbers object. It follows that it is automatically “locally small” and “complete and cocomplete” relative to the notion of “smallness” defined in terms of itself (actually, this is true for any topos).</p> <p>Conversely, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo lspace="0em" rspace="thinmathspace">Set</mo></mrow><annotation encoding="application/x-tex">\Set</annotation></semantics></math> in <a class="existingWikiWord" href="/nlab/show/constructive+mathematics">constructive mathematics</a> cannot satisfy the axiom of choice (since this implies <a class="existingWikiWord" href="/nlab/show/excluded+middle">excluded middle</a>), although constructivists might accept <a class="existingWikiWord" href="/nlab/show/COSHEP">COSHEP</a> (that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> has <a class="existingWikiWord" href="/nlab/show/projective+object">enough projectives</a>). In <a class="existingWikiWord" href="/nlab/show/predicative+mathematics">predicative mathematics</a>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo lspace="0em" rspace="thinmathspace">Set</mo></mrow><annotation encoding="application/x-tex">\Set</annotation></semantics></math> is not even a topos, although most predicativists would still agree that it is a <a class="existingWikiWord" href="/nlab/show/pretopos">pretopos</a>, and predicativists of the constructive school would even agree that it is a <a class="existingWikiWord" href="/nlab/show/locally+cartesian+closed+category">locally cartesian closed</a> pretopos.</p> <h3 id="size">Size</h3> <p>Above we considered <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> to be the category of <em>all</em> sets, so that in particular <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> itself is a <a class="existingWikiWord" href="/nlab/show/large+category">large category</a>. Authors who assume a <a class="existingWikiWord" href="/nlab/show/Grothendieck+universe">Grothendieck universe</a> as part of their <a class="existingWikiWord" href="/nlab/show/foundations">foundations</a> often define <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> to be the category of <em>small</em> sets (those contained in the universe). One often then writes <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>SET</mi></mrow><annotation encoding="application/x-tex">SET</annotation></semantics></math> for the category of <em>large</em> sets, which is the <a class="existingWikiWord" href="/nlab/show/universe+enlargement">universe enlargement</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math>.</p> <h3 id="OppositeCategory">Opposite category and Boolean algebras</h3> <div class="num_prop"> <h6 id="proposition">Proposition</h6> <p>The <a class="existingWikiWord" href="/nlab/show/power+set">power set</a>-<a class="existingWikiWord" href="/nlab/show/functor">functor</a></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>𝒫</mi><mspace width="thickmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thickmathspace"></mspace><mi>Set</mi><mo>→</mo><msup><mi>Bool</mi> <mi>op</mi></msup></mrow><annotation encoding="application/x-tex"> \mathcal{P} \;\colon\; Set \to Bool^{op} </annotation></semantics></math></div> <p>is a <a class="existingWikiWord" href="/nlab/show/faithful+functor">faithful functor</a> which in its <a href="http://ncatlab.org/nlab/show/%28eso%2Bfull%2C+faithful%29+factorization+system">(eso+full, faithful) factorization</a> induces an <a class="existingWikiWord" href="/nlab/show/equivalence+of+categories">equivalence of categories</a> between <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> and the <a class="existingWikiWord" href="/nlab/show/opposite+category">opposite category</a> of that of <a class="existingWikiWord" href="/nlab/show/complete+atomic+Boolean+algebras">complete atomic Boolean algebras</a>.</p> </div> <p>See for instance <a href="#vanOosten">van Oosten, theorem 2.4</a></p> <div class="num_remark"> <h6 id="remark">Remark</h6> <p>Restricted to <a class="existingWikiWord" href="/nlab/show/FinSet">FinSet</a> this equivalence restricts to an equivalence with finite Boolean algebras. See at <em><a class="existingWikiWord" href="/nlab/show/Stone+duality">Stone duality</a></em> for more on this.</p> </div> <div class="num_remark"> <h6 id="remark_2">Remark</h6> <p>In constructive mathematics, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>𝒫</mi></mrow><annotation encoding="application/x-tex">\mathcal{P}</annotation></semantics></math> defines an equivalence of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo lspace="0em" rspace="thinmathspace">Set</mo></mrow><annotation encoding="application/x-tex">\Set</annotation></semantics></math> with the opposite category of that of <a class="existingWikiWord" href="/nlab/show/complete+lattice">complete</a> <a class="existingWikiWord" href="/nlab/show/atom">atomic</a> <a class="existingWikiWord" href="/nlab/show/Heyting+algebras">Heyting algebras</a>. In fact, for any elementary <a class="existingWikiWord" href="/nlab/show/topos">topos</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">\mathcal{E}</annotation></semantics></math>, the <a class="existingWikiWord" href="/nlab/show/power+object">power object</a> functor defines an equivalence of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}</annotation></semantics></math> with the opposite category of that of internal complete atomic Heyting algebras. (This phrase can be interpreted using the <a class="existingWikiWord" href="/nlab/show/internal+language">internal language</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}</annotation></semantics></math>.)</p> </div> <h2 id="related_categories">Related categories</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Set+in+homotopy+type+theory">Set in homotopy type theory</a></p> </li> <li> <p>A variant of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> where <a class="existingWikiWord" href="/nlab/show/functions">functions</a> are generalized to <a class="existingWikiWord" href="/nlab/show/relations">relations</a> is <em><a class="existingWikiWord" href="/nlab/show/Rel">Rel</a></em>.</p> </li> </ul> <div> <p><strong><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>n</mi><mo>+</mo><mn>1</mn><mo>,</mo><mi>r</mi><mo>+</mo><mn>1</mn><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(n+1,r+1)</annotation></semantics></math>-categories of <a class="existingWikiWord" href="/nlab/show/%28n%2Cr%29-categories">(n,r)-categories</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Pos">Pos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Set">Set</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Rel">Rel</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Grpd">Grpd</a>, <a class="existingWikiWord" href="/nlab/show/%E2%88%9EGrpd">∞Grpd</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Cat">Cat</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Ho%28Cat%29">Ho(Cat)</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/AccCat">AccCat</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/PrCat">PrCat</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/LexCat">LexCat</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/MonCat">MonCat</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/VCat">VCat</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/CatAdj">CatAdj</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Prof">Prof</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Operad">Operad</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/2Cat">2Cat</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/ModCat">ModCat</a>, <a class="existingWikiWord" href="/nlab/show/CombModCat">CombModCat</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2C1%29Cat">(∞,1)Cat</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Pr%28%E2%88%9E%2C1%29Cat">Pr(∞,1)Cat</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2C1%29Operad">(∞,1)Operad</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2Cn%29Cat">(∞,n)Cat</a></p> </li> </ul> </div> <h2 id="references">References</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Saunders+MacLane">Saunders MacLane</a>, §IV.10 of: <em><a class="existingWikiWord" href="/nlab/show/Categories+for+the+Working+Mathematician">Categories for the Working Mathematician</a></em>, Graduate Texts in Mathematics <strong>5</strong> Springer (1971, second ed. 1997) [<a href="https://link.springer.com/book/10.1007/978-1-4757-4721-8">doi:10.1007/978-1-4757-4721-8</a>]</p> </li> <li id="vanOosten"> <p><a class="existingWikiWord" href="/nlab/show/Jaap+van+Oosten">Jaap van Oosten</a>, <em>Basic category theory</em> (<a href="http://www.staff.science.uu.nl/~ooste110/syllabi/catsmoeder.pdf">pdf</a>)</p> </li> </ul> <p>On <a class="existingWikiWord" href="/nlab/show/Set+in+homotopy+type+theory">Set in homotopy type theory</a>:</p> <ul> <li id="RijkeSpitters13"><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, Volume 25, Issue 5 (From type theory and homotopy theory to Univalent Foundations of Mathematics) (<a href="http://arxiv.org/abs/1305.3835">arXiv:1305.3835</a>)</li> </ul> <div class="property">category: <a class="category_link" href="/nlab/all_pages/category">category</a></div></body></html> </div> <div class="revisedby"> <p> Last revised on January 3, 2024 at 15:20:43. 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/824/#Item_18">Discuss</a><span class="backintime"><a href="/nlab/revision/Set/41" 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 (41 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>