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> universe 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> universe </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/2041/#Item_67" title="Discuss this page in its dedicated thread on the nForum" style="color: black">Discuss this page</a> | <form accept-charset="utf-8" action="/nlab/search" id="navigationSearchForm" method="get"> <fieldset class="search"><input type="text" id="searchField" name="query" value="Search" style="display:inline-block; float: left;" onfocus="this.value == 'Search' ? this.value = '' : true" onblur="this.value == '' ? this.value = 'Search' : true" /></fieldset> </form> <span id='navEnd'></span> </div> <div id="revision"> <html xmlns="http://www.w3.org/1999/xhtml" xmlns:svg="http://www.w3.org/2000/svg" xml:lang="en" lang="en"> <head><meta http-equiv="Content-type" content="application/xhtml+xml;charset=utf-8" /><title>Contents</title></head> <body> <blockquote> <p>This entry is about the notion in <a class="existingWikiWord" href="/nlab/show/mathematics">mathematics</a>/<a class="existingWikiWord" href="/nlab/show/logic">logic</a>/<a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a>. For the notion of the same name in <a class="existingWikiWord" href="/nlab/show/physics">physics</a> see at <em><a class="existingWikiWord" href="/nlab/show/observable+universe">observable universe</a></em>.</p> </blockquote> <hr /> <div class="rightHandSide"> <div class="toc clickDown" tabindex="0"> <h3 id="context">Context</h3> <h4 id="universes">Universes</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/universe">universe</a></strong></p> <p>(in <a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a>/<a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a>/<a class="existingWikiWord" href="/nlab/show/computer+science">computer science</a>)</p> <p><strong>of all <a class="existingWikiWord" href="/nlab/show/homotopy+types">homotopy types</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/type+of+types">type of types</a>, <a class="existingWikiWord" href="/nlab/show/object+classifier">object classifier</a>,</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/univalence">univalence</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/codomain+fibration">codomain fibration</a></p> </li> </ul> <p><strong>of <a class="existingWikiWord" href="/nlab/show/homotopy+n-types">homotopy n-types</a></strong></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/type+of+n-types">type of n-types</a></li> </ul> <p><strong>of <a class="existingWikiWord" href="/nlab/show/0-truncated+object">0-truncated types</a>/<a class="existingWikiWord" href="/nlab/show/h-sets">h-sets</a></strong></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/type+of+h-sets">type of h-sets</a>, <a class="existingWikiWord" href="/nlab/show/universe+in+a+topos">universe in a topos</a></li> </ul> <p><strong>of <a class="existingWikiWord" href="/nlab/show/%28-1%29-truncated+object">(-1)-truncated types</a>/<a class="existingWikiWord" href="/nlab/show/h-propositions">h-propositions</a></strong></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/type+of+propositions">type of propositions</a>, <a class="existingWikiWord" href="/nlab/show/subobject+classifier">subobject classifier</a></li> </ul> <h3 id="resizing">resizing</h3> <ul> <li><a class="existingWikiWord" href="/nlab/show/universe+enlargement">universe enlargement</a></li> </ul> </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> </div> </div> <h1 id="contents">Contents</h1> <div class='maruku_toc'> <ul> <li><a href='#idea'>Idea</a></li> <li><a href='#categories_as_universes'>Categories as universes</a></li> <li><a href='#universes_as_classes'>Universes as classes</a></li> <li><a href='#grothendieck_universes'>Grothendieck universes</a></li> <li><a href='#universes_inside_'>Universes inside <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></a></li> <li><a href='#reflection'>Reflection</a></li> <li><a href='#universes_in_type_theory'>Universes in type theory</a></li> <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='#in_type_theory'>In type theory</a></li> </ul> </ul> </div> <h2 id="idea">Idea</h2> <p>A universe is a realm within which (some conceived part, naively and virtually all, of) <a class="existingWikiWord" href="/nlab/show/mathematics">mathematics</a> may be thought of as taking place. Universes can be purely metamathematical, but we can also reflect upon them and bring them into mathematics. There are several different kinds of ‘universes’. For a physical notion of universe see <a class="existingWikiWord" href="/nlab/show/observable+universe">observable universe</a>.</p> <h2 id="categories_as_universes">Categories as universes</h2> <p>Much of <a class="existingWikiWord" href="/nlab/show/ordinary+mathematics">ordinary mathematics</a> can be thought of as taking place <a class="existingWikiWord" href="/nlab/show/internalization">inside</a> “the archetypical <a class="existingWikiWord" href="/nlab/show/category">category</a> <a class="existingWikiWord" href="/nlab/show/Set">SET</a> of sets”. Typically, the properties 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> are formulated in <a class="existingWikiWord" href="/nlab/show/first-order+logic">first-order logic</a> using a <a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a> such as <a class="existingWikiWord" href="/nlab/show/ZFC">ZFC</a> or (more directly) <a class="existingWikiWord" href="/nlab/show/ETCS">ETCS</a>.</p> <p>We can generalise this from <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 any other <a class="existingWikiWord" href="/nlab/show/category">category</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math>. Without further assumptions on the category, there is in general very little mathematics that can be formulated inside it, but a few extra properties and structures are usually sufficient to provide something interesting. This is the general topic of <em><a class="existingWikiWord" href="/nlab/show/internalisation">internalisation</a></em>. The attitude to take is that any <em>specific</em> category is merely one <a class="existingWikiWord" href="/nlab/show/model">model</a>, while a general <em>class</em> of categories is a <a class="existingWikiWord" href="/nlab/show/theory">theory</a> (really a <a class="existingWikiWord" href="/nlab/show/doctrine">doctrine</a>, or <a class="existingWikiWord" href="/nlab/show/2-theory">2-theory</a>).</p> <p>We can also use <a class="existingWikiWord" href="/nlab/show/higher+category+theory">higher categories</a> instead of mere categories here. Even for ordinary mathematics, this means starting with <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-Grpd">GRPD</a> instead 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> <h2 id="universes_as_classes">Universes as classes</h2> <p>The idea of the <a class="existingWikiWord" href="/nlab/show/large+category">large category</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> as the universe of mathematics has an analogue in <a class="existingWikiWord" href="/nlab/show/class+theory">class theory</a>. In a <a class="existingWikiWord" href="/nlab/show/material+class+theory">material class theory</a>, the <strong>von Neumann universe</strong> <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> is the <a class="existingWikiWord" href="/nlab/show/class">class</a> of all <a class="existingWikiWord" href="/nlab/show/axiom+of+foundation">well-founded</a> <a class="existingWikiWord" href="/nlab/show/pure+sets">pure sets</a>.</p> <p>More explicitly: for every <a class="existingWikiWord" href="/nlab/show/ordinal+number">ordinal number</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">\alpha</annotation></semantics></math>, we have a <a class="existingWikiWord" href="/nlab/show/set">set</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>V</mi> <mi>α</mi></msub></mrow><annotation encoding="application/x-tex">V_\alpha</annotation></semantics></math> (the von Neumann universe of <strong>rank</strong> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>α</mi></mrow><annotation encoding="application/x-tex">\alpha</annotation></semantics></math>), defined <a class="existingWikiWord" href="/nlab/show/recursion">recursively</a> using the operations of <a class="existingWikiWord" href="/nlab/show/power+set">power set</a> and (material) <a class="existingWikiWord" href="/nlab/show/union">union</a> as</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msub><mi>V</mi> <mi>α</mi></msub><mo>≔</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">⋃</mo> <mrow><mi>β</mi><mo><</mo><mi>α</mi></mrow></munder><mi>𝒫</mi><msub><mi>V</mi> <mi>β</mi></msub><mo>.</mo></mrow><annotation encoding="application/x-tex"> V_\alpha \coloneqq \bigcup_{\beta \lt \alpha} \mathcal{P}V_\beta .</annotation></semantics></math></div> <p>Then <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> itself is the union of all of the <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>V</mi> <mi>α</mi></msub></mrow><annotation encoding="application/x-tex">V_\alpha</annotation></semantics></math>.</p> <p>A similar but more complicated definition allows us to define the universe <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>L</mi></mrow><annotation encoding="application/x-tex">L</annotation></semantics></math> of <a class="existingWikiWord" href="/nlab/show/constructible+set">constructible set</a>s, called the <a class="existingWikiWord" href="/nlab/show/constructible+universe">constructible universe</a>.</p> <p>See also a <a href="https://secure.wikimedia.org/wikipedia/en/wiki/Universe_%28mathematics%29">Wikipedia article</a> written largely by <a class="existingWikiWord" href="/nlab/show/Toby+Bartels">Toby Bartels</a> in another lifetime.</p> <p>In a <a class="existingWikiWord" href="/nlab/show/structural+class+theory">structural class theory</a>, such as the <a class="existingWikiWord" href="/nlab/show/category+with+class+structure">category with class structure</a> found in <a class="existingWikiWord" href="/nlab/show/algebraic+set+theory">algebraic set theory</a>, a <strong>universe</strong> is a class <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi></mrow><annotation encoding="application/x-tex">U</annotation></semantics></math> with a <a class="existingWikiWord" href="/nlab/show/monic">monic</a> class <a class="existingWikiWord" href="/nlab/show/map">map</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>𝒫</mi><mo stretchy="false">(</mo><mi>U</mi><mo stretchy="false">)</mo><mo>↪</mo><mi>U</mi></mrow><annotation encoding="application/x-tex">\mathcal{P}(U) \hookrightarrow U</annotation></semantics></math> from the <a class="existingWikiWord" href="/nlab/show/power+object">powerclass</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi></mrow><annotation encoding="application/x-tex">U</annotation></semantics></math> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi></mrow><annotation encoding="application/x-tex">U</annotation></semantics></math>. In particular, every <a class="existingWikiWord" href="/nlab/show/universal+class">universal class</a> is a universe.</p> <h2 id="grothendieck_universes">Grothendieck universes</h2> <p>A <a class="existingWikiWord" href="/nlab/show/Grothendieck+universe">Grothendieck universe</a> is a set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi></mrow><annotation encoding="application/x-tex">U</annotation></semantics></math> such that the following properties hold for <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi></mrow><annotation encoding="application/x-tex">U</annotation></semantics></math>:</p> <ol> <li>if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>a</mi><mo>∈</mo><mi>U</mi></mrow><annotation encoding="application/x-tex">x \in a \in U</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>U</mi></mrow><annotation encoding="application/x-tex">x \in U</annotation></semantics></math>;</li> <li>if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>,</mo><mi>b</mi><mo>∈</mo><mi>U</mi></mrow><annotation encoding="application/x-tex">a, b \in U</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">{</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\{a, b\}</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>×</mo><mi>b</mi></mrow><annotation encoding="application/x-tex">a\times b</annotation></semantics></math> are elements of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi></mrow><annotation encoding="application/x-tex">U</annotation></semantics></math>;</li> <li>if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∈</mo><mi>U</mi></mrow><annotation encoding="application/x-tex">a \in U</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∪</mo><mi>a</mi></mrow><annotation encoding="application/x-tex">\cup a</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">P(a)</annotation></semantics></math> are elements of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi></mrow><annotation encoding="application/x-tex">U</annotation></semantics></math>;</li> <li>the set <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> of all natural numbers is an element of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi></mrow><annotation encoding="application/x-tex">U</annotation></semantics></math>;</li> <li>if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><mi>a</mi><mo>→</mo><mi>b</mi></mrow><annotation encoding="application/x-tex">f:a \to b</annotation></semantics></math> is surjective with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∈</mo><mi>U</mi></mrow><annotation encoding="application/x-tex">a \in U</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi><mo>⊆</mo><mi>U</mi></mrow><annotation encoding="application/x-tex">b \subseteq U</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi><mo>∈</mo><mi>U</mi></mrow><annotation encoding="application/x-tex">b \in U</annotation></semantics></math>.</li> </ol> <h2 id="universes_inside_">Universes inside <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></h2> <p>If set theory is the <a class="existingWikiWord" href="/nlab/show/foundation+of+mathematics">foundation of mathematics</a>, then the universes above are part of metamathematics rather than mathematics itself. However, we can also look for <a class="existingWikiWord" href="/nlab/show/small+categories">small categories</a> or sets that exist within set theory and have the properties of a universe.</p> <p>There is already a hint of this in the hierarchy <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>V</mi> <mi>α</mi></msub></mrow><annotation encoding="application/x-tex">V_\alpha</annotation></semantics></math> out of which the von Neumann universe is built. For some values 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">\alpha</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>V</mi> <mi>α</mi></msub></mrow><annotation encoding="application/x-tex">V_\alpha</annotation></semantics></math> might be a sufficiently large and complete collection of <a class="existingWikiWord" href="/nlab/show/sets">sets</a> in which to do ordinary mathematics. From the <a class="existingWikiWord" href="/nlab/show/nPOV">nPOV</a>, we can instead look at the category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Set</mi> <mi>α</mi></msub></mrow><annotation encoding="application/x-tex">Set_\alpha</annotation></semantics></math> of these sets and the <a class="existingWikiWord" href="/nlab/show/functions">functions</a> between them, although it's more common to think about <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Set</mi> <mi>κ</mi></msub></mrow><annotation encoding="application/x-tex">Set_\kappa</annotation></semantics></math> for some <a class="existingWikiWord" href="/nlab/show/cardinal+number">cardinal number</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>.</p> <p>An <a class="existingWikiWord" href="/nlab/show/infinite+set">infinite set</a> is a simple example, as <a class="existingWikiWord" href="/nlab/show/finite+mathematics">finite mathematics</a> can be done inside it. Going beyond this, a <a class="existingWikiWord" href="/nlab/show/Grothendieck+universe">Grothendieck universe</a> is a set within which other infinite sets exist but which is complete under the operations of <a class="existingWikiWord" href="/nlab/show/material+set+theory">material set theory</a> that are needed for ordinary mathematics. The <a class="existingWikiWord" href="/nlab/show/structural+set+theory">structural</a> analogue is a <a class="existingWikiWord" href="/nlab/show/universe+in+the+topos">universe in the 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>.</p> <p>In general, we need some axioms to state the existence of such universes; we can think of these as <a class="existingWikiWord" href="/nlab/show/large+cardinal">large cardinal</a> axioms. (The existence of an infinite set is the <a class="existingWikiWord" href="/nlab/show/axiom+of+infinity">axiom of infinity</a>; the existence of a Grothendieck universe is the existence of an <a class="existingWikiWord" href="/nlab/show/inaccessible+cardinal">inaccessible cardinal</a>.)</p> <p>The use of such universes is convenient when we want to work with <a class="existingWikiWord" href="/nlab/show/large+categories">large categories</a> “as if they were small.” That is, if we redefine “small” to mean “element of some fixed universe,” then the categories of all small structures of some sort will still be sets (rather than <a class="existingWikiWord" href="/nlab/show/proper+classes">proper classes</a>) in the bigger ambient universe, and thus we can for instance form <a class="existingWikiWord" href="/nlab/show/functor+categories">functor categories</a> between them freely. We do sometimes then need a way to “move a category” from one universe to another; see <a class="existingWikiWord" href="/nlab/show/universe+enlargement">universe enlargement</a>.</p> <h2 id="reflection">Reflection</h2> <p>In <a class="existingWikiWord" href="/nlab/show/logic">logic</a>, we use <a class="existingWikiWord" href="/nlab/show/reflection+principle">reflection principle</a>s (see <a href="https://secure.wikimedia.org/wikipedia/en/wiki/Reflection_principle">Wikipedia</a>) to systematically identify features of our meta-universe and see what is needed to prove the existence of an internal universe with these features.</p> <p>This follows the following outline:</p> <ol> <li> <p>We assume that we understand <em>a priori</em> what it means to use <a class="existingWikiWord" href="/nlab/show/first-order+logic">first-order logic</a> (or some other finitary base logic).</p> </li> <li> <p>Using this base logic, we can formulate a foundational <a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a> that describes a meta-universe such as <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> </li> <li> <p>Of course, <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> cannot be described from inside itself. But there may be objects 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> (<a class="existingWikiWord" href="/nlab/show/internal+categories">internal categories</a>) that <em>look like</em> <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.</p> </li> <li> <p>We add an additional axiom to our set theory stating that such objects, the <em>internal universes</em>, exist. These are then <a class="existingWikiWord" href="/nlab/show/models">models</a> of our original set theory.</p> </li> <li> <p>Now we are using a new, stronger set theory; repeat.</p> </li> </ol> <h2 id="universes_in_type_theory">Universes in type theory</h2> <p>Set theory is not the only <a class="existingWikiWord" href="/nlab/show/foundation+of+mathematics">foundation of mathematics</a>. For example, there are also various foundational <a class="existingWikiWord" href="/nlab/show/type+theories">type theories</a>, closely related to <a class="existingWikiWord" href="/nlab/show/structural+set+theory">structural set theory</a>. Then we have a meta-universe of all types, and we can also add axioms for the existence of internal <a class="existingWikiWord" href="/nlab/show/type+universes">type universes</a>.</p> <h2 id="related_concepts">Related concepts</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/constructible+universe">constructible universe</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/universe+enlargement">universe enlargement</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/universe+polymorphism">universe polymorphism</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/type+of+types">type of types</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/subobject+classifier">subobject classifier</a>, <a class="existingWikiWord" href="/nlab/show/object+classifier">object classifier</a>, <a class="existingWikiWord" href="/nlab/show/partial+map+classifier">partial map classifier</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/reflective+subuniverse">reflective subuniverse</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/G-universe">G-universe</a></p> </li> </ul> <h2 id="references">References</h2> <h3 id="general">General</h3> <p>For universes in <a class="existingWikiWord" href="/nlab/show/class+theory">class theory</a> and <a class="existingWikiWord" href="/nlab/show/algebraic+set+theory">algebraic set theory</a>, see</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Steve+Awodey">Steve Awodey</a>. <em>Notes on algebraic set theory</em>, Notes for lectures given at the Summer School on Topos Theory, Haute-Bodeux, Belgium. May 29 to June 5, 2005. Carnegie Mellon University Technical Report No. CMU-PHIL-170. June 2005. (<a href="https://www.phil.cmu.edu/projects/ast/Papers/bnotes.pdf">pdf</a>)</li> </ul> <h3 id="in_type_theory">In type theory</h3> <ul> <li><a class="existingWikiWord" href="/nlab/show/Martin+Hofmann">Martin Hofmann</a>, section 2.1.6 of <em>Syntax and semantics of dependent types</em> (<a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.36.8985">web</a>)</li> </ul> </body></html> </div> <div class="revisedby"> <p> Last revised on November 15, 2023 at 09:37:40. See the <a href="/nlab/history/universe" 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/universe" accesskey="E" class="navlink" id="edit" rel="nofollow">Edit</a><a href="https://nforum.ncatlab.org/discussion/2041/#Item_67">Discuss</a><span class="backintime"><a href="/nlab/revision/universe/25" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/diff/universe" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Changes from previous revision</a><a href="/nlab/history/universe" accesskey="S" class="navlink" id="history" rel="nofollow">History (25 revisions)</a> <a href="/nlab/show/universe/cite" style="color: black">Cite</a> <a href="/nlab/print/universe" accesskey="p" id="view_print" rel="nofollow">Print</a> <a href="/nlab/source/universe" id="view_source" rel="nofollow">Source</a> </div> </div>  </div>  </body> </html>