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> fully formal ETCS 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> fully formal ETCS </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/discussions/?CategoryID=0" title="Discuss this page on the nForum. It does not yet have a dedicated thread; feel free to create one, giving it the same name as the title of this page" style="color:black">Discuss this page</a> | <form accept-charset="utf-8" action="/nlab/search" id="navigationSearchForm" method="get"> <fieldset class="search"><input type="text" id="searchField" name="query" value="Search" style="display:inline-block; float: left;" onfocus="this.value == 'Search' ? this.value = '' : true" onblur="this.value == '' ? this.value = 'Search' : true" /></fieldset> </form> <span id='navEnd'></span> </div> <div id="revision"> <html xmlns="http://www.w3.org/1999/xhtml" xmlns:svg="http://www.w3.org/2000/svg" xml:lang="en" lang="en"> <head><meta http-equiv="Content-type" content="application/xhtml+xml;charset=utf-8" /><title>Contents</title></head> <body> <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+inequality+spaces">axiom of inequality spaces</a></p> </li> </ul> </div> <h2 id="removing_axioms">Removing axioms</h2> <ul> <li><a class="existingWikiWord" href="/nlab/show/constructive+mathematics">constructive mathematics</a></li> <li><a class="existingWikiWord" href="/nlab/show/predicative+mathematics">predicative mathematics</a></li> </ul> <div> <p> <a href="/nlab/edit/foundations+-+contents">Edit this sidebar</a> </p> </div></div></div> <h4 id="topos_theory">Topos Theory</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/topos+theory">topos theory</a></strong></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Toposes">Toposes</a></li> </ul> <h2 id="background">Background</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/category">category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/functor">functor</a></p> </li> </ul> </li> </ul> <h2 id="toposes">Toposes</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/%280%2C1%29-topos">(0,1)-topos</a>, <a class="existingWikiWord" href="/nlab/show/Heyting+algebra">Heyting algebra</a>, <a class="existingWikiWord" href="/nlab/show/locale">locale</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/pretopos">pretopos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/topos">topos</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Grothendieck+topos">Grothendieck topos</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/category+of+presheaves">category of presheaves</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/presheaf">presheaf</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/representable+functor">representable presheaf</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/category+of+sheaves">category of sheaves</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/site">site</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/sieve">sieve</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/coverage">coverage</a>, <a class="existingWikiWord" href="/nlab/show/Grothendieck+pretopology">pretopology</a>, <a class="existingWikiWord" href="/nlab/show/Grothendieck+topology">topology</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/sheaf">sheaf</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/sheafification">sheafification</a></p> </li> </ul> </li> </ul> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/quasitopos">quasitopos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/base+topos">base topos</a>, <a class="existingWikiWord" href="/nlab/show/indexed+topos">indexed topos</a></p> </li> </ul> <h2 id="internal_logic">Internal Logic</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/categorical+semantics">categorical semantics</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/internal+logic">internal logic</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/subobject+classifier">subobject classifier</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/natural+numbers+object">natural numbers object</a></p> </li> </ul> </li> </ul> <h2 id="topos_morphisms">Topos morphisms</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/logical+morphism">logical morphism</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/geometric+morphism">geometric morphism</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/direct+image">direct image</a>/<a class="existingWikiWord" href="/nlab/show/inverse+image">inverse image</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/global+section">global sections</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/geometric+embedding">geometric embedding</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/surjective+geometric+morphism">surjective geometric morphism</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/essential+geometric+morphism">essential geometric morphism</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/locally+connected+geometric+morphism">locally connected geometric morphism</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/connected+geometric+morphism">connected geometric morphism</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/totally+connected+geometric+morphism">totally connected geometric morphism</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/%C3%A9tale+geometric+morphism">étale geometric morphism</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/open+geometric+morphism">open geometric morphism</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/proper+geometric+morphism">proper geometric morphism</a>, <a class="existingWikiWord" href="/nlab/show/compact+topos">compact topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/separated+geometric+morphism">separated geometric morphism</a>, <a class="existingWikiWord" href="/nlab/show/Hausdorff+topos">Hausdorff topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/local+geometric+morphism">local geometric morphism</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/bounded+geometric+morphism">bounded geometric morphism</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/base+change">base change</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/localic+geometric+morphism">localic geometric morphism</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/hyperconnected+geometric+morphism">hyperconnected geometric morphism</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/atomic+geometric+morphism">atomic geometric morphism</a></p> </li> </ul> </li> </ul> <h2 id="extra_stuff_structure_properties">Extra stuff, structure, properties</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/topological+locale">topological locale</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/localic+topos">localic topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/petit+topos">petit topos/gros topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/locally+connected+topos">locally connected topos</a>, <a class="existingWikiWord" href="/nlab/show/connected+topos">connected topos</a>, <a class="existingWikiWord" href="/nlab/show/totally+connected+topos">totally connected topos</a>, <a class="existingWikiWord" href="/nlab/show/strongly+connected+topos">strongly connected topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/local+topos">local topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/cohesive+topos">cohesive topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/classifying+topos">classifying topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/smooth+topos">smooth topos</a></p> </li> </ul> <h2 id="cohomology_and_homotopy">Cohomology and homotopy</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/cohomology">cohomology</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/homotopy+groups+in+an+%28infinity%2C1%29-topos">homotopy</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/abelian+sheaf+cohomology">abelian sheaf cohomology</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/model+structure+on+simplicial+presheaves">model structure on simplicial presheaves</a></p> </li> </ul> <h2 id="in_higher_category_theory">In higher category theory</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/higher+topos+theory">higher topos theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/%280%2C1%29-topos">(0,1)-topos</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/%280%2C1%29-site">(0,1)-site</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/2-topos">2-topos</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/2-site">2-site</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/2-sheaf">2-sheaf</a>, <a class="existingWikiWord" href="/nlab/show/stack">stack</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2C1%29-topos">(∞,1)-topos</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2C1%29-site">(∞,1)-site</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2C1%29-sheaf">(∞,1)-sheaf</a>, <a class="existingWikiWord" href="/nlab/show/%E2%88%9E-stack">∞-stack</a>, <a class="existingWikiWord" href="/nlab/show/derived+stack">derived stack</a></p> </li> </ul> </li> </ul> <h2 id="theorems">Theorems</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Diaconescu%27s+theorem">Diaconescu's theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Barr%27s+theorem">Barr's theorem</a></p> </li> </ul> <div> <p> <a href="/nlab/edit/topos+theory+-+contents">Edit this sidebar</a> </p> </div></div></div> </div> </div> <h1 id="contents">Contents</h1> <div class='maruku_toc'> <ul> <li><a href='#introduction'>Introduction</a></li> <ul> <li><a href='#choices_in_presentation'>Choices in presentation</a></li> <ul> <li><a href='#choosing_sequent_calculus'>Choosing sequent calculus</a></li> <li><a href='#choosing_the_multiplicity_of_predicates'>Choosing the multiplicity of predicates</a></li> <li><a href='#whether_onthenose_or_up_to_isomorphism'>Whether on-the-nose or up to isomorphism?</a></li> </ul> <li><a href='#layering_etcs'>Layering ETCS</a></li> </ul> <li><a href='#preliminaries'>Preliminaries</a></li> <li><a href='#the_theory_of_categories'>The theory of categories</a></li> <li><a href='#the_theory_of_finitely_complete_categories'>The theory of finitely complete categories</a></li> <li><a href='#the_theory_of_elementary_toposes'>The theory of elementary toposes</a></li> <li><a href='#the_theory_etcs'>The theory ETCS</a></li> <li><a href='#remarks'>Remarks</a></li> <ul> <li><a href='#on_'>On <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Th</mi><mo stretchy="false">(</mo><mi>Cat</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Th(Cat)</annotation></semantics></math></a></li> </ul> <li><a href='#references'>References</a></li> </ul> </div> <h2 id="introduction">Introduction</h2> <p>This page addresses a frequently voiced but easily corrected misconception about <a href="http://ncatlab.org/nlab/show/foundation+of+mathematics#CFM">categorial</a> approaches to <a class="existingWikiWord" href="/nlab/show/foundations+of+mathematics">foundations of mathematics</a>, namely that there is a logical circularity in using <a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a> to give an axiomatic <a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a> (such as <a class="existingWikiWord" href="/nlab/show/ETCS">ETCS</a>), since categories themselves are <a class="existingWikiWord" href="/nlab/show/sets">sets</a> (or collections) with extra <a class="existingWikiWord" href="/nlab/show/structure">structure</a>.</p> <p>The most straightforward response is a formalist one: category theory and various elaborations like <a class="existingWikiWord" href="/nlab/show/ETCS">ETCS</a> are <a class="existingWikiWord" href="/nlab/show/first-order+theories">first-order theories</a>, just as <a class="existingWikiWord" href="/nlab/show/ZFC">ZFC</a> is. One doesn’t need a theory of sets prior to a theory of categories, any more than one needs a theory of sets prior to a theory of sets. Fully formalized, ETCS makes no mention of sets, only a <a class="existingWikiWord" href="/nlab/show/signature">signature</a> and a list of <a class="existingWikiWord" href="/nlab/show/axioms">axioms</a>; the only background is <a class="existingWikiWord" href="/nlab/show/predicate+logic">first-order logic</a> (which gives the rules for deducing theorems). All of these remarks are perfectly obvious, but the misunderstanding above is common enough that working out the details of full formalization and recording them might be a useful exercise, and that is what we carry out here.</p> <h3 id="choices_in_presentation">Choices in presentation</h3> <p>While we’re at it, however, we should also point out features of categorical set theory which distinguish it from traditional forms of set theory such as ZFC. Conceptually and philosophically, there is a big difference in that ZFC emphasizes membership between sets as the basic relation (founded on the idea that elements can themselves have elements), whereas in ETCS elements of sets are intuited as essentially featureless (sets being “bags of dots” so to speak, where elements are distinguishable but have no internal structure), and the emphasis is rather on mappings and patterns of mappings where mathematically relevant structure resides.</p> <p>These conceptual distinctions are discussed more fully elsewhere in the nLab; see for example <a class="existingWikiWord" href="/nlab/show/structural+set+theory">structural set theory</a> and pages and references linked therein. Our focus in this page will be on more formalist concerns, but even after disengaging from possibly contentious philosophical issues, experience has shown that logicians not familiar with the categorical background might easily misunderstand what we are doing and why we make the choices we do, and worse, deride those choices from lack of understanding. We thus feel some advance explanation might be of some benefit.</p> <h4 id="choosing_sequent_calculus">Choosing sequent calculus</h4> <p>Even if we restrict focus to formal aspects, there are notable differences between axioms of ETCS and axioms of ZFC in terms of the strength of the underlying logic needed to express them, or in terms of what <a href="http://ncatlab.org/nlab/show/internal+logic#kinds_of_internal_logics_in_different_categories_20">internal logical</a> assumptions are needed on a background environment in which to interpret them. The relevant distinctions between different types of internal theories (e.g., finite limit theories, coherent theories, etc.) is often conveniently expressed via a <a class="existingWikiWord" href="/nlab/show/sequent+calculus">sequent calculus</a>-style presentation of first-order logic that is common currency among categorical logicians, and that is the mode we will adopt here.</p> <p>When we write a sequent <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi><mo>⊢</mo><mi>ψ</mi></mrow><annotation encoding="application/x-tex">\varphi \vdash \psi</annotation></semantics></math>, it is understood that predicates <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi></mrow><annotation encoding="application/x-tex">\varphi</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ψ</mi></mrow><annotation encoding="application/x-tex">\psi</annotation></semantics></math> have the same type (we could write <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi><msub><mo>⊢</mo> <mi>X</mi></msub><mi>ψ</mi></mrow><annotation encoding="application/x-tex">\varphi \vdash_X \psi</annotation></semantics></math> to indicate that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>φ</mi></mrow><annotation encoding="application/x-tex">\varphi</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ψ</mi></mrow><annotation encoding="application/x-tex">\psi</annotation></semantics></math> are both of type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math>). Roughly speaking, this means they have the same free variables, although if we see a sequent of the form</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>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo>⊢</mo><mi>ψ</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\varphi(x, y) \vdash \psi(x)</annotation></semantics></math></div> <p>where a free variable <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi></mrow><annotation encoding="application/x-tex">y</annotation></semantics></math> does not appear explicitly, then we can match up the types by adding it in freely, replacing <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ψ</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\psi(x)</annotation></semantics></math> by <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ψ</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>∧</mo><mo stretchy="false">[</mo><mi>y</mi><mo>=</mo><mi>y</mi><mo stretchy="false">]</mo></mrow><annotation encoding="application/x-tex">\psi(x) \wedge [y = y]</annotation></semantics></math>. This replacement process corresponds to a “substitution” operation in a <a class="existingWikiWord" href="/nlab/show/hyperdoctrine">hyperdoctrine</a>, a way of doing categorical logic. In fact, a sequent calculus gives rise to a functor</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>Pred</mi><mo>:</mo><msup><mi>Types</mi> <mi>op</mi></msup><mo>→</mo><mi>Preord</mi></mrow><annotation encoding="application/x-tex">Pred: Types^{op} \to Preord</annotation></semantics></math></div> <p>taking each type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> to the set of predicates of that type, preordered by the entailment relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mo>⊢</mo> <mi>X</mi></msub></mrow><annotation encoding="application/x-tex">\vdash_X</annotation></semantics></math>, and where <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Pred</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Pred(f)</annotation></semantics></math> is a substitution map of preorders for each map <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><mi>X</mi><mo>→</mo><mi>Y</mi></mrow><annotation encoding="application/x-tex">f: X \to Y</annotation></semantics></math> between types. Composing with the posetal reflection <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Preord</mi><mo>→</mo><mi>Pos</mi></mrow><annotation encoding="application/x-tex">Preord \to Pos</annotation></semantics></math> gives a hyperdoctrine</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msup><mi>Types</mi> <mi>op</mi></msup><mo>→</mo><mo lspace="0em" rspace="thinmathspace">Pos</mo></mrow><annotation encoding="application/x-tex">Types^{op} \to \Pos</annotation></semantics></math></div> <p>which plays the role of a Lindenbaum algebra. Thus the close connection between sequent calculus presentations and the sorts of hyperdoctrine presentations that have proved effective in categorical logic.</p> <p>In a categorical semantics of a sequent calculus, we have a category of types <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> and a hyperdoctrine <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Sub</mi><mo>:</mo><msup><mi>C</mi> <mi>op</mi></msup><mo>→</mo><mi>Pos</mi></mrow><annotation encoding="application/x-tex">Sub: C^{op} \to Pos</annotation></semantics></math> that assigns to each object <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> its subobject lattice, and a map between hyperdoctrines <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Pred</mi><mo>→</mo><mi>Sub</mi></mrow><annotation encoding="application/x-tex">Pred \to Sub</annotation></semantics></math>. Thus each formula represents a subobject (of an object represented by the formula’s type), and a sequent represents an inclusion between subobjects. Logical operations represent categorical operations on subobject lattices in a natural way in the semantics of sequent calculus, e.g., <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∃</mo></mrow><annotation encoding="application/x-tex">\exists</annotation></semantics></math> represents taking the image of a subobject along a map, and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∧</mo></mrow><annotation encoding="application/x-tex">\wedge</annotation></semantics></math> represents intersections of subobjects.</p> <h4 id="choosing_the_multiplicity_of_predicates">Choosing the multiplicity of predicates</h4> <p>In addition, there are different choices of signature in which one might present a theory. Our own choices of signature are driven by the desire to have the model theorist’s notion of homomorphism match the category theorist’s notion of morphism appropriate for a given situation. For example: it is possible to define a monoid as a structure consisting of a associative binary operation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>m</mi></mrow><annotation encoding="application/x-tex">m</annotation></semantics></math> for which a two-sided identity element <em>exists</em> (so the signature of the theory of monoids consists of just a binary function symbol <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>m</mi></mrow><annotation encoding="application/x-tex">m</annotation></semantics></math>); one can then prove the identity is unique. However, homomorphisms of models of this theory, under this signature, need not preserve the identity; if we want identities to be preserved, then a constant for the identity needs to be explicitly added to the signature. In the same way, one <em>could</em> define a category by recourse to a single ternary relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>c</mi><mo stretchy="false">(</mo><mi>f</mi><mo>,</mo><mi>g</mi><mo>,</mo><mi>h</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">c(f, g, h)</annotation></semantics></math> whose intended interpretation is that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi></mrow><annotation encoding="application/x-tex">f</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>g</mi></mrow><annotation encoding="application/x-tex">g</annotation></semantics></math> are composable morphisms such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>∘</mo><mi>g</mi><mo>=</mo><mi>h</mi></mrow><annotation encoding="application/x-tex">f \circ g = h</annotation></semantics></math>, and add axioms stipulating existence of identities, but then homomorphisms fail to be functors.</p> <p>Likewise, if we are presenting a theory of finitely complete categories, then it is not enough to say they are categories for which finite limits exist: if we want the relevant homomorphisms of models of the theory to be functors that preserve finite limits, then appropriate predicates for finite limits (e.g., for pullbacks and terminal objects) need to be adjoined to the signature. And so on. Note that such requirements add (slightly) to the length of the presentation, but we regard that as a superficial consideration – it is more important to have the signature and axioms reflect the correct notion of homomorphism for each layer of structure.</p> <h4 id="whether_onthenose_or_up_to_isomorphism">Whether on-the-nose or up to isomorphism?</h4> <p>A final consideration is whether we want a categorical set theory to have <em>chosen</em> products, <em>chosen</em> power objects, etc. or we want such structures to be uniquely given only up to isomorphism. The prevailing tendency among category theorists is to go with the latter; if we want to reflect that practice, then the signature ought to be relational; for example, we might have a ternary predicate <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>prod</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo>,</mo><mi>c</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">prod(a, b, c)</annotation></semantics></math> which says <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 <em>a</em> product of objects <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 <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi></mrow><annotation encoding="application/x-tex">b</annotation></semantics></math>, rather than have a binary function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>×</mo><mi>b</mi></mrow><annotation encoding="application/x-tex">a \times b</annotation></semantics></math> which specifies <em>the</em> product.</p> <p>The present author (Todd Trimble) feels the difference isn’t such a big deal; while choosing particular products, pullbacks, power objects, etc. as part of the structure might not seem “natural”, such strict or rigid structure is basically harmless. This observation can be formalized in terms of suitable equivalences (in much the same way that while monoidal categories and monoidal functors occur more often in nature, there are strictification 2-functors which allow for them to be formally and equivalently replaced by strict monoidal categories and strict monoidal functors). There are in fact benefits to working with strict structures because they can be expressed in very weak fragments of logic. For example, the theory of strict toposes is a finite limit theory (it is finitary-algebraic over the category of directed graphs), meaning the notion of strict topos object can be internalized within any finitely complete category.</p> <p>Thus, we will present fragments of the theory ETCS along two parallel tracks, one being with structure considered only up to isomorphism (expressed in a coherent theory), and the other involving specific choices of structure (expressed in a finite limit theory). That will bring us up to the theory of toposes with a natural numbers object. This in itself is a reasonable notion of category of sets; to use words of Lawvere, we can view it as a categorical theory of “variable sets”.</p> <p>Two further axioms are adjoined to the theory of toposes with NNO to get ETCS (bringing one closer to a category of Zermelo sets; to use words of Lawvere, ETCS is a categorical theory of “constant sets”): the axiom of choice and the axiom of well-pointedness. These axioms are non-algebraic axioms that take us outside of finite limit logic: the axiom of choice is manifestly written in coherent logic, and the well-pointedness axiom is not even coherent (although ETCS can, via “Morleyization”, be rewritten in coherent logic if excluded middle is assumed in the meta-logic).</p> <h3 id="layering_etcs">Layering ETCS</h3> <p>ETCS as presented here is built up in stages:</p> <ul> <li> <p>The theory of categories, as a one-sorted theory. (The usual presentation involves two sorts, objects and morphisms. Our excuse is that many introductions to logic do not discuss any except one-sorted theories – thus these are more familiar to logical novices, the very ones subject to the misconceptions recounted above.) In a morphisms-only approach, we have “source” and “target” operations and a ternary predicate <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>c</mi><mo stretchy="false">(</mo><mi>f</mi><mo>,</mo><mi>g</mi><mo>,</mo><mi>h</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">c(f, g, h)</annotation></semantics></math>, meaning “<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi></mrow><annotation encoding="application/x-tex">f</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>g</mi></mrow><annotation encoding="application/x-tex">g</annotation></semantics></math> are composable and their composite is <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>h</mi></mrow><annotation encoding="application/x-tex">h</annotation></semantics></math>”.</p> </li> <li> <p>The theory of categories with finite limits. This builds on the previous theory and adds some new predicates, namely an unary predicate <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>1</mn></mrow><annotation encoding="application/x-tex">1</annotation></semantics></math> where <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>1</mn><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">1(x)</annotation></semantics></math> means “<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math> is terminal”, and a quaternary predicate <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi></mrow><annotation encoding="application/x-tex">p</annotation></semantics></math> where <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi><mo stretchy="false">(</mo><mi>f</mi><mo>,</mo><mi>g</mi><mo>,</mo><mi>h</mi><mo>,</mo><mi>k</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">p(f, g, h, k)</annotation></semantics></math> means “<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi></mrow><annotation encoding="application/x-tex">f</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>g</mi></mrow><annotation encoding="application/x-tex">g</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>h</mi></mrow><annotation encoding="application/x-tex">h</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>k</mi></mrow><annotation encoding="application/x-tex">k</annotation></semantics></math> are the arrows of a pullback square”.</p> </li> <li> <p>The theory of toposes with a <a class="existingWikiWord" href="/nlab/show/natural+numbers+object">natural numbers object</a> (NNO). Here we add in still more predicates to capture the notion of power object up to isomorphism.</p> </li> <li> <p>The theory of toposes with NNO that are well-pointed (terminal objects are generators) and satisfy AC (every epi has a section).</p> </li> </ul> <p>The sections below reflect this multi-stage approach.</p> <h2 id="preliminaries">Preliminaries</h2> <p>We assume familiarity with the standard notion of a <a class="existingWikiWord" href="/nlab/show/algebraic+theory">(finitary) first-order theory</a> with equality; this includes the standard rules of deduction in the Gentzen <a class="existingWikiWord" href="/nlab/show/sequent+calculus">sequent calculus</a> for first-order logic.</p> <p>First-order <a class="existingWikiWord" href="/nlab/show/theory">theories</a> are typically presented in terms of a <a class="existingWikiWord" href="/nlab/show/signature">signature</a> consisting of function and predicate symbols, together with axioms each of which is a closed formula in the first-order language generated by the signature. That mode of presentation will be followed here. Standard logical conventions are followed; for example, it is common to state axioms as formulas <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo stretchy="false">(</mo><msub><mi>x</mi> <mn>1</mn></msub><mo>,</mo><mi>…</mi><mo>,</mo><msub><mi>x</mi> <mi>n</mi></msub><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">P(x_1, \ldots, x_n)</annotation></semantics></math> in which some of the variables <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>x</mi> <mi>i</mi></msub></mrow><annotation encoding="application/x-tex">x_i</annotation></semantics></math> may appear freely, with the implicit understanding that such variables are bound by unwritten <a class="existingWikiWord" href="/nlab/show/universal+quantifiers">universal quantifiers</a> at the heads of formulas, to make the formulas closed.</p> <p>To make the exposition more readable, we add some explanations (in parentheses) which do not belong to the formal theory, but which may aid comprehension. We also employ the standard device of abbreviating formulas, by declaring at various junctures definitions and notational conventions.</p> <p>In formalizing universal properties, one very helpful purely logical abbreviation is the “exists-unique” quantifier <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∃</mo><mo>!</mo></mrow><annotation encoding="application/x-tex">\exists !</annotation></semantics></math>. Namely, if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Q</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Q(x)</annotation></semantics></math> is a formula in which a variable <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math> appears freely, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∃</mo><mo>!</mo><mi>x</mi><mo>:</mo><mi>Q</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\exists ! x: Q(x)</annotation></semantics></math> is shorthand for the conjunction of</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><msub><mo>∃</mo> <mi>x</mi></msub><mi>Q</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(\exists_x Q(x))</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>Q</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>=</mo><mi>Q</mi><mo stretchy="false">(</mo><mi>y</mi><mo stretchy="false">)</mo><mo>⊢</mo><mi>x</mi><mo>=</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">Q(x) = Q(y) \vdash x = y</annotation></semantics></math></div> <h2 id="the_theory_of_categories">The theory of categories</h2> <div class="un_def"> <h6 id="definition">Definition</h6> <p>We define the <a class="existingWikiWord" href="/nlab/show/theory">theory</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Th</mi><mo stretchy="false">(</mo><mi>Cat</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Th(Cat)</annotation></semantics></math> of <a class="existingWikiWord" href="/nlab/show/categories">categories</a>.</p> <p>The <a class="existingWikiWord" href="/nlab/show/signature">signature</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Th</mi><mo stretchy="false">(</mo><mi>Cat</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Th(Cat)</annotation></semantics></math> consists of</p> <ul> <li> <p>Unary function symbols <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi></mrow><annotation encoding="application/x-tex">s</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>t</mi></mrow><annotation encoding="application/x-tex">t</annotation></semantics></math>;</p> </li> <li> <p>A ternary predicate <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>.</p> </li> </ul> <p>(The <a class="existingWikiWord" href="/nlab/show/theory">theory</a> of <a class="existingWikiWord" href="/nlab/show/categories">categories</a> is commonly presented as a two-sorted theory, with an object sort and a morphism sort. Here we instead use <a class="existingWikiWord" href="/nlab/show/single-sorted+definition+of+a+category">the single-sorted theory</a>, whose terms are to be interpreted as <em>morphisms</em> of a category. We generally use letters <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>,</mo><mi>g</mi><mo>,</mo><mi>h</mi><mo>,</mo><mi>…</mi></mrow><annotation encoding="application/x-tex">f, g, h, \ldots</annotation></semantics></math> for variable terms. If <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>e</mi></mrow><annotation encoding="application/x-tex">e</annotation></semantics></math> is any term, then the intended interpretation of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi><mo stretchy="false">(</mo><mi>e</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">s(e)</annotation></semantics></math> is: the identity morphism of the domain of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>e</mi></mrow><annotation encoding="application/x-tex">e</annotation></semantics></math>. Similarly, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>t</mi><mo stretchy="false">(</mo><mi>e</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">t(e)</annotation></semantics></math> means the identity morphism of the codomain of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>e</mi></mrow><annotation encoding="application/x-tex">e</annotation></semantics></math>. The intended interpretation of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>c</mi><mo stretchy="false">(</mo><mi>f</mi><mo>,</mo><mi>g</mi><mo>,</mo><mi>h</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">c(f, g, h)</annotation></semantics></math> is that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>h</mi><mo>=</mo><mi>f</mi><mo>∘</mo><mi>g</mi></mrow><annotation encoding="application/x-tex">h = f \circ g</annotation></semantics></math>.)</p> <p>The axioms of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Th</mi><mo stretchy="false">(</mo><mi>Cat</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Th(Cat)</annotation></semantics></math> are as follows:</p> <ol> <li> <p><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊢</mo><mo stretchy="false">(</mo><mi>s</mi><mi>s</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo>=</mo><mi>s</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo>=</mo><mi>t</mi><mi>s</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>∧</mo><mo stretchy="false">(</mo><mi>t</mi><mi>t</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo>=</mo><mi>t</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo>=</mo><mi>s</mi><mi>t</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\vdash (s s(f) = s(f) = t s (f)) \wedge (t t(f) = t(f) = s t(f))</annotation></semantics></math>.</p> </li> <li> <p><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>c</mi><mo stretchy="false">(</mo><mi>f</mi><mo>,</mo><mi>g</mi><mo>,</mo><mi>h</mi><mo stretchy="false">)</mo><mo>⊢</mo><mo stretchy="false">(</mo><mi>s</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo>=</mo><mi>t</mi><mo stretchy="false">(</mo><mi>g</mi><mo stretchy="false">)</mo><mo>∧</mo><mi>t</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo>=</mo><mi>t</mi><mo stretchy="false">(</mo><mi>h</mi><mo stretchy="false">)</mo><mo>∧</mo><mi>s</mi><mo stretchy="false">(</mo><mi>g</mi><mo stretchy="false">)</mo><mo>=</mo><mi>s</mi><mo stretchy="false">(</mo><mi>h</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">c(f, g, h) \vdash (s(f) = t(g) \wedge t(f) = t(h) \wedge s(g) = s(h))</annotation></semantics></math></p> </li> <li> <p><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo>=</mo><mi>t</mi><mo stretchy="false">(</mo><mi>g</mi><mo stretchy="false">)</mo><mo>⊢</mo><mo>∃</mo><msub><mo>!</mo> <mi>h</mi></msub><mi>c</mi><mo stretchy="false">(</mo><mi>f</mi><mo>,</mo><mi>g</mi><mo>,</mo><mi>h</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">s(f) = t(g) \vdash \exists !_h c(f, g, h)</annotation></semantics></math></p> </li> <li> <p>(<a class="existingWikiWord" href="/nlab/show/identity">Identity</a> laws) <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊢</mo><mi>c</mi><mo stretchy="false">(</mo><mi>f</mi><mo>,</mo><mi>s</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo>,</mo><mi>f</mi><mo stretchy="false">)</mo><mo>∧</mo><mi>c</mi><mo stretchy="false">(</mo><mi>t</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo>,</mo><mi>f</mi><mo>,</mo><mi>f</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\vdash c(f, s(f), f) \wedge c(t(f), f, f)</annotation></semantics></math></p> </li> <li> <p>(<a class="existingWikiWord" href="/nlab/show/associativity">Associativity</a>) <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>f</mi><mo>,</mo><mi>g</mi><mo>,</mo><mi>j</mi><mo stretchy="false">)</mo><mo>∧</mo><mi>c</mi><mo stretchy="false">(</mo><mi>g</mi><mo>,</mo><mi>h</mi><mo>,</mo><mi>k</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>⊢</mo><mo stretchy="false">(</mo><mi>c</mi><mo stretchy="false">(</mo><mi>j</mi><mo>,</mo><mi>h</mi><mo>,</mo><mi>m</mi><mo stretchy="false">)</mo><mo>⇔</mo><mi>c</mi><mo stretchy="false">(</mo><mi>f</mi><mo>,</mo><mi>k</mi><mo>,</mo><mi>m</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(c(f, g, j) \wedge c(g, h, k)) \vdash (c(j, h, m) \Leftrightarrow c(f, k, m))</annotation></semantics></math></p> </li> </ol> <p>(Notice that an <strong>object-term</strong> may be defined as a term <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>e</mi></mrow><annotation encoding="application/x-tex">e</annotation></semantics></math> for which either of the following equivalent equations holds: <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>e</mi><mo>=</mo><mi>s</mi><mo stretchy="false">(</mo><mi>e</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">e = s(e)</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>e</mi><mo>=</mo><mi>t</mi><mo stretchy="false">(</mo><mi>e</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">e = t(e)</annotation></semantics></math>.)</p> </div> <h2 id="the_theory_of_finitely_complete_categories">The theory of finitely complete categories</h2> <div class="un_def"> <h6 id="definition_2">Definition</h6> <p>We define the <a class="existingWikiWord" href="/nlab/show/theory">theory</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Th</mi><mo stretchy="false">(</mo><mi>Lex</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Th(Lex)</annotation></semantics></math> of <a class="existingWikiWord" href="/nlab/show/finitely+complete+categories">finitely complete categories</a>.</p> <p>(The axioms say there is a <a class="existingWikiWord" href="/nlab/show/terminal+object">terminal object</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>1</mn></mrow><annotation encoding="application/x-tex">1</annotation></semantics></math>, and a <a class="existingWikiWord" href="/nlab/show/pullback">pullback</a> for each pair <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>,</mo><mi>g</mi></mrow><annotation encoding="application/x-tex">f, g</annotation></semantics></math> with common target.)</p> <p>The axioms of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Th</mi><mo stretchy="false">(</mo><mi>Lex</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Th(Lex)</annotation></semantics></math> are the axioms of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Th</mi><mo stretchy="false">(</mo><mi>Cat</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Th(Cat)</annotation></semantics></math> plus the following:</p> <ol> <li> <p><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mo>∃</mo> <mn>1</mn></msub><mo stretchy="false">(</mo><mn>1</mn><mo>=</mo><mi>s</mi><mo stretchy="false">(</mo><mn>1</mn><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>∧</mo><mo stretchy="false">(</mo><msub><mo>∀</mo> <mi>f</mi></msub><mo stretchy="false">(</mo><mi>f</mi><mo>=</mo><mi>s</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>⇒</mo><mo stretchy="false">(</mo><mo>∃</mo><mo>!</mo><mi>g</mi><mo>:</mo><mo stretchy="false">(</mo><mi>s</mi><mo stretchy="false">(</mo><mi>g</mi><mo stretchy="false">)</mo><mo>=</mo><mi>f</mi><mo>∧</mo><mi>t</mi><mo stretchy="false">(</mo><mi>g</mi><mo stretchy="false">)</mo><mo>=</mo><mn>1</mn><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\exists_1 (1 = s(1)) \wedge (\forall_f (f = s(f)) \Rightarrow (\exists ! g: (s(g) = f \wedge t(g) = 1))</annotation></semantics></math></p> </li> <li> <p>(Pullbacks exist) Define <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi><mo stretchy="false">(</mo><mi>f</mi><mo>,</mo><mi>g</mi><mo>,</mo><mi>h</mi><mo>,</mo><mi>k</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">p(f, g, h, k)</annotation></semantics></math> to be the conjunction of the formulas</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><msub><mo>∃</mo> <mi>j</mi></msub><mi>c</mi><mo stretchy="false">(</mo><mi>f</mi><mo>,</mo><mi>h</mi><mo>,</mo><mi>j</mi><mo stretchy="false">)</mo><mo>∧</mo><mi>c</mi><mo stretchy="false">(</mo><mi>g</mi><mo>,</mo><mi>k</mi><mo>,</mo><mi>j</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(\exists_j c(f, h, j) \wedge c(g, k, j))</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mspace width="thinmathspace"></mspace></mrow><annotation encoding="application/x-tex">\,</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><msub><mo>∃</mo> <mrow><mi>j</mi><mo>′</mo></mrow></msub><mo stretchy="false">(</mo><mi>c</mi><mo stretchy="false">(</mo><mi>f</mi><mo>,</mo><mi>h</mi><mo>′</mo><mo>,</mo><mi>j</mi><mo>′</mo><mo stretchy="false">)</mo><mo>∧</mo><mi>c</mi><mo stretchy="false">(</mo><mi>g</mi><mo>,</mo><mi>k</mi><mo>′</mo><mo>,</mo><mi>j</mi><mo>′</mo><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>⇒</mo><mo stretchy="false">(</mo><mo>∃</mo><mo>!</mo><mi>i</mi><mo>:</mo><mo stretchy="false">(</mo><mi>c</mi><mo stretchy="false">(</mo><mi>h</mi><mo>,</mo><mi>i</mi><mo>,</mo><mi>h</mi><mo>′</mo><mo stretchy="false">)</mo><mo>∧</mo><mi>c</mi><mo stretchy="false">(</mo><mi>k</mi><mo>,</mo><mi>i</mi><mo>,</mo><mi>k</mi><mo>′</mo><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(\exists_{j'} (c(f, h', j') \wedge c(g, k', j')) \Rightarrow (\exists ! i: (c(h, i, h') \wedge c(k, i, k')))</annotation></semantics></math></div> <p>Then</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>t</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo>=</mo><mi>t</mi><mo stretchy="false">(</mo><mi>g</mi><mo stretchy="false">)</mo><mo>⊢</mo><msub><mo>∃</mo> <mi>h</mi></msub><msub><mo>∃</mo> <mi>k</mi></msub><mi>p</mi><mo stretchy="false">(</mo><mi>f</mi><mo>,</mo><mi>g</mi><mo>,</mo><mi>h</mi><mo>,</mo><mi>k</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">t(f) = t(g) \vdash \exists_h \exists_k p(f, g, h, k)</annotation></semantics></math></div></li> </ol> </div> <h2 id="the_theory_of_elementary_toposes">The theory of elementary toposes</h2> <div class="un_def"> <h6 id="definition_3">Definition</h6> <p>We define the <a class="existingWikiWord" href="/nlab/show/theory">theory</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Th</mi><mo stretchy="false">(</mo><mi>Topos</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Th(Topos)</annotation></semantics></math> of <a class="existingWikiWord" href="/nlab/show/elementary+toposes">elementary toposes</a>.</p> <p>The signature of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Th</mi><mo stretchy="false">(</mo><mi>Topos</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Th(Topos)</annotation></semantics></math> is obtained by adding to the signature of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Th</mi><mo stretchy="false">(</mo><mi>Lex</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Th(Lex)</annotation></semantics></math> unary function symbols <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo>,</mo><mi>λ</mi><mo>,</mo><mi>ρ</mi></mrow><annotation encoding="application/x-tex">P, \lambda, \rho</annotation></semantics></math>.</p> <p>(The intended interpretation is that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo stretchy="false">(</mo><mi>f</mi><mo>:</mo><mi>X</mi><mo>→</mo><mi>Y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">P(f: X \to Y)</annotation></semantics></math> is the <a class="existingWikiWord" href="/nlab/show/power+object">power object</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Y</mi></mrow><annotation encoding="application/x-tex">Y</annotation></semantics></math>, and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">⟨</mo><mi>λ</mi><mo stretchy="false">(</mo><mi>Y</mi><mo stretchy="false">)</mo><mo>,</mo><mi>ρ</mi><mo stretchy="false">(</mo><mi>Y</mi><mo stretchy="false">)</mo><mo stretchy="false">⟩</mo><mo>:</mo><mi>E</mi><mo stretchy="false">(</mo><mi>Y</mi><mo stretchy="false">)</mo><mo>↪</mo><mi>P</mi><mo stretchy="false">(</mo><mi>Y</mi><mo stretchy="false">)</mo><mo>×</mo><mi>Y</mi></mrow><annotation encoding="application/x-tex">\langle \lambda(Y), \rho(Y) \rangle: E(Y) \hookrightarrow P(Y) \times Y</annotation></semantics></math> is the elementhood relation, which we rewrite as a jointly <a class="existingWikiWord" href="/nlab/show/monomorphism">monic</a> <a class="existingWikiWord" href="/nlab/show/span">span</a>, and consider as a <a class="existingWikiWord" href="/nlab/show/universal+property">universal</a> relation from <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo stretchy="false">(</mo><mi>Y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">P(Y)</annotation></semantics></math> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Y</mi></mrow><annotation encoding="application/x-tex">Y</annotation></semantics></math>.)</p> <p>The axioms of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Th</mi><mo stretchy="false">(</mo><mi>Topos</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Th(Topos)</annotation></semantics></math> are obtained by adjoining to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Th</mi><mo stretchy="false">(</mo><mi>Lex</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Th(Lex)</annotation></semantics></math> the following further axioms. In what follows, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>M</mi><mo stretchy="false">(</mo><mi>f</mi><mo>,</mo><mi>g</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">M(f, g)</annotation></semantics></math> denote the following formula in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Th</mi><mo stretchy="false">(</mo><mi>Cat</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Th(Cat)</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>s</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo>=</mo><mi>s</mi><mo stretchy="false">(</mo><mi>g</mi><mo stretchy="false">)</mo><mo>∧</mo><mo stretchy="false">(</mo><msub><mo>∀</mo> <mrow><mi>h</mi><mo>,</mo><mi>i</mi><mo>,</mo><mi>j</mi><mo>,</mo><mi>k</mi></mrow></msub><mo stretchy="false">(</mo><mi>c</mi><mo stretchy="false">(</mo><mi>f</mi><mo>,</mo><mi>h</mi><mo>,</mo><mi>j</mi><mo stretchy="false">)</mo><mo>∧</mo><mi>c</mi><mo stretchy="false">(</mo><mi>f</mi><mo>,</mo><mi>i</mi><mo>,</mo><mi>j</mi><mo stretchy="false">)</mo><mo>∧</mo><mi>c</mi><mo stretchy="false">(</mo><mi>g</mi><mo>,</mo><mi>h</mi><mo>,</mo><mi>k</mi><mo stretchy="false">)</mo><mo>∧</mo><mi>c</mi><mo stretchy="false">(</mo><mi>g</mi><mo>,</mo><mi>i</mi><mo>,</mo><mi>k</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>⇒</mo><mi>h</mi><mo>=</mo><mi>i</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">s(f) = s(g) \wedge (\forall_{h, i, j, k} (c(f, h, j) \wedge c(f, i, j) \wedge c(g, h, k) \wedge c(g, i, k)) \Rightarrow h = i)</annotation></semantics></math></div> <p>(<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>M</mi><mo stretchy="false">(</mo><mi>f</mi><mo>,</mo><mi>g</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">M(f, g)</annotation></semantics></math> means that the pair <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>f</mi><mo>,</mo><mi>g</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(f, g)</annotation></semantics></math> is a jointly monic span, aka a relation. In other words, that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">⟨</mo><mi>f</mi><mo>,</mo><mi>g</mi><mo stretchy="false">⟩</mo><mo lspace="verythinmathspace">:</mo><mi>s</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo>→</mo><mi>t</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo>×</mo><mi>t</mi><mo stretchy="false">(</mo><mi>g</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\langle f, g \rangle \colon s(f) \to t(f) \times t(g)</annotation></semantics></math> is monic, and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>f</mi><mo>,</mo><mi>g</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(f, g)</annotation></semantics></math> form a relation between <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>t</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">t(f)</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>t</mi><mo stretchy="false">(</mo><mi>g</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">t(g)</annotation></semantics></math>.)</p> <ol> <li> <p>(<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo stretchy="false">(</mo><mi>f</mi><mo>:</mo><mi>X</mi><mo>→</mo><mi>Y</mi><mo stretchy="false">)</mo><mo>=</mo><mi>P</mi><mo stretchy="false">(</mo><mi>Y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">P(f: X \to Y) = P(Y)</annotation></semantics></math> is an object that depends only on the codomain of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi></mrow><annotation encoding="application/x-tex">f</annotation></semantics></math>, and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>λ</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo>,</mo><mi>ρ</mi></mrow><annotation encoding="application/x-tex">\lambda(f), \rho</annotation></semantics></math> are morphisms that span between <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo stretchy="false">(</mo><mi>Y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">P(Y)</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Y</mi></mrow><annotation encoding="application/x-tex">Y</annotation></semantics></math>, comprising a local elementhood relation)</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo>⊢</mo><mo stretchy="false">(</mo><mi>P</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo>=</mo><mi>P</mi><mo stretchy="false">(</mo><mi>t</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>=</mo><mi>t</mi><mo stretchy="false">(</mo><mi>P</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>=</mo><mi>t</mi><mo stretchy="false">(</mo><mi>λ</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>∧</mo><mo stretchy="false">(</mo><mi>t</mi><mo stretchy="false">(</mo><mi>ρ</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>=</mo><mi>t</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\vdash (P(f) = P(t(f)) = t(P(f)) = t(\lambda(f))) \wedge (t(\rho(f)) = t(f))</annotation></semantics></math></div></li> <li> <p><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊢</mo><mi>M</mi><mo stretchy="false">(</mo><mi>λ</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo>,</mo><mi>ρ</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\vdash M(\lambda(f), \rho(f))</annotation></semantics></math></p> </li> <li> <p>(Universal property of power objects)</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>M</mi><mo stretchy="false">(</mo><mi>f</mi><mo>,</mo><mi>g</mi><mo stretchy="false">)</mo><mo>⊢</mo><mo>∃</mo><mo>!</mo><mi>h</mi><mo>:</mo><msub><mo>∃</mo> <mi>k</mi></msub><mi>p</mi><mo stretchy="false">(</mo><mi>h</mi><mo>,</mo><mi>λ</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo>,</mo><mi>g</mi><mo>,</mo><mi>k</mi><mo stretchy="false">)</mo><mo>∧</mo><mi>c</mi><mo stretchy="false">(</mo><mi>ρ</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo>,</mo><mi>k</mi><mo>,</mo><mi>f</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">M(f, g) \vdash \exists ! h: \exists_k p(h, \lambda(f), g, k) \wedge c(\rho(f), k, f)</annotation></semantics></math></div></li> </ol> </div> <h2 id="the_theory_etcs">The theory ETCS</h2> <div class="un_def"> <h6 id="definition_4">Definition</h6> <p>Finally, we define the <a class="existingWikiWord" href="/nlab/show/theory">theory</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Th</mi><mo stretchy="false">(</mo><mi>ETCS</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Th(ETCS)</annotation></semantics></math>: <a class="existingWikiWord" href="/nlab/show/ETCS">ETCS</a>.</p> <p>The signature of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Th</mi><mo stretchy="false">(</mo><mi>ETCS</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Th(ETCS)</annotation></semantics></math> is obtained by adjoining to the signature of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Th</mi><mo stretchy="false">(</mo><mi>Topos</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Th(Topos)</annotation></semantics></math> the following</p> <ul> <li>Nullary function symbols (i.e., constants) <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℕ</mi><mo>,</mo><mn>0</mn><mo>,</mo><mi>σ</mi></mrow><annotation encoding="application/x-tex">\mathbb{N}, 0, \sigma</annotation></semantics></math>.</li> </ul> <p>The axioms of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Th</mi><mo stretchy="false">(</mo><mi>ETCS</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Th(ETCS)</annotation></semantics></math> are obtained by adjoining to the axioms of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Th</mi><mo stretchy="false">(</mo><mi>Topos</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Th(Topos)</annotation></semantics></math> the following further axioms:</p> <ol> <li> <p>(<a class="existingWikiWord" href="/nlab/show/well-pointed+topos">Well-pointedness</a>: equality of maps <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>→</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">x \to y</annotation></semantics></math> is detected by points <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>1</mn><mo>→</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">1 \to x</annotation></semantics></math>)</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>s</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo>=</mo><mi>s</mi><mo stretchy="false">(</mo><mi>g</mi><mo stretchy="false">)</mo><mo>∧</mo><mi>t</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo>=</mo><mi>t</mi><mo stretchy="false">(</mo><mi>g</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>⊢</mo><msub><mo>∀</mo> <mi>h</mi></msub><mo stretchy="false">(</mo><mi>s</mi><mo stretchy="false">(</mo><mi>h</mi><mo stretchy="false">)</mo><mo>=</mo><mn>1</mn><mo>∧</mo><mi>t</mi><mo stretchy="false">(</mo><mi>h</mi><mo stretchy="false">)</mo><mo>=</mo><mi>s</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo>⇒</mo><mi>f</mi><mo>∘</mo><mi>h</mi><mo>=</mo><mi>g</mi><mo>∘</mo><mi>h</mi><mo stretchy="false">)</mo><mo>⇒</mo><mi>f</mi><mo>=</mo><mi>g</mi></mrow><annotation encoding="application/x-tex">(s(f) = s(g) \wedge t(f) = t(g)) \vdash \forall_h (s(h) = 1 \wedge t(h) = s(f) \Rightarrow f \circ h = g \circ h) \Rightarrow f = g</annotation></semantics></math></div></li> <li> <p>(<a class="existingWikiWord" href="/nlab/show/axiom+of+choice">Axiom of Choice</a>: every epi <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi></mrow><annotation encoding="application/x-tex">f</annotation></semantics></math> admits a section <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>i</mi></mrow><annotation encoding="application/x-tex">i</annotation></semantics></math>)</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><msub><mo>∀</mo> <mrow><mi>g</mi><mo>,</mo><mi>h</mi></mrow></msub><mo stretchy="false">(</mo><mi>t</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo>=</mo><mi>s</mi><mo stretchy="false">(</mo><mi>g</mi><mo stretchy="false">)</mo><mo>=</mo><mi>s</mi><mo stretchy="false">(</mo><mi>h</mi><mo stretchy="false">)</mo><mspace width="thickmathspace"></mspace><mo>∧</mo><mspace width="thickmathspace"></mspace><mi>t</mi><mo stretchy="false">(</mo><mi>g</mi><mo stretchy="false">)</mo><mo>=</mo><mi>t</mi><mo stretchy="false">(</mo><mi>h</mi><mo stretchy="false">)</mo><mspace width="thickmathspace"></mspace><mo>∧</mo><mspace width="thickmathspace"></mspace><mi>g</mi><mo>∘</mo><mi>f</mi><mo>=</mo><mi>h</mi><mo>∘</mo><mi>f</mi><mo stretchy="false">)</mo><mspace width="thickmathspace"></mspace><mo>⇒</mo><mspace width="thickmathspace"></mspace><mi>g</mi><mo>=</mo><mi>h</mi><mo stretchy="false">)</mo><mo>⊢</mo><msub><mo>∃</mo> <mi>i</mi></msub><mo stretchy="false">(</mo><mi>s</mi><mo stretchy="false">(</mo><mi>i</mi><mo stretchy="false">)</mo><mo>=</mo><mi>t</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mspace width="thickmathspace"></mspace><mo>∧</mo><mspace width="thickmathspace"></mspace><mi>t</mi><mo stretchy="false">(</mo><mi>i</mi><mo stretchy="false">)</mo><mo>=</mo><mi>s</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mspace width="thickmathspace"></mspace><mo>∧</mo><mspace width="thickmathspace"></mspace><mi>f</mi><mo>∘</mo><mi>i</mi><mo>=</mo><mi>t</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(\forall_{g, h} (t(f) = s(g) = s(h) \;\wedge\; t(g) = t(h) \;\wedge\; g \circ f = h \circ f) \;\Rightarrow\; g = h) \vdash \exists_i (s(i) = t(f) \;\wedge\; t(i) = s(f) \;\wedge\; f \circ i = t(f))</annotation></semantics></math></div></li> <li> <p>(<a class="existingWikiWord" href="/nlab/show/natural+numbers+object">Zero and successor</a>)</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo>⊢</mo><mi>s</mi><mo stretchy="false">(</mo><mn>0</mn><mo stretchy="false">)</mo><mo>=</mo><mn>1</mn><mo>∧</mo><mi>t</mi><mo stretchy="false">(</mo><mn>0</mn><mo stretchy="false">)</mo><mo>=</mo><mi>ℕ</mi><mo>=</mo><mi>s</mi><mo stretchy="false">(</mo><mi>σ</mi><mo stretchy="false">)</mo><mo>=</mo><mi>t</mi><mo stretchy="false">(</mo><mi>σ</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\vdash s(0) = 1 \wedge t(0) = \mathbb{N} = s(\sigma) = t(\sigma)</annotation></semantics></math></div></li> <li> <p>(<a class="existingWikiWord" href="/nlab/show/natural+numbers+object">Recursion: existence</a>)</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>s</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo>=</mo><mn>1</mn><mo>∧</mo><mi>t</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo>=</mo><mi>s</mi><mo stretchy="false">(</mo><mi>g</mi><mo stretchy="false">)</mo><mo>=</mo><mi>t</mi><mo stretchy="false">(</mo><mi>g</mi><mo stretchy="false">)</mo><mo>⊢</mo><msub><mo>∃</mo> <mi>h</mi></msub><mo stretchy="false">(</mo><mi>s</mi><mo stretchy="false">(</mo><mi>h</mi><mo stretchy="false">)</mo><mo>=</mo><mi>ℕ</mi><mo>∧</mo><mi>t</mi><mo stretchy="false">(</mo><mi>h</mi><mo stretchy="false">)</mo><mo>=</mo><mi>t</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo>∧</mo><mi>f</mi><mo>=</mo><mi>h</mi><mo>∘</mo><mn>0</mn><mo>∧</mo><mi>h</mi><mo>∘</mo><mi>σ</mi><mo>=</mo><mi>g</mi><mo>∘</mo><mi>h</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">s(f) = 1 \wedge t(f) = s(g) = t(g) \vdash \exists_h (s(h) = \mathbb{N} \wedge t(h) = t(f) \wedge f = h \circ 0 \wedge h \circ \sigma = g \circ h)</annotation></semantics></math></div></li> <li> <p>(Recursion: uniqueness)</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>s</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo>=</mo><mi>ℕ</mi><mo>=</mo><mi>s</mi><mo stretchy="false">(</mo><mi>g</mi><mo stretchy="false">)</mo><mo>∧</mo><mi>t</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo>=</mo><mi>t</mi><mo stretchy="false">(</mo><mi>g</mi><mo stretchy="false">)</mo><mo>∧</mo><mi>f</mi><mo>∘</mo><mn>0</mn><mo>=</mo><mi>g</mi><mo>∘</mo><mn>0</mn><mo>∧</mo><mi>f</mi><mo>∘</mo><mi>σ</mi><mo>=</mo><mi>g</mi><mo>∘</mo><mi>σ</mi><mo stretchy="false">)</mo><mo>⊢</mo><mi>f</mi><mo>=</mo><mi>g</mi></mrow><annotation encoding="application/x-tex">(s(f) = \mathbb{N} = s(g) \wedge t(f) = t(g) \wedge f \circ 0 = g \circ 0 \wedge f \circ \sigma = g \circ \sigma) \vdash f = g</annotation></semantics></math></div></li> </ol> <p>This completes the formal specification of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Th</mi><mo stretchy="false">(</mo><mi>ETCS</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Th(ETCS)</annotation></semantics></math>.</p> </div> <h2 id="remarks">Remarks</h2> <h3 id="on_">On <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Th</mi><mo stretchy="false">(</mo><mi>Cat</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Th(Cat)</annotation></semantics></math></h3> <p>The theory of categories is usually presented as a two-sorted theory, where the sorts <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>O</mi></mrow><annotation encoding="application/x-tex">O</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>M</mi></mrow><annotation encoding="application/x-tex">M</annotation></semantics></math> are for objects and morphisms.</p> <p>Despite the length of the list of axioms, it should be noted that they generally have an extremely simple logical structure. Indeed, with some slight modification, the theory <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Th</mi><mo stretchy="false">(</mo><mi>Topos</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Th(Topos)</annotation></semantics></math> may be rewritten so that it becomes an <a class="existingWikiWord" href="/nlab/show/essentially+algebraic+theory">essentially algebraic theory</a>, at least in the sense that the models of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Th</mi><mo stretchy="false">(</mo><mi>Topos</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Th(Topos)</annotation></semantics></math> are categorially equivalent (as categories = models of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Th</mi><mo stretchy="false">(</mo><mi>Cat</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Th(Cat)</annotation></semantics></math>) to models of an essentially algebraic theory. That is to say, the notion of “topos” can be <a class="existingWikiWord" href="/nlab/show/internalization">internalized</a> in any category with finite limits; this is even true of toposes with natural numbers object.</p> <p>Hence, the only “irremovable” existential clauses (that necessitate passing from essentially algebraic logic to a larger fragment of first-order logic) are well-pointedness and the axiom of choice. The axiom of choice belongs to <a class="existingWikiWord" href="/nlab/show/geometric+logic">geometric logic</a>.</p> <p>This is in marked contrast to ZFC, whose axiom list is superficially shorter (ignoring the fact that axiom schemas are technically infinite lists of axioms!) but whose logical complexity is much greater.</p> <p>It must be added that this fully formal presentation masks much of the conceptual clarity afforded by the underlying categorical and structural insights that are actually at work, particularly the systematic use of universal mapping properties. To put it more sharply: the traditional syntactic machinery used to present first-order theories is not really a natural or well-adapted ‘home’ for presenting categorical theories such as ETCS. The natural mode of presentation would use diagrams of arrows from the outset, as formalized say by Freyd’s <span class="newWikiWord">Q-sequence<a href="/nlab/new/Q-sequence">?</a></span>s, and that is as fully formal as the more traditional mode adopted here, which after all goes back to Frege and hasn’t changed in a century.</p> <h2 id="references">References</h2> <p>Over the years various people at</p> <ul id="FOM"> <li><em>Foundations of Mathematics</em> <a href="http://www.math.psu.edu/simpson/fom/">mailing list</a> (around 1998)</li> </ul> <p>have challenged <a class="existingWikiWord" href="/nlab/show/category+theory">category theorists</a> to write down a fully formal presentation of ETCS.</p> <p>note1: Note how cumbersome are the traditional “machine-level” logical scripts for expressing this theory, as opposed to the more visual and easily apprehended arrow-theoretic notations (which are just as rigorous). No doubt this was anticipated by those in the FOM debate who wished to portray categorical foundations in the worst possible light: traditional 1-dimensional logical notations tend to make the theory look as clumsy as possible!</p> <p>note2: We use <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> to denote an entailment between formulas; axioms of our theory are written in the form <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>⊢</mo><mi>P</mi></mrow><annotation encoding="application/x-tex">\Gamma \vdash P</annotation></semantics></math> where <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi></mrow><annotation encoding="application/x-tex">\Gamma</annotation></semantics></math> is a finite, possibly empty list of formulas which provide the <em>context</em> in which <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math> is asserted. Obviously one could eschew this symbol entirely, and instead give each axiom in the form of a single formula with appropriately embedded implication symbols <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⇒</mo></mrow><annotation encoding="application/x-tex">\Rightarrow</annotation></semantics></math>. But, as explained in this article, this would obscure the later point that large fragments of ETCS, in fact all axioms except well-pointedness, are manifestly expressible in <em>coherent logic</em>.</p> </body></html> </div> <div class="revisedby"> <p> Last revised on April 3, 2016 at 08:53:34. See the <a href="/nlab/history/fully+formal+ETCS" 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/fully+formal+ETCS" accesskey="E" class="navlink" id="edit" rel="nofollow">Edit</a><a href="https://nforum.ncatlab.org/discussions/?CategoryID=0">Discuss</a><span class="backintime"><a href="/nlab/revision/fully+formal+ETCS/30" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/diff/fully+formal+ETCS" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Changes from previous revision</a><a href="/nlab/history/fully+formal+ETCS" accesskey="S" class="navlink" id="history" rel="nofollow">History (30 revisions)</a> <a href="/nlab/show/fully+formal+ETCS/cite" style="color: black">Cite</a> <a href="/nlab/print/fully+formal+ETCS" accesskey="p" id="view_print" rel="nofollow">Print</a> <a href="/nlab/source/fully+formal+ETCS" id="view_source" rel="nofollow">Source</a> </div> </div>  </div>  </body> </html>