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> 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> 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/discussion/8582/#Item_10" title="Discuss this page in its dedicated thread on the nForum" style="color: black">Discuss this page</a> | <form accept-charset="utf-8" action="/nlab/search" id="navigationSearchForm" method="get"> <fieldset class="search"><input type="text" id="searchField" name="query" value="Search" style="display:inline-block; float: left;" onfocus="this.value == 'Search' ? this.value = '' : true" onblur="this.value == '' ? this.value = 'Search' : true" /></fieldset> </form> <span id='navEnd'></span> </div> <div id="revision"> <html xmlns="http://www.w3.org/1999/xhtml" xmlns:svg="http://www.w3.org/2000/svg" xml:lang="en" lang="en"> <head><meta http-equiv="Content-type" content="application/xhtml+xml;charset=utf-8" /><title>Contents</title></head> <body> <div class="rightHandSide"> <div class="toc clickDown" tabindex="0"> <h3 id="context">Context</h3> <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="toc_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> <h4 id="foundations">Foundations</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/foundations">foundations</a></strong></p> <h2 id="the_basis_of_it_all">The basis of it all</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/mathematical+logic">mathematical logic</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/deduction+system">deduction system</a>, <a class="existingWikiWord" href="/nlab/show/natural+deduction">natural deduction</a>, <a class="existingWikiWord" href="/nlab/show/sequent+calculus">sequent calculus</a>, <a class="existingWikiWord" href="/nlab/show/lambda-calculus">lambda-calculus</a>, <a class="existingWikiWord" href="/nlab/show/judgment">judgment</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a>, <a class="existingWikiWord" href="/nlab/show/simple+type+theory">simple type theory</a>, <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/collection">collection</a>, <a class="existingWikiWord" href="/nlab/show/object">object</a>, <a class="existingWikiWord" href="/nlab/show/type">type</a>, <a class="existingWikiWord" href="/nlab/show/term">term</a>, <a class="existingWikiWord" href="/nlab/show/set">set</a>, <a class="existingWikiWord" href="/nlab/show/element">element</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/equality">equality</a>, <a class="existingWikiWord" href="/nlab/show/judgmental+equality">judgmental equality</a>, <a class="existingWikiWord" href="/nlab/show/typal+equality">typal equality</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/universe">universe</a>, <a class="existingWikiWord" href="/nlab/show/size+issues">size issues</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/higher-order+logic">higher-order logic</a></p> </li> </ul> <h2 id="set_theory"> Set theory</h2> <div> <p><strong><a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a></strong></p> <ul> <li>fundamentals of set theory <ul> <li><a class="existingWikiWord" href="/nlab/show/propositional+logic">propositional logic</a></li> <li><a class="existingWikiWord" href="/nlab/show/first-order+logic">first-order logic</a></li> <li><a class="existingWikiWord" href="/nlab/show/typed+predicate+logic">typed predicate logic</a></li> <li><a class="existingWikiWord" href="/nlab/show/membership+relation">membership relation</a></li> <li><a class="existingWikiWord" href="/nlab/show/propositional+equality">propositional equality</a></li> <li><a class="existingWikiWord" href="/nlab/show/set">set</a>, <a class="existingWikiWord" href="/nlab/show/element">element</a>, <a class="existingWikiWord" href="/nlab/show/function">function</a>, <a class="existingWikiWord" href="/nlab/show/relation">relation</a></li> <li><a class="existingWikiWord" href="/nlab/show/universe">universe</a>, <a class="existingWikiWord" href="/nlab/show/small+set">small set</a>, <a class="existingWikiWord" href="/nlab/show/large+set">large set</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/material+set+theory">material set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/membership+relation">membership relation</a>, <a class="existingWikiWord" href="/nlab/show/propositional+equality">propositional equality</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+extensionality">axiom of extensionality</a></li> <li><a class="existingWikiWord" href="/nlab/show/pairing+structure">pairing structure</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+pairing">axiom of pairing</a></li> <li><a class="existingWikiWord" href="/nlab/show/union+structure">union structure</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+union">axiom of union</a></li> <li><a class="existingWikiWord" href="/nlab/show/powerset+structure">powerset structure</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+power+sets">axiom of power sets</a></li> <li><a class="existingWikiWord" href="/nlab/show/natural+numbers+structure">natural numbers structure</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+infinity">axiom of infinity</a></li> </ul> </li> <li>presentations of set theory <ul> <li><a class="existingWikiWord" href="/nlab/show/first-order+set+theory">first-order set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/unsorted+set+theory">unsorted set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/simply+sorted+set+theory">simply sorted set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/one-sorted+set+theory">one-sorted set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/two-sorted+set+theory">two-sorted set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/three-sorted+set+theory">three-sorted set theory</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/dependently+sorted+set+theory">dependently sorted set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/structurally+presented+set+theory">structurally presented set theory</a></li> </ul> </li> <li>structuralism in set theory <ul> <li><a class="existingWikiWord" href="/nlab/show/material+set+theory">material set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/ZFC">ZFC</a></li> <li><a class="existingWikiWord" href="/nlab/show/ZFA">ZFA</a></li> <li><a class="existingWikiWord" href="/nlab/show/Mostowski+set+theory">Mostowski set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/New+Foundations">New Foundations</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/structural+set+theory">structural set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/categorical+set+theory">categorical set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/ETCS">ETCS</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/fully+formal+ETCS">fully formal ETCS</a></li> <li><a class="existingWikiWord" href="/nlab/show/ETCS+with+elements">ETCS with elements</a></li> <li><a class="existingWikiWord" href="/nlab/show/Trimble+on+ETCS+I">Trimble on ETCS I</a></li> <li><a class="existingWikiWord" href="/nlab/show/Trimble+on+ETCS+II">Trimble on ETCS II</a></li> <li><a class="existingWikiWord" href="/nlab/show/Trimble+on+ETCS+III">Trimble on ETCS III</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/structural+ZFC">structural ZFC</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/allegorical+set+theory">allegorical set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/SEAR">SEAR</a></li> </ul> </li> </ul> </li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/class-set+theory">class-set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/class">class</a>, <a class="existingWikiWord" href="/nlab/show/proper+class">proper class</a></li> <li><a class="existingWikiWord" href="/nlab/show/universal+class">universal class</a>, <a class="existingWikiWord" href="/nlab/show/universe">universe</a></li> <li><a class="existingWikiWord" href="/nlab/show/category+of+classes">category of classes</a></li> <li><a class="existingWikiWord" href="/nlab/show/category+with+class+structure">category with class structure</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/constructive+set+theory">constructive set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/algebraic+set+theory">algebraic set theory</a></li> </ul> </div> <h2 id="foundational_axioms">Foundational axioms</h2> <div> <p><strong><a class="existingWikiWord" href="/nlab/show/foundational+axiom">foundational</a> <a class="existingWikiWord" href="/nlab/show/axioms">axioms</a></strong></p> <ul> <li> <p>basic constructions:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+cartesian+products">axiom of cartesian products</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+disjoint+unions">axiom of disjoint unions</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+the+empty+set">axiom of the empty set</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+fullness">axiom of fullness</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+function+sets">axiom of function sets</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+power+sets">axiom of power sets</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+quotient+sets">axiom of quotient sets</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/material+set+theory">material axioms</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+extensionality">axiom of extensionality</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+foundation">axiom of foundation</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+anti-foundation">axiom of anti-foundation</a></li> <li><a class="existingWikiWord" href="/nlab/show/Mostowski%27s+axiom">Mostowski's axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+pairing">axiom of pairing</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+transitive+closure">axiom of transitive closure</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+union">axiom of union</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/structural+set+theory">structural axioms</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+materialization">axiom of materialization</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/type+theory">type theoretic axioms</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axioms+of+set+truncation">axioms of set truncation</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/uniqueness+of+identity+proofs">uniqueness of identity proofs</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+K">axiom K</a></li> <li><a class="existingWikiWord" href="/nlab/show/boundary+separation">boundary separation</a></li> <li><a class="existingWikiWord" href="/nlab/show/equality+reflection">equality reflection</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+circle+type+localization">axiom of circle type localization</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theoretic axioms</a>: <ul> <li><a class="existingWikiWord" href="/nlab/show/univalence+axiom">univalence axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/Whitehead%27s+principle">Whitehead's principle</a></li> </ul> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/axioms+of+choice">axioms of choice</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+countable+choice">axiom of countable choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+dependent+choice">axiom of dependent choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+excluded+middle">axiom of excluded middle</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+existence">axiom of existence</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+multiple+choice">axiom of multiple choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/Markov%27s+axiom">Markov's axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/presentation+axiom">presentation axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/small+cardinality+selection+axiom">small cardinality selection axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+small+violations+of+choice">axiom of small violations of choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+weakly+initial+sets+of+covers">axiom of weakly initial sets of covers</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/large+cardinal+axioms">large cardinal axioms</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+infinity">axiom of infinity</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+universes">axiom of universes</a></li> <li><a class="existingWikiWord" href="/nlab/show/regular+extension+axiom">regular extension axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/inaccessible+cardinal">inaccessible cardinal</a></li> <li><a class="existingWikiWord" href="/nlab/show/measurable+cardinal">measurable cardinal</a></li> <li><a class="existingWikiWord" href="/nlab/show/elementary+embedding">elementary embedding</a></li> <li><a class="existingWikiWord" href="/nlab/show/supercompact+cardinal">supercompact cardinal</a></li> <li><a class="existingWikiWord" href="/nlab/show/Vop%C4%9Bnka%27s+principle">Vopěnka's principle</a></li> </ul> </li> <li> <p>strong axioms</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+separation">axiom of separation</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+replacement">axiom of replacement</a></li> </ul> </li> <li> <p>further</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/reflection+principle">reflection principle</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/axiom+of+tight+apartness">axiom of tight apartness</a></p> </li> </ul> </div> <h2 id="removing_axioms">Removing axioms</h2> <ul> <li><a class="existingWikiWord" href="/nlab/show/constructive+mathematics">constructive mathematics</a></li> <li><a class="existingWikiWord" href="/nlab/show/predicative+mathematics">predicative mathematics</a></li> </ul> <div> <p> <a href="/nlab/edit/foundations+-+contents">Edit this sidebar</a> </p> </div></div></div> </div> </div> <h1 id="contents">Contents</h1> <div class='maruku_toc'> <ul> <li><a href='#idea'>Idea</a></li> <li><a href='#definition'>Definition</a></li> <li><a href='#a_constructive_view'>A constructive view</a></li> <li><a href='#a_contemporary_perspective'>A contemporary perspective</a></li> <li><a href='#ExpositionByTrimble'>Todd Trimble’s exposition of ETCS</a></li> <li><a href='#related_entries'>Related entries</a></li> <li><a href='#references'>References</a></li> </ul> </div> <h2 id="idea">Idea</h2> <p>The <strong>Elementary Theory of the Category of Sets</strong>, or <em>ETCS</em> for short, is an axiomatic formulation of <a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a> in a <a class="existingWikiWord" href="/nlab/show/category+theory">category-theoretic</a> spirit. As such, it is the prototypical <a class="existingWikiWord" href="/nlab/show/structural+set+theory">structural set theory</a>. Proposed shortly after <a class="existingWikiWord" href="/nlab/show/ETCC">ETCC</a> in (<a href="#Lawvere64">Lawvere 64</a>) it is also the paradigm for a <a class="existingWikiWord" href="/nlab/show/foundations">categorical foundation</a> of mathematics.<sup id="fnref:1"><a href="#fn:1" rel="footnote">1</a></sup></p> <p>The theory intends to capture in an invariant way the notion of a (constant) <em>‘abstract set’</em> whose elements lack internal structure and whose only external property is cardinality with further external relations arising from <em>mappings</em>. The membership relation is <em>local</em> and <em>relative</em> i.e. membership is meaningful only between an element of a set and a subset of the very same set. (See <a href="#Lawvere76">Lawvere (1976, p.119)</a> for a detailed description of the notion ‘abstract set’.<sup id="fnref:2"><a href="#fn:2" rel="footnote">2</a></sup> <sup id="fnref:3"><a href="#fn:3" rel="footnote">3</a></sup> <sup id="fnref:4"><a href="#fn:4" rel="footnote">4</a></sup> <sup id="fnref:5"><a href="#fn:5" rel="footnote">5</a></sup>)</p> <p>More in detail, ETCS is a <a class="existingWikiWord" href="/nlab/show/first-order+theory">first-order theory</a> axiomatizing <a class="existingWikiWord" href="/nlab/show/elementary+toposes">elementary toposes</a> and specifically those which are <a class="existingWikiWord" href="/nlab/show/well-pointed+topos">well-pointed</a>, have a <a class="existingWikiWord" href="/nlab/show/natural+numbers+object">natural numbers object</a> and satisfy the <a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a>. The theory omits the <a class="existingWikiWord" href="/nlab/show/axiom+of+replacement">axiom of replacement</a>, however.</p> <p>The idea is, first of all, that much of traditional mathematics naturally takes place “<a class="existingWikiWord" href="/nlab/show/internal+logic">inside</a>” such a topos of <em>constant</em> sets, and second that this perspective generalizes beyond ETCS proper to toposes of <em>variable</em> and <em>cohesive</em> sets by varying the axioms: for instance omitting the <a class="existingWikiWord" href="/nlab/show/well-pointed+topos">well-pointedness</a> and the <a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a> but adding the <a class="existingWikiWord" href="/nlab/show/Kock-Lawvere+axiom">Kock-Lawvere axiom</a> gives a <a class="existingWikiWord" href="/nlab/show/smooth+topos">smooth topos</a> inside which <a class="existingWikiWord" href="/nlab/show/synthetic+differential+geometry">synthetic differential geometry</a> takes place.</p> <p>That is, ETCS locates the category of sets by the well-pointedness axiom as the discrete zero point on a ‘continuous’ range of toposes eligible for foundations. In particular, whereas ZF mainly provides ‘substance’ for mathematics, ETCS lives as a special type of form within the continuum of mathematical form itself.</p> <h2 id="definition">Definition</h2> <p>The axioms of ETCS can be summed up in one sentence as:</p> <div class="num_defn"> <h6 id="definition_2">Definition</h6> <p>The <a class="existingWikiWord" href="/nlab/show/Set">category of sets</a> is <a class="existingWikiWord" href="/nlab/show/generalized+the">the</a> <a class="existingWikiWord" href="/nlab/show/topos">topos</a> which</p> <ol> <li> <p>is a <a class="existingWikiWord" href="/nlab/show/well-pointed+topos">well-pointed topos</a></p> </li> <li> <p>has a <a class="existingWikiWord" href="/nlab/show/natural+numbers+object">natural numbers object</a></p> </li> <li> <p>and satisfies the <a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a>.</p> </li> </ol> </div> <p>For more details see</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/fully+formal+ETCS">fully formal ETCS</a>.</li> </ul> <h2 id="a_constructive_view">A constructive view</h2> <p><a class="existingWikiWord" href="/nlab/show/Erik+Palmgren">Erik Palmgren</a> (<a href="#Palmgren">Palmgren 2012</a>) has a <a class="existingWikiWord" href="/nlab/show/constructive+mathematics">constructive</a> <a class="existingWikiWord" href="/nlab/show/predicative+mathematics">predicative</a> variant of ETCS, which can be summarized as:</p> <p><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> is a <a class="existingWikiWord" href="/nlab/show/well-pointed+topos">well-pointed</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Π</mi></mrow><annotation encoding="application/x-tex">\Pi</annotation></semantics></math>-<a class="existingWikiWord" href="/nlab/show/%CE%A0-pretopos">pretopos</a> with a <a class="existingWikiWord" href="/nlab/show/NNO">NNO</a> and <a class="existingWikiWord" href="/nlab/show/enough+projectives">enough projectives</a> (i.e. <a class="existingWikiWord" href="/nlab/show/COSHEP">COSHEP</a> is satisfied). Here “well-pointed” must be taken in its constructive sense, as including that the <a class="existingWikiWord" href="/nlab/show/terminal+object">terminal object</a> is indecomposable and projective.</p> <h2 id="a_contemporary_perspective">A contemporary perspective</h2> <p>Modern mathematics with its emphasis on concepts from <a class="existingWikiWord" href="/nlab/show/homotopy+theory">homotopy theory</a> would more directly be founded in a similar spirit by an axiomatization not just of <a class="existingWikiWord" href="/nlab/show/elementary+toposes">elementary toposes</a> but of <a class="existingWikiWord" href="/nlab/show/elementary+%28%E2%88%9E%2C1%29-toposes">elementary (∞,1)-toposes</a>. This is roughly what <a class="existingWikiWord" href="/nlab/show/univalence">univalent</a> <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a> accomplishes – for more on this see at <em><a href="relation+between+type+theory+and+category+theory#HomotopyWithUnivalence">relation between type theory and category theory – Univalent HoTT and Elementary infinity-toposes</a></em>.</p> <p>Instead of increasing the <a class="existingWikiWord" href="/nlab/show/higher+category+theory">higher categorical dimension</a> <a class="existingWikiWord" href="/nlab/show/%28n%2Cr%29-category">(n,r)</a> in the first argument, one may also, in this context of elementary foundations, consider raising the second argument. The case <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mn>2</mn><mo>,</mo><mn>2</mn><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(2,2)</annotation></semantics></math> is the elementary theory of the 2-category of categories (<a class="existingWikiWord" href="/nlab/show/ETCC">ETCC</a>).</p> <h2 id="ExpositionByTrimble">Todd Trimble’s exposition of ETCS</h2> <p><a class="existingWikiWord" href="/nlab/show/Todd+Trimble">Todd Trimble</a> has a series of expository writings on ETCS which provide a very careful introduction and at the same time a wealth of useful details.</p> <ul> <li> <p>Todd Trimble, <em>ZFC and ETCS: Elementary Theory of the Category of Sets</em> (<a class="existingWikiWord" href="/nlab/show/Trimble+on+ETCS+I">nLab entry</a>, <a href="http://topologicalmusings.wordpress.com/2008/09/01/zfc-and-etcs-elementary-theory-of-the-category-of-sets/">original blog entry</a>)</p> </li> <li> <p>Todd Trimble, <em>ETCS: Internalizing the logic</em> (<a class="existingWikiWord" href="/nlab/show/Trimble+on+ETCS+II">nLab entry</a>, <a href="http://topologicalmusings.wordpress.com/2008/09/10/etcs-internalizing-the-logic/">original blog entry</a>)</p> </li> <li> <p>Todd Trimble, <em>ETCS: Building joins and coproducts</em> (<a class="existingWikiWord" href="/nlab/show/Trimble+on+ETCS+III">nLab entry</a>, <a href="http://topologicalmusings.wordpress.com/2008/12/15/etcs-building-joins-and-coproducts/">original blog entry</a>)</p> </li> </ul> <h2 id="related_entries">Related entries</h2> <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/structural+set+theory">structural set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/ZFC">Zermelo Fraenkel set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/Cohesive+Toposes+and+Cantor%27s+%22lauter+Einsen%22">Cohesive Toposes and Cantor's "lauter Einsen"</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+replacement">axiom of replacement</a></li> <li><a class="existingWikiWord" href="/nlab/show/ETCC">ETCC</a></li> <li><a class="existingWikiWord" href="/nlab/show/practical+foundations+of+mathematics">practical foundations of mathematics</a></li> <li><a class="existingWikiWord" href="/nlab/show/foundations+of+mathematics">foundations of mathematics</a></li> <li><a class="existingWikiWord" href="/nlab/show/ETCR">ETCR</a></li> <li><a class="existingWikiWord" href="/nlab/show/Mostowski+set+theory">Mostowski set theory</a></li> </ul> <h2 id="references">References</h2> <p>ETCS grew out of Lawvere’s experiences of teaching undergraduate foundations of analysis at Reed college in 1963 and was originally published in</p> <ul> <li id="Lawvere64"><a class="existingWikiWord" href="/nlab/show/William+Lawvere">William Lawvere</a>, <em>An elementary theory of the category of sets</em> , Proceedings of the National Academy of Science of the U.S.A <strong>52</strong> pp.1506-1511 (1964). (<a href="http://www.ncbi.nlm.nih.gov/pmc/articles/PMC300477/pdf/pnas00186-0196.pdf">pdf</a>)</li> </ul> <p>A more or less contemporary review is</p> <ul> <li>C.C. Elgot, <em>Review</em>, JSL <strong>37</strong> no.1 (1972) pp. 191-192.</li> </ul> <p>A longer version of Lawvere’s 1964 paper appears in</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/William+Lawvere">William Lawvere</a>, <a class="existingWikiWord" href="/nlab/show/Colin+McLarty">Colin McLarty</a>, <em>An elementary theory of the category of sets (long version) with commentary</em> , Reprints in Theory and Applications of Categories <strong>11</strong> (2005) pp. 1-35. (<a href="http://tac.mta.ca/tac/reprints/articles/11/tr11abs.html">TAC</a>)</li> </ul> <p>An undergraduate set-theory textbook using it is</p> <ul> <li id="LawvereRosebrugh"><a class="existingWikiWord" href="/nlab/show/William+Lawvere">William Lawvere</a>, <a class="existingWikiWord" href="/nlab/show/Robert+Rosebrugh">Robert Rosebrugh</a>, <em><a class="existingWikiWord" href="/nlab/show/Sets+for+Mathematics">Sets for Mathematics</a></em> , CUP 2003. (<a href="http://books.google.de/books?id=h3_7aZz9ZMoC&pg=PP1&dq=sets+for+mathematics">web</a>)</li> </ul> <p>Lawvere explains in detail his views on constant and variable ‘abstract sets’ on pp.118-128 of</p> <ul> <li id="Lawvere76"><a class="existingWikiWord" href="/nlab/show/William+Lawvere">William Lawvere</a>, <em>Variable Quantities and Variable Structures in Topoi</em> , pp.101-131 in Heller, Tierney (eds.), <em>Algebra, Topology and Category Theory: a Collection of Papers in Honor of Samuel Eilenberg</em> , Academic Press New York 1976.</li> </ul> <p>See also ch. 2,3 of</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/William+Lawvere">William Lawvere</a>, <em>Variable Sets Entendu and Variable Structure in Topoi</em> , lecture notes University of Chicago 1975.</li> </ul> <p>On the anticipation of ‘abstract sets’ in <a class="existingWikiWord" href="/nlab/show/Georg+Cantor">Cantor</a>:</p> <ul> <li id="Lawvere94"><a class="existingWikiWord" href="/nlab/show/William+Lawvere">William Lawvere</a>, <em><a class="existingWikiWord" href="/nlab/show/Cohesive+Toposes+and+Cantor%27s+%22lauter+Einsen%22">Cohesive Toposes and Cantor's "lauter Einsen"</a></em>, Philosophia Mathematica <strong>2</strong> no.3 (1994) pp.5-15. (<a class="existingWikiWord" href="/nlab/files/LawvereCohesiveToposes.pdf" title="pdf">pdf</a>)</li> </ul> <p>A short overview article on ETCS:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Tom+Leinster">Tom Leinster</a>, <em>Rethinking set theory</em> <a href="http://arxiv.org/abs/1212.6543">arXiv</a>.</li> </ul> <p>An insightful and non-partisan view of ETCS can be found in a section of:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Andreas+Blass">Andreas Blass</a>, Yuri Gurevich, <em>Why Sets ?</em> , Bull. Europ. Assoc. Theoret. Comp. Sci. <strong>84</strong> (2004) 139-156. (<a href="http://www.math.lsa.umich.edu/~ablass/set.pdf">draft</a>)</li> </ul> <p>An extended discussion from a philosophical perspective is in</p> <ul> <li id="McLarty04"> <p><a class="existingWikiWord" href="/nlab/show/Colin+McLarty">Colin McLarty</a>, <em>Exploring Categorical Structuralism</em> , Phil. Math. <strong>12</strong> (2004) 37-53.</p> </li> <li> <p>Øystein Linnebo, Richard Pettigrew, <em>Category theory as an autonomous foundation</em>, Phil. Math. <strong>19</strong> (2011) 227–254 (<a href="https://doi.org/10.1093/philmat/nkr024">doi:10.1093/philmat/nkr024</a>, <a href="http://philsci-archive.pitt.edu/5392/1/onlyuptoiso.pdf">preprint version (pdf)</a>)</p> </li> </ul> <p>For a more recent review from a critical perspective containing additional recent references see</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Solomon+Feferman">Solomon Feferman</a>, <em>Foundations of Unlimited Category Theory: What Remains to be Done</em> , Review of Symbolic Logic <strong>6</strong> no.1 (2013) 6-15. (<a href="http://math.stanford.edu/~feferman/papers/FCT-RSL-2013.pdf">pdf</a>)</li> </ul> <p>An informative discussion of the pros and cons of Lawvere’s approach can be found in</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Jean-Pierre+Marquis">Jean-Pierre Marquis</a>, <em>Kreisel and Lawvere on Category Theory and the Foundations of Mathematics</em> . (<a href="http://www.math.mcgill.ca/rags/seminar/Marquis_KreiselLawvere.pdf">pdf-slides</a>)</li> </ul> <p>Palmgren’s ideas can be found here:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Erik+Palmgren">Erik Palmgren</a>, <em>Constructivist and Structuralist Foundations: Bishop’s and Lawvere’s Theories of Sets</em>, Annals of Pure and Applied Logic <strong>163</strong> 10 (2012) 1384-1399 (2009) [<a href="https://doi.org/10.1016/j.apal.2012.01.011">doi:10.1016/j.apal.2012.01.011</a>, <a href="https://arxiv.org/abs/1201.6272">arXiv:1201.6272</a>]</li> </ul> <p>For the relation between the theory of well-pointed toposes and <strong>weak Zermelo set theory</strong> as elucidated by work of <a class="existingWikiWord" href="/nlab/show/Julian+Cole">J. Cole</a>, <a class="existingWikiWord" href="/nlab/show/Barry+Mitchell">Barry Mitchell</a>, and <a class="existingWikiWord" href="/nlab/show/Gerhard+Osius">G. Osius</a> in the early 1970s see</p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Peter+Johnstone">Peter Johnstone</a>, <em>Topos Theory</em> , Academic Press New York 1977 (Dover reprint 2014). (sections 9.2-3)</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Barry+Mitchell">Barry Mitchell</a>, <em>Boolean Topoi and the Theory of Sets</em> , JPAA <strong>2</strong> (1972) pp.261-274.</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Gerhard+Osius">Gerhard Osius</a>, <em>Categorical Set Theory: A Characterization of the Category of Sets</em>, JPAA <strong>4</strong> (1974) 79-119.</p> </li> </ul> <div class="footnotes"><hr /><ol><li id="fn:1"> <p>For a comparative discussion of its virtues as foundation see <a class="existingWikiWord" href="/nlab/show/foundations+of+mathematics">foundations of mathematics</a> , the <a href="#ExpositionByTrimble">texts by Todd Trimble</a> or the informative paper by <a href="#McLarty04">McLarty (2004)</a>. <a href="#fnref:1" rev="footnote">↩</a></p> </li><li id="fn:2"> <p>It has been pointed out by John Myhill that Cantor’s concept of ‘cardinal’ as a set of abstract units should be viewed as a structural set theory and a precursor to Lawvere’s concept of an ‘abstract set’. This view is endorsed and expanded in <a href="#Lawvere94">Lawvere 1994</a>. <a href="#fnref:2" rev="footnote">↩</a></p> </li><li id="fn:3"> <p><a class="existingWikiWord" href="/nlab/show/Richard+Dedekind"> R. Dedekind's</a> views are also anticipating ‘abstract sets’ e.g. Bernstein reports in Dedekind’s works vol.3 (1932, p.449) that Dedekind gave as his intuition of a set: “a closed bag, containing determinate things that one can not see and of which one knows nothing beyond their existence and determinateness”. <a href="#fnref:3" rev="footnote">↩</a></p> </li><li id="fn:4"> <p>The first axiomatic set theory without primitive membership relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∈</mo></mrow><annotation encoding="application/x-tex">\in</annotation></semantics></math> was presumably proposed by A. Schoenflies in 1920: he modeled elements of sets as indecomposable subsets. See A. Schoenflies, <em>Zur Axiomatik der Mengenlehre</em> , Math. Ann. <strong>83</strong> (1921) pp.173-200; and <em>Bemerkung zur Axiomatik der Grössen und Mengen</em> , Math. Ann. <strong>85</strong> (1922) pp.60-64. <a href="#fnref:4" rev="footnote">↩</a></p> </li><li id="fn:5"> <p>The first axiomatic set theory based on the notion of function was <a class="existingWikiWord" href="/nlab/show/John+von+Neumann">von Neumann</a>‘s 1925 version of what later became the set based <a class="existingWikiWord" href="/nlab/show/NBG">NBG</a> theory of classes. <a href="#fnref:5" rev="footnote">↩</a></p> </li></ol></div></body></html> </div> <div class="revisedby"> <p> Last revised on June 15, 2024 at 13:08:11. See the <a href="/nlab/history/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/ETCS" accesskey="E" class="navlink" id="edit" rel="nofollow">Edit</a><a href="https://nforum.ncatlab.org/discussion/8582/#Item_10">Discuss</a><span class="backintime"><a href="/nlab/revision/ETCS/61" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/diff/ETCS" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Changes from previous revision</a><a href="/nlab/history/ETCS" accesskey="S" class="navlink" id="history" rel="nofollow">History (61 revisions)</a> <a href="/nlab/show/ETCS/cite" style="color: black">Cite</a> <a href="/nlab/print/ETCS" accesskey="p" id="view_print" rel="nofollow">Print</a> <a href="/nlab/source/ETCS" id="view_source" rel="nofollow">Source</a> </div> </div>  </div>  </body> </html>