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> class 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> class </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/8919/#Item_26" 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></title></head> <body> <div class="rightHandSide"> <div class="toc clickDown" tabindex="0"> <h3 id="context">Context</h3> <h4 id="foundations">Foundations</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/foundations">foundations</a></strong></p> <h2 id="the_basis_of_it_all">The basis of it all</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/mathematical+logic">mathematical logic</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/deduction+system">deduction system</a>, <a class="existingWikiWord" href="/nlab/show/natural+deduction">natural deduction</a>, <a class="existingWikiWord" href="/nlab/show/sequent+calculus">sequent calculus</a>, <a class="existingWikiWord" href="/nlab/show/lambda-calculus">lambda-calculus</a>, <a class="existingWikiWord" href="/nlab/show/judgment">judgment</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a>, <a class="existingWikiWord" href="/nlab/show/simple+type+theory">simple type theory</a>, <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/collection">collection</a>, <a class="existingWikiWord" href="/nlab/show/object">object</a>, <a class="existingWikiWord" href="/nlab/show/type">type</a>, <a class="existingWikiWord" href="/nlab/show/term">term</a>, <a class="existingWikiWord" href="/nlab/show/set">set</a>, <a class="existingWikiWord" href="/nlab/show/element">element</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/equality">equality</a>, <a class="existingWikiWord" href="/nlab/show/judgmental+equality">judgmental equality</a>, <a class="existingWikiWord" href="/nlab/show/typal+equality">typal equality</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/universe">universe</a>, <a class="existingWikiWord" href="/nlab/show/size+issues">size issues</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/higher-order+logic">higher-order logic</a></p> </li> </ul> <h2 id="set_theory"> Set theory</h2> <div> <p><strong><a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a></strong></p> <ul> <li>fundamentals of set theory <ul> <li><a class="existingWikiWord" href="/nlab/show/propositional+logic">propositional logic</a></li> <li><a class="existingWikiWord" href="/nlab/show/first-order+logic">first-order logic</a></li> <li><a class="existingWikiWord" href="/nlab/show/typed+predicate+logic">typed predicate logic</a></li> <li><a class="existingWikiWord" href="/nlab/show/membership+relation">membership relation</a></li> <li><a class="existingWikiWord" href="/nlab/show/propositional+equality">propositional equality</a></li> <li><a class="existingWikiWord" href="/nlab/show/set">set</a>, <a class="existingWikiWord" href="/nlab/show/element">element</a>, <a class="existingWikiWord" href="/nlab/show/function">function</a>, <a class="existingWikiWord" href="/nlab/show/relation">relation</a></li> <li><a class="existingWikiWord" href="/nlab/show/universe">universe</a>, <a class="existingWikiWord" href="/nlab/show/small+set">small set</a>, <a class="existingWikiWord" href="/nlab/show/large+set">large set</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/material+set+theory">material set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/membership+relation">membership relation</a>, <a class="existingWikiWord" href="/nlab/show/propositional+equality">propositional equality</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+extensionality">axiom of extensionality</a></li> <li><a class="existingWikiWord" href="/nlab/show/pairing+structure">pairing structure</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+pairing">axiom of pairing</a></li> <li><a class="existingWikiWord" href="/nlab/show/union+structure">union structure</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+union">axiom of union</a></li> <li><a class="existingWikiWord" href="/nlab/show/powerset+structure">powerset structure</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+power+sets">axiom of power sets</a></li> <li><a class="existingWikiWord" href="/nlab/show/natural+numbers+structure">natural numbers structure</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+infinity">axiom of infinity</a></li> </ul> </li> <li>presentations of set theory <ul> <li><a class="existingWikiWord" href="/nlab/show/first-order+set+theory">first-order set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/unsorted+set+theory">unsorted set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/simply+sorted+set+theory">simply sorted set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/one-sorted+set+theory">one-sorted set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/two-sorted+set+theory">two-sorted set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/three-sorted+set+theory">three-sorted set theory</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/dependently+sorted+set+theory">dependently sorted set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/structurally+presented+set+theory">structurally presented set theory</a></li> </ul> </li> <li>structuralism in set theory <ul> <li><a class="existingWikiWord" href="/nlab/show/material+set+theory">material set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/ZFC">ZFC</a></li> <li><a class="existingWikiWord" href="/nlab/show/ZFA">ZFA</a></li> <li><a class="existingWikiWord" href="/nlab/show/Mostowski+set+theory">Mostowski set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/New+Foundations">New Foundations</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/structural+set+theory">structural set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/categorical+set+theory">categorical set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/ETCS">ETCS</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/fully+formal+ETCS">fully formal ETCS</a></li> <li><a class="existingWikiWord" href="/nlab/show/ETCS+with+elements">ETCS with elements</a></li> <li><a class="existingWikiWord" href="/nlab/show/Trimble+on+ETCS+I">Trimble on ETCS I</a></li> <li><a class="existingWikiWord" href="/nlab/show/Trimble+on+ETCS+II">Trimble on ETCS II</a></li> <li><a class="existingWikiWord" href="/nlab/show/Trimble+on+ETCS+III">Trimble on ETCS III</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/structural+ZFC">structural ZFC</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/allegorical+set+theory">allegorical set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/SEAR">SEAR</a></li> </ul> </li> </ul> </li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/class-set+theory">class-set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/class">class</a>, <a class="existingWikiWord" href="/nlab/show/proper+class">proper class</a></li> <li><a class="existingWikiWord" href="/nlab/show/universal+class">universal class</a>, <a class="existingWikiWord" href="/nlab/show/universe">universe</a></li> <li><a class="existingWikiWord" href="/nlab/show/category+of+classes">category of classes</a></li> <li><a class="existingWikiWord" href="/nlab/show/category+with+class+structure">category with class structure</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/constructive+set+theory">constructive set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/algebraic+set+theory">algebraic set theory</a></li> </ul> </div> <h2 id="foundational_axioms">Foundational axioms</h2> <div> <p><strong><a class="existingWikiWord" href="/nlab/show/foundational+axiom">foundational</a> <a class="existingWikiWord" href="/nlab/show/axioms">axioms</a></strong></p> <ul> <li> <p>basic constructions:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+cartesian+products">axiom of cartesian products</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+disjoint+unions">axiom of disjoint unions</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+the+empty+set">axiom of the empty set</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+fullness">axiom of fullness</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+function+sets">axiom of function sets</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+power+sets">axiom of power sets</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+quotient+sets">axiom of quotient sets</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/material+set+theory">material axioms</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+extensionality">axiom of extensionality</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+foundation">axiom of foundation</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+anti-foundation">axiom of anti-foundation</a></li> <li><a class="existingWikiWord" href="/nlab/show/Mostowski%27s+axiom">Mostowski's axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+pairing">axiom of pairing</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+transitive+closure">axiom of transitive closure</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+union">axiom of union</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/structural+set+theory">structural axioms</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+materialization">axiom of materialization</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/type+theory">type theoretic axioms</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axioms+of+set+truncation">axioms of set truncation</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/uniqueness+of+identity+proofs">uniqueness of identity proofs</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+K">axiom K</a></li> <li><a class="existingWikiWord" href="/nlab/show/boundary+separation">boundary separation</a></li> <li><a class="existingWikiWord" href="/nlab/show/equality+reflection">equality reflection</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+circle+type+localization">axiom of circle type localization</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theoretic axioms</a>: <ul> <li><a class="existingWikiWord" href="/nlab/show/univalence+axiom">univalence axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/Whitehead%27s+principle">Whitehead's principle</a></li> </ul> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/axioms+of+choice">axioms of choice</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+countable+choice">axiom of countable choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+dependent+choice">axiom of dependent choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+excluded+middle">axiom of excluded middle</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+existence">axiom of existence</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+multiple+choice">axiom of multiple choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/Markov%27s+axiom">Markov's axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/presentation+axiom">presentation axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/small+cardinality+selection+axiom">small cardinality selection axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+small+violations+of+choice">axiom of small violations of choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+weakly+initial+sets+of+covers">axiom of weakly initial sets of covers</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/large+cardinal+axioms">large cardinal axioms</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+infinity">axiom of infinity</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+universes">axiom of universes</a></li> <li><a class="existingWikiWord" href="/nlab/show/regular+extension+axiom">regular extension axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/inaccessible+cardinal">inaccessible cardinal</a></li> <li><a class="existingWikiWord" href="/nlab/show/measurable+cardinal">measurable cardinal</a></li> <li><a class="existingWikiWord" href="/nlab/show/elementary+embedding">elementary embedding</a></li> <li><a class="existingWikiWord" href="/nlab/show/supercompact+cardinal">supercompact cardinal</a></li> <li><a class="existingWikiWord" href="/nlab/show/Vop%C4%9Bnka%27s+principle">Vopěnka's principle</a></li> </ul> </li> <li> <p>strong axioms</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+separation">axiom of separation</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+replacement">axiom of replacement</a></li> </ul> </li> <li> <p>further</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/reflection+principle">reflection principle</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/axiom+of+tight+apartness">axiom of tight apartness</a></p> </li> </ul> </div> <h2 id="removing_axioms">Removing axioms</h2> <ul> <li><a class="existingWikiWord" href="/nlab/show/constructive+mathematics">constructive mathematics</a></li> <li><a class="existingWikiWord" href="/nlab/show/predicative+mathematics">predicative mathematics</a></li> </ul> <div> <p> <a href="/nlab/edit/foundations+-+contents">Edit this sidebar</a> </p> </div></div></div> <h4 id="type_theory">Type theory</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/natural+deduction">natural deduction</a></strong> <a class="existingWikiWord" href="/nlab/show/metalanguage">metalanguage</a>, <a class="existingWikiWord" href="/nlab/show/practical+foundations">practical foundations</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/judgement">judgement</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/hypothetical+judgement">hypothetical judgement</a>, <a class="existingWikiWord" href="/nlab/show/sequent">sequent</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/antecedents">antecedents</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊢</mo></mrow><annotation encoding="application/x-tex">\vdash</annotation></semantics></math> <a class="existingWikiWord" href="/nlab/show/consequent">consequent</a>, <a class="existingWikiWord" href="/nlab/show/succedents">succedents</a></li> </ul> </li> </ul> <ol> <li><a class="existingWikiWord" href="/nlab/show/type+formation+rule">type formation rule</a></li> <li><a class="existingWikiWord" href="/nlab/show/term+introduction+rule">term introduction rule</a></li> <li><a class="existingWikiWord" href="/nlab/show/term+elimination+rule">term elimination rule</a></li> <li><a class="existingWikiWord" href="/nlab/show/computation+rule">computation rule</a></li> </ol> <p><strong><a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a></strong> (<a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent</a>, <a class="existingWikiWord" href="/nlab/show/intensional+type+theory">intensional</a>, <a class="existingWikiWord" href="/nlab/show/observational+type+theory">observational type theory</a>, <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a>)</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/calculus+of+constructions">calculus of constructions</a></li> </ul> <p><strong><a class="existingWikiWord" href="/nlab/show/syntax">syntax</a></strong> <a class="existingWikiWord" href="/nlab/show/object+language">object language</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/theory">theory</a>, <a class="existingWikiWord" href="/nlab/show/axiom">axiom</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/proposition">proposition</a>/<a class="existingWikiWord" href="/nlab/show/type">type</a> (<a class="existingWikiWord" href="/nlab/show/propositions+as+types">propositions as types</a>)</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/definition">definition</a>/<a class="existingWikiWord" href="/nlab/show/proof">proof</a>/<a class="existingWikiWord" href="/nlab/show/program">program</a> (<a class="existingWikiWord" href="/nlab/show/proofs+as+programs">proofs as programs</a>)</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/theorem">theorem</a></p> </li> </ul> <div> <p><strong><a class="existingWikiWord" href="/nlab/show/computational+trinitarianism">computational trinitarianism</a></strong> = <br /> <strong><a class="existingWikiWord" href="/nlab/show/propositions+as+types">propositions as types</a></strong> +<strong><a class="existingWikiWord" href="/nlab/show/programs+as+proofs">programs as proofs</a></strong> +<strong><a class="existingWikiWord" href="/nlab/show/relation+between+type+theory+and+category+theory">relation type theory/category theory</a></strong></p> <table><thead><tr><th><a class="existingWikiWord" href="/nlab/show/logic">logic</a></th><th><a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a> (<a class="existingWikiWord" href="/nlab/show/internal+logic+of+set+theory">internal logic</a> of)</th><th><a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a></th><th><a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a></th></tr></thead><tbody><tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/proposition">proposition</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/set">set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/object">object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/type">type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/predicate">predicate</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/family+of+sets">family of sets</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/display+morphism">display morphism</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/dependent+type">dependent type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/proof">proof</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/element">element</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/generalized+element">generalized element</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/term">term</a>/<a class="existingWikiWord" href="/nlab/show/program">program</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/cut+rule">cut rule</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/composition">composition</a> of <a class="existingWikiWord" href="/nlab/show/classifying+morphisms">classifying morphisms</a> / <a class="existingWikiWord" href="/nlab/show/pullback">pullback</a> of <a class="existingWikiWord" href="/nlab/show/display+maps">display maps</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/substitution">substitution</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/introduction+rule">introduction rule</a> for <a class="existingWikiWord" href="/nlab/show/implication">implication</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/counit">counit</a> for hom-tensor adjunction</td><td style="text-align: left;">lambda</td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/elimination+rule">elimination rule</a> for <a class="existingWikiWord" href="/nlab/show/implication">implication</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/unit">unit</a> for hom-tensor adjunction</td><td style="text-align: left;">application</td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/cut+elimination">cut elimination</a> for <a class="existingWikiWord" href="/nlab/show/implication">implication</a></td><td style="text-align: left;"></td><td style="text-align: left;">one of the <a class="existingWikiWord" href="/nlab/show/zigzag+identities">zigzag identities</a> for hom-tensor adjunction</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/beta+reduction">beta reduction</a></td></tr> <tr><td style="text-align: left;">identity elimination for <a class="existingWikiWord" href="/nlab/show/implication">implication</a></td><td style="text-align: left;"></td><td style="text-align: left;">the other <a class="existingWikiWord" href="/nlab/show/zigzag+identity">zigzag identity</a> for hom-tensor adjunction</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/eta+conversion">eta conversion</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/true">true</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/singleton">singleton</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/terminal+object">terminal object</a>/<a class="existingWikiWord" href="/nlab/show/%28-2%29-truncated+object">(-2)-truncated object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/h-level+0">h-level 0</a>-<a class="existingWikiWord" href="/nlab/show/type">type</a>/<a class="existingWikiWord" href="/nlab/show/unit+type">unit type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/false">false</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/empty+set">empty set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/initial+object">initial object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/empty+type">empty type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/proposition">proposition</a>, <a class="existingWikiWord" href="/nlab/show/truth+value">truth value</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/subsingleton">subsingleton</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/subterminal+object">subterminal object</a>/<a class="existingWikiWord" href="/nlab/show/%28-1%29-truncated+object">(-1)-truncated object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/h-proposition">h-proposition</a>, <a class="existingWikiWord" href="/nlab/show/mere+proposition">mere proposition</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/logical+conjunction">logical conjunction</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/cartesian+product">cartesian product</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/product">product</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/product+type">product type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/disjunction">disjunction</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/disjoint+union">disjoint union</a> (<a class="existingWikiWord" href="/nlab/show/support">support</a> of)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/coproduct">coproduct</a> (<a class="existingWikiWord" href="/nlab/show/%28-1%29-truncation">(-1)-truncation</a> of)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/sum+type">sum type</a> (<a class="existingWikiWord" href="/nlab/show/bracket+type">bracket type</a> of)</td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/implication">implication</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/function+set">function set</a> (into <a class="existingWikiWord" href="/nlab/show/subsingleton">subsingleton</a>)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/internal+hom">internal hom</a> (into <a class="existingWikiWord" href="/nlab/show/subterminal+object">subterminal object</a>)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/function+type">function type</a> (into <a class="existingWikiWord" href="/nlab/show/h-proposition">h-proposition</a>)</td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/negation">negation</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/function+set">function set</a> into <a class="existingWikiWord" href="/nlab/show/empty+set">empty set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/internal+hom">internal hom</a> into <a class="existingWikiWord" href="/nlab/show/initial+object">initial object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/function+type">function type</a> into <a class="existingWikiWord" href="/nlab/show/empty+type">empty type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/universal+quantification">universal quantification</a></td><td style="text-align: left;">indexed <a class="existingWikiWord" href="/nlab/show/cartesian+product">cartesian product</a> (of family of <a class="existingWikiWord" href="/nlab/show/subsingletons">subsingletons</a>)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/dependent+product">dependent product</a> (of family of <a class="existingWikiWord" href="/nlab/show/subterminal+objects">subterminal objects</a>)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/dependent+product+type">dependent product type</a> (of family of <a class="existingWikiWord" href="/nlab/show/h-propositions">h-propositions</a>)</td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/existential+quantification">existential quantification</a></td><td style="text-align: left;">indexed <a class="existingWikiWord" href="/nlab/show/disjoint+union">disjoint union</a> (<a class="existingWikiWord" href="/nlab/show/support">support</a> of)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/dependent+sum">dependent sum</a> (<a class="existingWikiWord" href="/nlab/show/%28-1%29-truncation">(-1)-truncation</a> of)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/dependent+sum+type">dependent sum type</a> (<a class="existingWikiWord" href="/nlab/show/bracket+type">bracket type</a> of)</td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/logical+equivalence">logical equivalence</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/bijection+set">bijection set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/object+of+isomorphisms">object of isomorphisms</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/equivalence+type">equivalence type</a></td></tr> <tr><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/support+set">support set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/support+object">support object</a>/<a class="existingWikiWord" href="/nlab/show/%28-1%29-truncation">(-1)-truncation</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/propositional+truncation">propositional truncation</a>/<a class="existingWikiWord" href="/nlab/show/bracket+type">bracket type</a></td></tr> <tr><td style="text-align: left;"></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/n-image">n-image</a> of <a class="existingWikiWord" href="/nlab/show/morphism">morphism</a> into <a class="existingWikiWord" href="/nlab/show/terminal+object">terminal object</a>/<a class="existingWikiWord" href="/nlab/show/n-truncation">n-truncation</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/n-truncation+modality">n-truncation modality</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/equality">equality</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/diagonal+function">diagonal function</a>/<a class="existingWikiWord" href="/nlab/show/diagonal+subset">diagonal subset</a>/<a class="existingWikiWord" href="/nlab/show/diagonal+relation">diagonal relation</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/path+space+object">path space object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/identity+type">identity type</a>/<a class="existingWikiWord" href="/nlab/show/path+type">path type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/completely+presented+set">completely presented set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/set">set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/discrete+object">discrete object</a>/<a class="existingWikiWord" href="/nlab/show/0-truncated+object">0-truncated object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/h-level+2">h-level 2</a>-<a class="existingWikiWord" href="/nlab/show/type">type</a>/<a class="existingWikiWord" href="/nlab/show/set">set</a>/<a class="existingWikiWord" href="/nlab/show/h-set">h-set</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/set">set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/set">set</a> with <a class="existingWikiWord" href="/nlab/show/equivalence+relation">equivalence relation</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/groupoid+object+in+an+%28infinity%2C1%29-category">internal 0-groupoid</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/Bishop+set">Bishop set</a>/<a class="existingWikiWord" href="/nlab/show/setoid">setoid</a> with its <a class="existingWikiWord" href="/nlab/show/pseudo-equivalence+relation">pseudo-equivalence relation</a> an actual <a class="existingWikiWord" href="/nlab/show/equivalence+relation">equivalence relation</a></td></tr> <tr><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/equivalence+class">equivalence class</a>/<a class="existingWikiWord" href="/nlab/show/quotient+set">quotient set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/quotient">quotient</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/quotient+type">quotient type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/induction">induction</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/colimit">colimit</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/inductive+type">inductive type</a>, <a class="existingWikiWord" href="/nlab/show/W-type">W-type</a>, <a class="existingWikiWord" href="/nlab/show/M-type">M-type</a></td></tr> <tr><td style="text-align: left;">higher <a class="existingWikiWord" href="/nlab/show/induction">induction</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/%28infinity%2C1%29-colimit">higher colimit</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/higher+inductive+type">higher inductive type</a></td></tr> <tr><td style="text-align: left;">-</td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/0-truncated">0-truncated</a> <a class="existingWikiWord" href="/nlab/show/%28infinity%2C1%29-colimit">higher colimit</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/quotient+inductive+type">quotient inductive type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/coinduction">coinduction</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/limit">limit</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/coinductive+type">coinductive type</a></td></tr> <tr><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/preset">preset</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/type">type</a> without <a class="existingWikiWord" href="/nlab/show/identity+types">identity types</a></td></tr> <tr><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/set">set</a> of <a class="existingWikiWord" href="/nlab/show/truth+values">truth values</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/subobject+classifier">subobject classifier</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/type+of+propositions">type of propositions</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/domain+of+discourse">domain of discourse</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/universe">universe</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/object+classifier">object classifier</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/type+universe">type universe</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/modality">modality</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/closure+operator">closure operator</a>, (<a class="existingWikiWord" href="/nlab/show/idempotent+monad">idempotent</a>) <a class="existingWikiWord" href="/nlab/show/monad">monad</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/modal+type+theory">modal type theory</a>, <a class="existingWikiWord" href="/nlab/show/monad+%28in+computer+science%29">monad (in computer science)</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/linear+logic">linear logic</a></td><td style="text-align: left;"></td><td style="text-align: left;">(<a class="existingWikiWord" href="/nlab/show/symmetric+monoidal+category">symmetric</a>, <a class="existingWikiWord" href="/nlab/show/closed+monoidal+category">closed</a>) <a class="existingWikiWord" href="/nlab/show/monoidal+category">monoidal category</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/linear+type+theory">linear type theory</a>/<a class="existingWikiWord" href="/nlab/show/quantum+computation">quantum computation</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/proof+net">proof net</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/string+diagram">string diagram</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/quantum+circuit">quantum circuit</a></td></tr> <tr><td style="text-align: left;">(absence of) <a class="existingWikiWord" href="/nlab/show/contraction+rule">contraction rule</a></td><td style="text-align: left;"></td><td style="text-align: left;">(absence of) <a class="existingWikiWord" href="/nlab/show/diagonal">diagonal</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/no-cloning+theorem">no-cloning theorem</a></td></tr> <tr><td style="text-align: left;"></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/synthetic+mathematics">synthetic mathematics</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/domain+specific+embedded+programming+language">domain specific embedded programming language</a></td></tr> </tbody></table> </div> <p><strong><a class="existingWikiWord" href="/nlab/show/homotopy+levels">homotopy levels</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/2-type+theory">2-type theory</a>, <a class="existingWikiWord" href="/michaelshulman/show/2-categorical+logic">2-categorical logic</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a>, <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory+-+contents">homotopy type theory - contents</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/homotopy+type">homotopy type</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/univalence">univalence</a>, <a class="existingWikiWord" href="/nlab/show/function+extensionality">function extensionality</a>, <a class="existingWikiWord" href="/nlab/show/internal+logic+of+an+%28%E2%88%9E%2C1%29-topos">internal logic of an (∞,1)-topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/cohesive+homotopy+type+theory">cohesive homotopy type theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/directed+homotopy+type+theory">directed homotopy type theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/HoTT+methods+for+homotopy+theorists">HoTT methods for homotopy theorists</a></p> </li> </ul> </li> </ul> <p><strong><a class="existingWikiWord" href="/nlab/show/semantics">semantics</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/internal+logic">internal logic</a>, <a class="existingWikiWord" href="/nlab/show/categorical+semantics">categorical semantics</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/display+map">display map</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/internal+logic+of+a+topos">internal logic of a topos</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Mitchell-Benabou+language">Mitchell-Benabou language</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Kripke-Joyal+semantics">Kripke-Joyal semantics</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/internal+logic+of+an+%28%E2%88%9E%2C1%29-topos">internal logic of an (∞,1)-topos</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/type-theoretic+model+category">type-theoretic model category</a></li> </ul> </li> </ul> <div> <p> <a href="/nlab/edit/type+theory+-+contents">Edit this sidebar</a> </p> </div></div></div> <h4 id="modalities_closure_and_reflection">Modalities, Closure and Reflection</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/modal+type+theory">modal type theory</a></strong>, <a class="existingWikiWord" href="/nlab/show/modal+logic">modal logic</a></p> <p><strong><a class="existingWikiWord" href="/nlab/show/closure+operator">closure operator</a></strong>, <a class="existingWikiWord" href="/nlab/show/universal+closure+operator">universal closure operator</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/idempotent+monad">idempotent monad</a>, <a class="existingWikiWord" href="/nlab/show/comonad">comonad</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/modal+type">modal type</a>, <a class="existingWikiWord" href="/nlab/show/local+object">local object</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/reflective+subcategory">reflective subcategory</a>, <a class="existingWikiWord" href="/nlab/show/coreflective+subcategory">coreflective subcategory</a></p> </li> </ul> <p><strong>Examples</strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Moore+closure">Moore closure</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/geometric+modality">geometric modality</a>/<a class="existingWikiWord" href="/nlab/show/Lawvere-Tierney+topology">Lawvere-Tierney topology</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/S4+modal+logic">S4 modal logic</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/n-truncated+object+in+an+%28infinity%2C1%29-category">n-truncation</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/shape+modality">shape modality</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊣</mo></mrow><annotation encoding="application/x-tex">\dashv</annotation></semantics></math> <a class="existingWikiWord" href="/nlab/show/flat+modality">flat modality</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊣</mo></mrow><annotation encoding="application/x-tex">\dashv</annotation></semantics></math> <a class="existingWikiWord" href="/nlab/show/sharp+modality">sharp modality</a></p> </li> </ul> </div></div> </div> </div> <h1 id='section_table_of_contents'>Contents</h1> <div class='maruku_toc'> <ul> <li><a href='#idea'>Idea</a></li> <li><a href='#definitions'>Definitions</a></li> <li><a href='#examples'>Examples</a></li> <li><a href='#internal_classes'>Internal classes</a></li> <ul> <li><a href='#classes_as_primitive'>Classes as primitive</a></li> <li><a href='#classes_as_derived_from_universes'>Classes as derived from universes</a></li> <ul> <li><a href='#in_set_theory'>In set theory</a></li> <li><a href='#in_dependent_type_theory'>In dependent type theory</a></li> </ul> <li><a href='#proper_classes'>Proper classes</a></li> </ul> <li><a href='#category_of_classes'>Category of classes</a></li> <li><a href='#see_also'> See also</a></li> <li><a href='#references'>References</a></li> </ul> </div> <h2 id="idea">Idea</h2> <p>In <a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a>, a class is a <a class="existingWikiWord" href="/nlab/show/proposition">proposition</a> or <a class="existingWikiWord" href="/nlab/show/truth+value">truth value</a> in the <a class="existingWikiWord" href="/nlab/show/context">context</a> of a <a class="existingWikiWord" href="/nlab/show/set">set</a> <a class="existingWikiWord" href="/nlab/show/free+variable">free variable</a>. In <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a> with a <a class="existingWikiWord" href="/nlab/show/type+universe">type universe</a> <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>, a class is an <a class="existingWikiWord" href="/nlab/show/h-proposition">h-proposition</a> in the context of a <a class="existingWikiWord" href="/nlab/show/free+variable">free variable</a> <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:U</annotation></semantics></math>.</p> <p>In <a class="existingWikiWord" href="/nlab/show/set-level+type+theory">set-level</a> <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a> with a separate <a class="existingWikiWord" href="/nlab/show/set">set</a> or <a class="existingWikiWord" href="/nlab/show/type">type</a> <a class="existingWikiWord" href="/nlab/show/judgment">judgment</a> but no <a class="existingWikiWord" href="/nlab/show/type+universes">type universes</a>, there are no <a class="existingWikiWord" href="/nlab/show/set">set</a>/<a class="existingWikiWord" href="/nlab/show/type">type</a> free variables. However, one could nevertheless interpret a class in <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a> as a generalized <a class="existingWikiWord" href="/nlab/show/modal+operator">modal operator</a> on <a class="existingWikiWord" href="/nlab/show/sets">sets</a>/<a class="existingWikiWord" href="/nlab/show/types">types</a> which takes sets to <a class="existingWikiWord" href="/nlab/show/h-propositions">h-propositions</a> by the <a class="existingWikiWord" href="/nlab/show/propositions+as+some+types">propositions as some types</a> interpretation. If we use the <a class="existingWikiWord" href="/nlab/show/propositions+as+types">propositions as types</a> interpretation of <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a>, then a class in any <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a> is just a generalized <a class="existingWikiWord" href="/nlab/show/modal+operator">modal operator</a> on <a class="existingWikiWord" href="/nlab/show/sets">sets</a>/<a class="existingWikiWord" href="/nlab/show/types">types</a>. The generalized modal operators here are not required to be either <a class="existingWikiWord" href="/nlab/show/idempotent">idempotent</a> or <a class="existingWikiWord" href="/nlab/show/monadic">monadic</a>.</p> <p>One could internalize the notion of class inside of the foundations, and this internal notion of class is used to address size issues in foundations, and in particular, are used in <a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a> for defining various <a class="existingWikiWord" href="/nlab/show/locally+small+categories">locally small categories</a> and <a class="existingWikiWord" href="/nlab/show/large+categories">large categories</a>.</p> <h2 id="definitions">Definitions</h2> <p>There are multiple ways to define a class in different <a class="existingWikiWord" href="/nlab/show/foundations+of+mathematics">foundations of mathematics</a>. Let us work in <a class="existingWikiWord" href="/nlab/show/natural+deduction">natural deduction</a>.</p> <ul> <li> <p>Suppose we are given an <a class="existingWikiWord" href="/nlab/show/unsorted+set+theory">unsorted set theory</a> as <a class="existingWikiWord" href="/nlab/show/logic+over+type+theory">logic over type theory</a> whose objects are <a class="existingWikiWord" href="/nlab/show/sets">sets</a>. A <strong>class</strong> <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> is a <a class="existingWikiWord" href="/nlab/show/proposition">proposition</a> or <a class="existingWikiWord" href="/nlab/show/truth+value">truth value</a> in the <a class="existingWikiWord" href="/nlab/show/context">context</a> of a <a class="existingWikiWord" href="/nlab/show/free+variable">free variable</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>.</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>,</mo><mi>A</mi><mo stretchy="false">|</mo><mi>Φ</mi><mo>⊢</mo><mi>C</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">prop</mi></mrow><annotation encoding="application/x-tex">\Gamma, A \vert \Phi \vdash C \; \mathrm{prop}</annotation></semantics></math></div></li> <li> <p>Suppose we are given a <a class="existingWikiWord" href="/nlab/show/simply+sorted+set+theory">simply sorted set theory</a> or <a class="existingWikiWord" href="/nlab/show/dependently+sorted+set+theory">dependently sorted set theory</a> as <a class="existingWikiWord" href="/nlab/show/logic+over+type+theory">logic over type theory</a> with a <a class="existingWikiWord" href="/nlab/show/sort">sort</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">Set</mi></mrow><annotation encoding="application/x-tex">\mathrm{Set}</annotation></semantics></math> of <a class="existingWikiWord" href="/nlab/show/sets">sets</a>. A <strong>class</strong> <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> is a <a class="existingWikiWord" href="/nlab/show/proposition">proposition</a> or <a class="existingWikiWord" href="/nlab/show/truth+value">truth value</a> in the <a class="existingWikiWord" href="/nlab/show/context">context</a> of a <a class="existingWikiWord" href="/nlab/show/free+variable">free variable</a> for a set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>:</mo><mi mathvariant="normal">Set</mi></mrow><annotation encoding="application/x-tex">A:\mathrm{Set}</annotation></semantics></math>.</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>,</mo><mi>A</mi><mo>:</mo><mi mathvariant="normal">Set</mi><mo stretchy="false">|</mo><mi>Φ</mi><mo>⊢</mo><mi>C</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">prop</mi></mrow><annotation encoding="application/x-tex">\Gamma, A:\mathrm{Set} \vert \Phi \vdash C \; \mathrm{prop}</annotation></semantics></math></div></li> <li> <p>Suppose we are given an <a class="existingWikiWord" href="/nlab/show/unsorted+set+theory">unsorted set theory</a> as <a class="existingWikiWord" href="/nlab/show/logic+over+type+theory">logic over type theory</a> whose objects are “probable sets”, with a <a class="existingWikiWord" href="/nlab/show/predicate">predicate</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">isSet</mi><mo stretchy="false">(</mo><mi>A</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathrm{isSet}(A)</annotation></semantics></math> saying whether a “probable set” <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> is a set. A <strong>class</strong> <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> is a <a class="existingWikiWord" href="/nlab/show/proposition">proposition</a> or <a class="existingWikiWord" href="/nlab/show/truth+value">truth value</a> in the <a class="existingWikiWord" href="/nlab/show/context">context</a> of a <a class="existingWikiWord" href="/nlab/show/free+variable">free variable</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> and the true proposition <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">isSet</mi><mo stretchy="false">(</mo><mi>A</mi><mo stretchy="false">)</mo><mspace width="thickmathspace"></mspace><mi mathvariant="normal">true</mi></mrow><annotation encoding="application/x-tex">\mathrm{isSet}(A) \; \mathrm{true}</annotation></semantics></math>.</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>,</mo><mi>A</mi><mo stretchy="false">|</mo><mi>Φ</mi><mo>,</mo><mi mathvariant="normal">isSet</mi><mo stretchy="false">(</mo><mi>A</mi><mo stretchy="false">)</mo><mspace width="thickmathspace"></mspace><mi mathvariant="normal">true</mi><mo>⊢</mo><mi>C</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">prop</mi></mrow><annotation encoding="application/x-tex">\Gamma, A \vert \Phi, \mathrm{isSet}(A) \; \mathrm{true} \vdash C \; \mathrm{prop}</annotation></semantics></math></div></li> <li> <p>Suppose we are given a <a class="existingWikiWord" href="/nlab/show/simply+sorted+set+theory">simply sorted set theory</a> or <a class="existingWikiWord" href="/nlab/show/dependently+sorted+set+theory">dependently sorted set theory</a> as <a class="existingWikiWord" href="/nlab/show/logic+over+type+theory">logic over type theory</a> with a <a class="existingWikiWord" href="/nlab/show/sort">sort</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">ProbSet</mi></mrow><annotation encoding="application/x-tex">\mathrm{ProbSet}</annotation></semantics></math> of “probable sets” with a <a class="existingWikiWord" href="/nlab/show/predicate">predicate</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">isSet</mi><mo stretchy="false">(</mo><mi>A</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathrm{isSet}(A)</annotation></semantics></math> on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">ProbSet</mi></mrow><annotation encoding="application/x-tex">\mathrm{ProbSet}</annotation></semantics></math> saying whether a term <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>:</mo><mi mathvariant="normal">ProbSet</mi></mrow><annotation encoding="application/x-tex">A:\mathrm{ProbSet}</annotation></semantics></math> is a set. A <strong>class</strong> <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> is a <a class="existingWikiWord" href="/nlab/show/proposition">proposition</a> or <a class="existingWikiWord" href="/nlab/show/truth+value">truth value</a> in the <a class="existingWikiWord" href="/nlab/show/context">context</a> of a <a class="existingWikiWord" href="/nlab/show/free+variable">free variable</a> for a probable set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>:</mo><mi mathvariant="normal">ProbSet</mi></mrow><annotation encoding="application/x-tex">A:\mathrm{ProbSet}</annotation></semantics></math> and the true proposition <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">isSet</mi><mo stretchy="false">(</mo><mi>A</mi><mo stretchy="false">)</mo><mspace width="thickmathspace"></mspace><mi mathvariant="normal">true</mi></mrow><annotation encoding="application/x-tex">\mathrm{isSet}(A) \; \mathrm{true}</annotation></semantics></math>.</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>,</mo><mi>A</mi><mo>:</mo><mi mathvariant="normal">ProbSet</mi><mo stretchy="false">|</mo><mi>Φ</mi><mo>,</mo><mi mathvariant="normal">isSet</mi><mo stretchy="false">(</mo><mi>A</mi><mo stretchy="false">)</mo><mspace width="thickmathspace"></mspace><mi mathvariant="normal">true</mi><mo>⊢</mo><mi>C</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">prop</mi></mrow><annotation encoding="application/x-tex">\Gamma, A:\mathrm{ProbSet} \vert \Phi, \mathrm{isSet}(A) \; \mathrm{true} \vdash C \; \mathrm{prop}</annotation></semantics></math></div></li> <li> <p>Suppose we are given a <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a> with a <a class="existingWikiWord" href="/nlab/show/type+universes">type universes</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{U}</annotation></semantics></math> and a separate <a class="existingWikiWord" href="/nlab/show/type">type</a> <a class="existingWikiWord" href="/nlab/show/judgment">judgment</a>, as well as a <a class="existingWikiWord" href="/nlab/show/type+of+all+propositions">type of all propositions</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">\Omega</annotation></semantics></math>. Then a <strong>class</strong> <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> is a <a class="existingWikiWord" href="/nlab/show/proposition">proposition</a> in the <a class="existingWikiWord" href="/nlab/show/context">context</a> of a type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>:</mo><mi>𝒰</mi></mrow><annotation encoding="application/x-tex">A:\mathcal{U}</annotation></semantics></math></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>,</mo><mi>A</mi><mo>:</mo><mi>𝒰</mi><mo>⊢</mo><mi>C</mi><mo>:</mo><mi>Ω</mi></mrow><annotation encoding="application/x-tex">\Gamma, A:\mathcal{U} \vdash C:\Omega</annotation></semantics></math></div></li> <li> <p>Suppose we are given a <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a> with a <a class="existingWikiWord" href="/nlab/show/type+universes">type universes</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{U}</annotation></semantics></math> and a separate <a class="existingWikiWord" href="/nlab/show/type">type</a> <a class="existingWikiWord" href="/nlab/show/judgment">judgment</a>, and are using the <a class="existingWikiWord" href="/nlab/show/propositions+as+some+types">propositions as some types</a> interpretation of dependent type theory. Then a <strong>class</strong> <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> is a <a class="existingWikiWord" href="/nlab/show/type">type</a> in the <a class="existingWikiWord" href="/nlab/show/context">context</a> of a type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>:</mo><mi>𝒰</mi></mrow><annotation encoding="application/x-tex">A:\mathcal{U}</annotation></semantics></math></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>,</mo><mi>A</mi><mo>:</mo><mi>𝒰</mi><mo>⊢</mo><mi>C</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mrow><annotation encoding="application/x-tex">\Gamma, A:\mathcal{U} \vdash C \; \mathrm{type}</annotation></semantics></math></div> <p>with the rule</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>Γ</mi><mo>,</mo><mi>A</mi><mo>:</mo><mi>𝒰</mi><mo>⊢</mo><mi>C</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>B</mi><mo>:</mo><mi>𝒰</mi></mrow><mrow><mi>Γ</mi><mo>⊢</mo><msup><mi>p</mi> <mi>C</mi></msup><mo stretchy="false">(</mo><mi>B</mi><mo stretchy="false">)</mo><mo>:</mo><mi mathvariant="normal">isProp</mi><mo stretchy="false">(</mo><mi>C</mi><mo stretchy="false">[</mo><mi>B</mi><mo stretchy="false">/</mo><mi>A</mi><mo stretchy="false">]</mo><mo stretchy="false">)</mo></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma, A:\mathcal{U} \vdash C \; \mathrm{type} \quad \Gamma \vdash B:\mathcal{U}}{\Gamma \vdash p^C(B):\mathrm{isProp}(C[B/A])}</annotation></semantics></math></div></li> <li> <p>Suppose we are given a <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a> with a <a class="existingWikiWord" href="/nlab/show/type+universes">type universes</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{U}</annotation></semantics></math> and a separate <a class="existingWikiWord" href="/nlab/show/type">type</a> <a class="existingWikiWord" href="/nlab/show/judgment">judgment</a>, and are using the <a class="existingWikiWord" href="/nlab/show/propositions+as+types">propositions as types</a> interpretation of dependent type theory. Then a <strong>class</strong> <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> is a <a class="existingWikiWord" href="/nlab/show/type">type</a> in the <a class="existingWikiWord" href="/nlab/show/context">context</a> of a type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>:</mo><mi>𝒰</mi></mrow><annotation encoding="application/x-tex">A:\mathcal{U}</annotation></semantics></math></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>,</mo><mi>A</mi><mo>:</mo><mi>𝒰</mi><mo>⊢</mo><mi>C</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mrow><annotation encoding="application/x-tex">\Gamma, A:\mathcal{U} \vdash C \; \mathrm{type}</annotation></semantics></math></div></li> <li> <p>Suppose we are given a <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a> with a <a class="existingWikiWord" href="/nlab/show/sequence">sequence</a> of <a class="existingWikiWord" href="/nlab/show/Russell+universes">Russell universes</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>𝒰</mi> <mi>i</mi></msub></mrow><annotation encoding="application/x-tex">\mathcal{U}_i</annotation></semantics></math> but no separate <a class="existingWikiWord" href="/nlab/show/type">type</a> <a class="existingWikiWord" href="/nlab/show/judgment">judgment</a>, and are using the <a class="existingWikiWord" href="/nlab/show/propositions+as+some+types">propositions as some types</a> interpretation of dependent type theory. Then a <strong>class</strong> <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> is an <a class="existingWikiWord" href="/nlab/show/h-proposition">h-proposition</a> in the successor universe <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>𝒰</mi> <mrow><msub><mi>s</mi> <mi>𝒩</mi></msub><mo stretchy="false">(</mo><mi>i</mi><mo stretchy="false">)</mo></mrow></msub></mrow><annotation encoding="application/x-tex">\mathcal{U}_{s_\mathcal{N}(i)}</annotation></semantics></math> in the <a class="existingWikiWord" href="/nlab/show/context">context</a> of a type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>:</mo><msub><mi>𝒰</mi> <mi>i</mi></msub></mrow><annotation encoding="application/x-tex">A:\mathcal{U}_i</annotation></semantics></math></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>Ξ</mi><mo stretchy="false">|</mo><mi>Γ</mi><mo>,</mo><mi>A</mi><mo>:</mo><msub><mi>𝒰</mi> <mi>i</mi></msub><mo>⊢</mo><mi>C</mi><mo>:</mo><msub><mi mathvariant="normal">Prop</mi> <mrow><msub><mi>𝒰</mi> <mrow><msub><mi>s</mi> <mi>𝒩</mi></msub><mo stretchy="false">(</mo><mi>i</mi><mo stretchy="false">)</mo></mrow></msub></mrow></msub></mrow><annotation encoding="application/x-tex">\Xi \vert \Gamma, A:\mathcal{U}_i \vdash C:\mathrm{Prop}_{\mathcal{U}_{s_\mathcal{N}(i)}}</annotation></semantics></math></div></li> <li> <p>Suppose we are given a <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a> with a <a class="existingWikiWord" href="/nlab/show/sequence">sequence</a> of <a class="existingWikiWord" href="/nlab/show/Russell+universes">Russell universes</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>𝒰</mi> <mi>i</mi></msub></mrow><annotation encoding="application/x-tex">\mathcal{U}_i</annotation></semantics></math> but no separate <a class="existingWikiWord" href="/nlab/show/type">type</a> <a class="existingWikiWord" href="/nlab/show/judgment">judgment</a>, and are using the <a class="existingWikiWord" href="/nlab/show/propositions+as+types">propositions as types</a> interpretation of dependent type theory. Then a <strong>class</strong> <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> is a <a class="existingWikiWord" href="/nlab/show/type">type</a> in the successor universe <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>𝒰</mi> <mrow><msub><mi>s</mi> <mi>𝒩</mi></msub><mo stretchy="false">(</mo><mi>i</mi><mo stretchy="false">)</mo></mrow></msub></mrow><annotation encoding="application/x-tex">\mathcal{U}_{s_\mathcal{N}(i)}</annotation></semantics></math> in the <a class="existingWikiWord" href="/nlab/show/context">context</a> of a type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>:</mo><msub><mi>𝒰</mi> <mi>i</mi></msub></mrow><annotation encoding="application/x-tex">A:\mathcal{U}_i</annotation></semantics></math></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>Ξ</mi><mo stretchy="false">|</mo><mi>Γ</mi><mo>,</mo><mi>A</mi><mo>:</mo><msub><mi>𝒰</mi> <mi>i</mi></msub><mo>⊢</mo><mi>C</mi><mo>:</mo><msub><mi>𝒰</mi> <mrow><msub><mi>s</mi> <mi>𝒩</mi></msub><mo stretchy="false">(</mo><mi>i</mi><mo stretchy="false">)</mo></mrow></msub></mrow><annotation encoding="application/x-tex">\Xi \vert \Gamma, A:\mathcal{U}_i \vdash C:\mathcal{U}_{s_\mathcal{N}(i)}</annotation></semantics></math></div></li> <li> <p>Suppose we are given a <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a> with a separate <a class="existingWikiWord" href="/nlab/show/type">type</a> <a class="existingWikiWord" href="/nlab/show/judgment">judgment</a> but no universes. Then a <strong>class</strong> <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> is a generalized <a class="existingWikiWord" href="/nlab/show/modal+operator">modal operator</a> on the type theory, which isn’t required to be either <a class="existingWikiWord" href="/nlab/show/idempotent">idempotent</a> or <a class="existingWikiWord" href="/nlab/show/monadic">monadic</a>, such that given a <a class="existingWikiWord" href="/nlab/show/type">type</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>, the <a class="existingWikiWord" href="/nlab/show/type">type</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi><mo stretchy="false">(</mo><mi>A</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">C(A)</annotation></semantics></math> is an <a class="existingWikiWord" href="/nlab/show/h-proposition">h-proposition</a>.</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mrow><mrow><mi>Γ</mi><mo>⊢</mo><mi>C</mi><mo stretchy="false">(</mo><mi>A</mi><mo stretchy="false">)</mo><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mrow></mfrac><mspace width="2em"></mspace><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mrow><mrow><mi>Γ</mi><mo>⊢</mo><msubsup><mi>p</mi> <mi>A</mi> <mi>C</mi></msubsup><mo>:</mo><mi mathvariant="normal">isProp</mi><mo stretchy="false">(</mo><mi>C</mi><mo stretchy="false">(</mo><mi>A</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash C(A) \; \mathrm{type}} \qquad \frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash p_A^C:\mathrm{isProp}(C(A))}</annotation></semantics></math></div></li> <li> <p>Suppose we are given a <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a> with a separate <a class="existingWikiWord" href="/nlab/show/type">type</a> <a class="existingWikiWord" href="/nlab/show/judgment">judgment</a> but no <a class="existingWikiWord" href="/nlab/show/type+universes">type universes</a>, and are using the <a class="existingWikiWord" href="/nlab/show/propositions+as+types">propositions as types</a> interpretation of dependent type theory. Then a <strong>class</strong> <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> is a generalized <a class="existingWikiWord" href="/nlab/show/modal+operator">modal operator</a> on the type theory which isn’t required to be either <a class="existingWikiWord" href="/nlab/show/idempotent">idempotent</a> or <a class="existingWikiWord" href="/nlab/show/monadic">monadic</a>.</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mrow><mrow><mi>Γ</mi><mo>⊢</mo><mi>C</mi><mo stretchy="false">(</mo><mi>A</mi><mo stretchy="false">)</mo><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash C(A) \; \mathrm{type}}</annotation></semantics></math></div></li> </ul> <h2 id="examples">Examples</h2> <ul> <li> <p>In <a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a>, there is a class <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∃</mo><mi>a</mi><mo>.</mo><mi>a</mi><mo>∈</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">\exists a.a \in A</annotation></semantics></math> for whether the set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> is an <a class="existingWikiWord" href="/nlab/show/inhabited+set">inhabited set</a>. In <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a>, the class is the <a class="existingWikiWord" href="/nlab/show/propositional+truncation">propositional truncation</a> <a class="existingWikiWord" href="/nlab/show/modal+operator">modal operator</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">[</mo><mi>A</mi><mo stretchy="false">]</mo></mrow><annotation encoding="application/x-tex">[A]</annotation></semantics></math>.</p> </li> <li> <p>In <a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a>, there is a class <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∀</mo><mi>a</mi><mo>.</mo><mi>a</mi><mo>∈</mo><mi>A</mi><mo>∧</mo><mo>∀</mo><mi>b</mi><mo>.</mo><mi>b</mi><mo>∈</mo><mi>A</mi><mo>∧</mo><mi>a</mi><mo>=</mo><mi>b</mi></mrow><annotation encoding="application/x-tex">\forall a.a \in A \wedge \forall b.b \in A \wedge a = b</annotation></semantics></math> for whether the set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> is a <a class="existingWikiWord" href="/nlab/show/subsingleton">subsingleton</a>. In <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a>, the class is the <a class="existingWikiWord" href="/nlab/show/isProp">isProp</a> <a class="existingWikiWord" href="/nlab/show/modal+operator">modal operator</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Π</mi><mo stretchy="false">(</mo><mi>a</mi><mo>:</mo><mi>A</mi><mo stretchy="false">)</mo><mo>.</mo><mi>Π</mi><mo stretchy="false">(</mo><mi>b</mi><mo>:</mo><mi>A</mi><mo stretchy="false">)</mo><mo>.</mo><mo stretchy="false">(</mo><mi>a</mi><msub><mo>=</mo> <mi>A</mi></msub><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\Pi (a:A).\Pi (b:A).(a =_A b)</annotation></semantics></math>.</p> </li> <li> <p>In <a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a>, there is a class <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∃</mo><mi>a</mi><mo>.</mo><mi>a</mi><mo>∈</mo><mi>A</mi><mo>∧</mo><mo>∀</mo><mi>b</mi><mo>.</mo><mi>b</mi><mo>∈</mo><mi>A</mi><mo>∧</mo><mi>a</mi><mo>=</mo><mi>b</mi></mrow><annotation encoding="application/x-tex">\exists a.a \in A \wedge \forall b.b \in A \wedge a = b</annotation></semantics></math> for whether the set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> is a <a class="existingWikiWord" href="/nlab/show/singleton">singleton</a>. In <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a>, the class is the <a class="existingWikiWord" href="/nlab/show/isContr">isContr</a> <a class="existingWikiWord" href="/nlab/show/modal+operator">modal operator</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi><mo stretchy="false">(</mo><mi>a</mi><mo>:</mo><mi>A</mi><mo stretchy="false">)</mo><mo>.</mo><mi>Π</mi><mo stretchy="false">(</mo><mi>b</mi><mo>:</mo><mi>A</mi><mo stretchy="false">)</mo><mo>.</mo><mo stretchy="false">(</mo><mi>a</mi><msub><mo>=</mo> <mi>A</mi></msub><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\Sigma (a:A).\Pi (b:A).(a =_A b)</annotation></semantics></math>.</p> </li> </ul> <h2 id="internal_classes">Internal classes</h2> <p>It is possible to <a class="existingWikiWord" href="/nlab/show/internalization">internalize</a> the notion of class inside of the <a class="existingWikiWord" href="/nlab/show/foundations">foundations</a> itself. Classes are either primitive, such as in <a class="existingWikiWord" href="/nlab/show/class+theory">class theory</a>, or a derived concept from a notion of <a class="existingWikiWord" href="/nlab/show/universe">universe</a> in the foundations, such as in <a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a> or <a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a>. These internal classes are useful to address size issues in foundations, and in particular, are used in <a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a> for defining various <a class="existingWikiWord" href="/nlab/show/locally+small+categories">locally small categories</a> and <a class="existingWikiWord" href="/nlab/show/large+categories">large categories</a>.</p> <h3 id="classes_as_primitive">Classes as primitive</h3> <p>There are foundational theories called <a class="existingWikiWord" href="/nlab/show/class+theories">class theories</a> where classes are primitives, rather than propositions in the context of a free variable <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>:</mo><mi mathvariant="normal">Set</mi></mrow><annotation encoding="application/x-tex">x:\mathrm{Set}</annotation></semantics></math>. This is similar to <a class="existingWikiWord" href="/nlab/show/dependently+sorted+set+theory">dependently sorted</a> <a class="existingWikiWord" href="/nlab/show/allegorical+set+theories">allegorical set theories</a>, where <a class="existingWikiWord" href="/nlab/show/relations">relations</a> are primitives, rather than propositions in the context of free variables <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>:</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">a:A</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>B</mi></mrow><annotation encoding="application/x-tex">b:B</annotation></semantics></math>.</p> <ul> <li> <p>Material class theory: Classes are primitives of the theory, and sets are defined as specific kinds of classes. Examples include <a class="existingWikiWord" href="/nlab/show/Morse-Kelley+class+theory">Morse-Kelley class theory</a> and <a class="existingWikiWord" href="/nlab/show/von+Neumann%E2%80%93Bernays%E2%80%93G%C3%B6del+class+theory">von Neumann–Bernays–Gödel class theory</a>.</p> </li> <li> <p>Structural class theory: A <strong>class</strong> is an object of a <a class="existingWikiWord" href="/nlab/show/category+of+classes">category of classes</a>, and sets are defined as specific kinds of classes. Examples include <a class="existingWikiWord" href="/nlab/show/category+with+class+structure">category with class structure</a> and the branch of <a class="existingWikiWord" href="/nlab/show/algebraic+set+theory">algebraic set theory</a></p> </li> </ul> <h3 id="classes_as_derived_from_universes">Classes as derived from universes</h3> <h4 id="in_set_theory">In set theory</h4> <p>There are many notions of <a class="existingWikiWord" href="/nlab/show/universe">universe</a> in <a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a>, including <a class="existingWikiWord" href="/nlab/show/Grothendieck+universes">Grothendieck universes</a>, <a class="existingWikiWord" href="/nlab/show/well-pointed+pretopos">well-pointed</a> <a class="existingWikiWord" href="/nlab/show/Heyting+pretopoi">Heyting pretopoi</a>, and <a class="existingWikiWord" href="/nlab/show/well-pointed+category">well-pointed</a> <a class="existingWikiWord" href="/nlab/show/division+allegories">division allegories</a>.</p> <p>Let <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> be a <a class="existingWikiWord" href="/nlab/show/universe">universe</a>. Then a <strong>class</strong> relative 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> is a <a class="existingWikiWord" href="/nlab/show/subset">subset</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi><mo>⊆</mo><mi>U</mi></mrow><annotation encoding="application/x-tex">C \subseteq U</annotation></semantics></math> with a given injection <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>i</mi><mo>:</mo><mi>C</mi><mo>↪</mo><mi>U</mi></mrow><annotation encoding="application/x-tex">i:C \hookrightarrow U</annotation></semantics></math>. If one has choice, any subset comes with a given injection via the <a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a>. Thus, by this definition, it is a injective <a class="existingWikiWord" href="/nlab/show/family+of+sets">family 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>-small sets</a>.</p> <p>Equivalently, a class <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> relative 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> is an <a class="existingWikiWord" href="/nlab/show/endofunction">endofunction</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi><mo>:</mo><mi>U</mi><mo>→</mo><mi>U</mi></mrow><annotation encoding="application/x-tex">C:U \to U</annotation></semantics></math> such that for all <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>-small sets <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>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi><mo stretchy="false">(</mo><mi>A</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">C(A)</annotation></semantics></math> is a <a class="existingWikiWord" href="/nlab/show/subsingleton">subsingleton</a> subset.</p> <h4 id="in_dependent_type_theory">In dependent type theory</h4> <p>In <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a>, let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>U</mi><mo>,</mo><mi>T</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(U, T)</annotation></semantics></math> be a <a class="existingWikiWord" href="/nlab/show/univalent+universe">univalent</a> <a class="existingWikiWord" href="/nlab/show/Tarski+universe">Tarski universe</a>, let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><msub><mi mathvariant="normal">Set</mi> <mi>U</mi></msub><mo>,</mo><msub><mi mathvariant="normal">Set</mi> <mi>T</mi></msub><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(\mathrm{Set}_U, \mathrm{Set}_T)</annotation></semantics></math> be the univalent <a class="existingWikiWord" href="/nlab/show/h-groupoid">h-groupoid</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>-small <a class="existingWikiWord" href="/nlab/show/h-sets">h-sets</a>, let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>V</mi> <mi>U</mi></msub></mrow><annotation encoding="application/x-tex">V_U</annotation></semantics></math> be the <a class="existingWikiWord" href="/nlab/show/material+set+theory">material</a> <a class="existingWikiWord" href="/nlab/show/cumulative+hierarchy">cumulative hierarchy</a> <a class="existingWikiWord" href="/nlab/show/higher+inductive+type">higher inductive type</a> relative 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>. Then a <strong>class</strong> is an <a class="existingWikiWord" href="/nlab/show/endofunction">endofunction</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi><mo>:</mo><msub><mi mathvariant="normal">Set</mi> <mi>U</mi></msub><mo>→</mo><msub><mi mathvariant="normal">Set</mi> <mi>U</mi></msub></mrow><annotation encoding="application/x-tex">C:\mathrm{Set}_U \to \mathrm{Set}_U</annotation></semantics></math> such that for all <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>-small sets <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>:</mo><msub><mi mathvariant="normal">Set</mi> <mi>U</mi></msub></mrow><annotation encoding="application/x-tex">A:\mathrm{Set}_U</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>C</mi><mo stretchy="false">(</mo><mi>A</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(C(A))</annotation></semantics></math> is a <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>-small <a class="existingWikiWord" href="/nlab/show/h-proposition">h-proposition</a>, and a <strong>material class</strong> is a function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi><mo>:</mo><msub><mi>V</mi> <mi>U</mi></msub><mo>→</mo><msub><mi mathvariant="normal">Set</mi> <mi>U</mi></msub></mrow><annotation encoding="application/x-tex">C:V_U \to \mathrm{Set}_U</annotation></semantics></math> such that for all material sets <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>:</mo><msub><mi>V</mi> <mi>U</mi></msub></mrow><annotation encoding="application/x-tex">A:V_U</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>C</mi><mo stretchy="false">(</mo><mi>A</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(C(A))</annotation></semantics></math> is a <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>-small <a class="existingWikiWord" href="/nlab/show/h-proposition">h-proposition</a>.</p> <h3 id="proper_classes">Proper classes</h3> <p>A <strong>proper class</strong> is a class which is not a <a class="existingWikiWord" href="/nlab/show/set">set</a>. What a set is differs from foundations to foundations.</p> <p>What not being a set means depends upon the foundation; in <a class="existingWikiWord" href="/nlab/show/material+set+theory">material set theory</a>, one would use the property of not being equal to any sets, while in <a class="existingWikiWord" href="/nlab/show/structural+set+theory">structural set theory</a>, one would use the property of not being in <a class="existingWikiWord" href="/nlab/show/bijection">bijection</a> with any sets.</p> <p>Given a notion of <a class="existingWikiWord" href="/nlab/show/universe">universe</a>, a <strong><a class="existingWikiWord" href="/nlab/show/proper+class">proper class</a> relative 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></strong> is a class relative 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> which is not a set. If classes are defined as subsets 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> with an injection into <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>, then a proper class is a class which is not a <a class="existingWikiWord" href="/nlab/show/singleton+subset">singleton subset</a>.</p> <p>In the context of the <a class="existingWikiWord" href="/nlab/show/global+axiom+of+choice">global axiom of choice</a>, a proper class is a class which can be put in <a class="existingWikiWord" href="/nlab/show/bijection">bijection</a> with the class of all <a class="existingWikiWord" href="/nlab/show/ordinal+number">ordinals</a>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Ord</mi></mrow><annotation encoding="application/x-tex">Ord</annotation></semantics></math>.</p> <h2 id="category_of_classes">Category of classes</h2> <p>The <a class="existingWikiWord" href="/nlab/show/category+of+classes">category of classes</a> is closed under all large <a class="existingWikiWord" href="/nlab/show/colimits">colimits</a> and <a class="existingWikiWord" href="/nlab/show/small+limits">small limits</a>. See the linked article for more information and precise definitions.</p> <p>Just as an <a class="existingWikiWord" href="/nlab/show/elementary+topos">elementary topos</a> is an axiomatization of basic properties of the category <a class="existingWikiWord" href="/nlab/show/Set">Set</a>, a <a class="existingWikiWord" href="/nlab/show/category+with+class+structure">category with class structure</a> is an axiomatization of basic properties of the category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Class</mi></mrow><annotation encoding="application/x-tex">Class</annotation></semantics></math>. See also <a class="existingWikiWord" href="/nlab/show/algebraic+set+theory">algebraic set theory</a>.</p> <h2 id="see_also"> See also</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/class+object">class object</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/class+theory">class theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/category+of+classes">category of classes</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/type+of+classes">type of classes</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/family+of+sets">family of sets</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/large+set">large set</a>, <a class="existingWikiWord" href="/nlab/show/small+set">small set</a></p> </li> </ul> <h2 id="references">References</h2> <p>For the definition of a material class relative to a universe <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 <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a>, see section 10.5.3 of:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Univalent+Foundations+Project">Univalent Foundations Project</a>, <em><a class="existingWikiWord" href="/nlab/show/Homotopy+Type+Theory+--+Univalent+Foundations+of+Mathematics">Homotopy Type Theory – Univalent Foundations of Mathematics</a></em>, Institute for Advanced Study (2013) [<a href="http://homotopytypetheory.org/book/">web</a>, <a href="http://hottheory.files.wordpress.com/2013/03/hott-online-323-g28e4374.pdf">pdf</a>]</li> </ul> <p>A paper detailing one approach to the technical side of how classes appear in <a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a> (namely using <a class="existingWikiWord" href="/nlab/show/Grothendieck+universes">Grothendieck universes</a>) is</p> <ul> <li id="Levy18"><a class="existingWikiWord" href="/nlab/show/Paul+Blain+Levy">Paul Blain Levy</a>, <em>Formulating Categorical Concepts using Classes</em> [<a href="https://arxiv.org/abs/1801.08528">arXiv:1801.08528</a>]</li> </ul> </body></html> </div> <div class="revisedby"> <p> Last revised on November 19, 2022 at 19:01:51. See the <a href="/nlab/history/class" 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/class" accesskey="E" class="navlink" id="edit" rel="nofollow">Edit</a><a href="https://nforum.ncatlab.org/discussion/8919/#Item_26">Discuss</a><span class="backintime"><a href="/nlab/revision/class/25" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/diff/class" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Changes from previous revision</a><a href="/nlab/history/class" accesskey="S" class="navlink" id="history" rel="nofollow">History (25 revisions)</a> <a href="/nlab/show/class/cite" style="color: black">Cite</a> <a href="/nlab/print/class" accesskey="p" id="view_print" rel="nofollow">Print</a> <a href="/nlab/source/class" id="view_source" rel="nofollow">Source</a> </div> </div>  </div>  </body> </html>