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> presentation axiom 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> presentation axiom </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/4368/#Item_15" 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="foundations">Foundations</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/foundations">foundations</a></strong></p> <h2 id="the_basis_of_it_all">The basis of it all</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/mathematical+logic">mathematical logic</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/deduction+system">deduction system</a>, <a class="existingWikiWord" href="/nlab/show/natural+deduction">natural deduction</a>, <a class="existingWikiWord" href="/nlab/show/sequent+calculus">sequent calculus</a>, <a class="existingWikiWord" href="/nlab/show/lambda-calculus">lambda-calculus</a>, <a class="existingWikiWord" href="/nlab/show/judgment">judgment</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a>, <a class="existingWikiWord" href="/nlab/show/simple+type+theory">simple type theory</a>, <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/collection">collection</a>, <a class="existingWikiWord" href="/nlab/show/object">object</a>, <a class="existingWikiWord" href="/nlab/show/type">type</a>, <a class="existingWikiWord" href="/nlab/show/term">term</a>, <a class="existingWikiWord" href="/nlab/show/set">set</a>, <a class="existingWikiWord" href="/nlab/show/element">element</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/equality">equality</a>, <a class="existingWikiWord" href="/nlab/show/judgmental+equality">judgmental equality</a>, <a class="existingWikiWord" href="/nlab/show/typal+equality">typal equality</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/universe">universe</a>, <a class="existingWikiWord" href="/nlab/show/size+issues">size issues</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/higher-order+logic">higher-order logic</a></p> </li> </ul> <h2 id="set_theory"> Set theory</h2> <div> <p><strong><a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a></strong></p> <ul> <li>fundamentals of set theory <ul> <li><a class="existingWikiWord" href="/nlab/show/propositional+logic">propositional logic</a></li> <li><a class="existingWikiWord" href="/nlab/show/first-order+logic">first-order logic</a></li> <li><a class="existingWikiWord" href="/nlab/show/typed+predicate+logic">typed predicate logic</a></li> <li><a class="existingWikiWord" href="/nlab/show/membership+relation">membership relation</a></li> <li><a class="existingWikiWord" href="/nlab/show/propositional+equality">propositional equality</a></li> <li><a class="existingWikiWord" href="/nlab/show/set">set</a>, <a class="existingWikiWord" href="/nlab/show/element">element</a>, <a class="existingWikiWord" href="/nlab/show/function">function</a>, <a class="existingWikiWord" href="/nlab/show/relation">relation</a></li> <li><a class="existingWikiWord" href="/nlab/show/universe">universe</a>, <a class="existingWikiWord" href="/nlab/show/small+set">small set</a>, <a class="existingWikiWord" href="/nlab/show/large+set">large set</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/material+set+theory">material set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/membership+relation">membership relation</a>, <a class="existingWikiWord" href="/nlab/show/propositional+equality">propositional equality</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+extensionality">axiom of extensionality</a></li> <li><a class="existingWikiWord" href="/nlab/show/pairing+structure">pairing structure</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+pairing">axiom of pairing</a></li> <li><a class="existingWikiWord" href="/nlab/show/union+structure">union structure</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+union">axiom of union</a></li> <li><a class="existingWikiWord" href="/nlab/show/powerset+structure">powerset structure</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+power+sets">axiom of power sets</a></li> <li><a class="existingWikiWord" href="/nlab/show/natural+numbers+structure">natural numbers structure</a>, <a class="existingWikiWord" href="/nlab/show/axiom+of+infinity">axiom of infinity</a></li> </ul> </li> <li>presentations of set theory <ul> <li><a class="existingWikiWord" href="/nlab/show/first-order+set+theory">first-order set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/unsorted+set+theory">unsorted set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/simply+sorted+set+theory">simply sorted set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/one-sorted+set+theory">one-sorted set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/two-sorted+set+theory">two-sorted set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/three-sorted+set+theory">three-sorted set theory</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/dependently+sorted+set+theory">dependently sorted set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/structurally+presented+set+theory">structurally presented set theory</a></li> </ul> </li> <li>structuralism in set theory <ul> <li><a class="existingWikiWord" href="/nlab/show/material+set+theory">material set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/ZFC">ZFC</a></li> <li><a class="existingWikiWord" href="/nlab/show/ZFA">ZFA</a></li> <li><a class="existingWikiWord" href="/nlab/show/Mostowski+set+theory">Mostowski set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/New+Foundations">New Foundations</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/structural+set+theory">structural set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/categorical+set+theory">categorical set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/ETCS">ETCS</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/fully+formal+ETCS">fully formal ETCS</a></li> <li><a class="existingWikiWord" href="/nlab/show/ETCS+with+elements">ETCS with elements</a></li> <li><a class="existingWikiWord" href="/nlab/show/Trimble+on+ETCS+I">Trimble on ETCS I</a></li> <li><a class="existingWikiWord" href="/nlab/show/Trimble+on+ETCS+II">Trimble on ETCS II</a></li> <li><a class="existingWikiWord" href="/nlab/show/Trimble+on+ETCS+III">Trimble on ETCS III</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/structural+ZFC">structural ZFC</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/allegorical+set+theory">allegorical set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/SEAR">SEAR</a></li> </ul> </li> </ul> </li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/class-set+theory">class-set theory</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/class">class</a>, <a class="existingWikiWord" href="/nlab/show/proper+class">proper class</a></li> <li><a class="existingWikiWord" href="/nlab/show/universal+class">universal class</a>, <a class="existingWikiWord" href="/nlab/show/universe">universe</a></li> <li><a class="existingWikiWord" href="/nlab/show/category+of+classes">category of classes</a></li> <li><a class="existingWikiWord" href="/nlab/show/category+with+class+structure">category with class structure</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/constructive+set+theory">constructive set theory</a></li> <li><a class="existingWikiWord" href="/nlab/show/algebraic+set+theory">algebraic set theory</a></li> </ul> </div> <h2 id="foundational_axioms">Foundational axioms</h2> <div> <p><strong><a class="existingWikiWord" href="/nlab/show/foundational+axiom">foundational</a> <a class="existingWikiWord" href="/nlab/show/axioms">axioms</a></strong></p> <ul> <li> <p>basic constructions:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+cartesian+products">axiom of cartesian products</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+disjoint+unions">axiom of disjoint unions</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+the+empty+set">axiom of the empty set</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+fullness">axiom of fullness</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+function+sets">axiom of function sets</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+power+sets">axiom of power sets</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+quotient+sets">axiom of quotient sets</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/material+set+theory">material axioms</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+extensionality">axiom of extensionality</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+foundation">axiom of foundation</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+anti-foundation">axiom of anti-foundation</a></li> <li><a class="existingWikiWord" href="/nlab/show/Mostowski%27s+axiom">Mostowski's axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+pairing">axiom of pairing</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+transitive+closure">axiom of transitive closure</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+union">axiom of union</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/structural+set+theory">structural axioms</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+materialization">axiom of materialization</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/type+theory">type theoretic axioms</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axioms+of+set+truncation">axioms of set truncation</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/uniqueness+of+identity+proofs">uniqueness of identity proofs</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+K">axiom K</a></li> <li><a class="existingWikiWord" href="/nlab/show/boundary+separation">boundary separation</a></li> <li><a class="existingWikiWord" href="/nlab/show/equality+reflection">equality reflection</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+circle+type+localization">axiom of circle type localization</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theoretic axioms</a>: <ul> <li><a class="existingWikiWord" href="/nlab/show/univalence+axiom">univalence axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/Whitehead%27s+principle">Whitehead's principle</a></li> </ul> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/axioms+of+choice">axioms of choice</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+countable+choice">axiom of countable choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+dependent+choice">axiom of dependent choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+excluded+middle">axiom of excluded middle</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+existence">axiom of existence</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+multiple+choice">axiom of multiple choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/Markov%27s+axiom">Markov's axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/presentation+axiom">presentation axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/small+cardinality+selection+axiom">small cardinality selection axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+small+violations+of+choice">axiom of small violations of choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+weakly+initial+sets+of+covers">axiom of weakly initial sets of covers</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/large+cardinal+axioms">large cardinal axioms</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+infinity">axiom of infinity</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+universes">axiom of universes</a></li> <li><a class="existingWikiWord" href="/nlab/show/regular+extension+axiom">regular extension axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/inaccessible+cardinal">inaccessible cardinal</a></li> <li><a class="existingWikiWord" href="/nlab/show/measurable+cardinal">measurable cardinal</a></li> <li><a class="existingWikiWord" href="/nlab/show/elementary+embedding">elementary embedding</a></li> <li><a class="existingWikiWord" href="/nlab/show/supercompact+cardinal">supercompact cardinal</a></li> <li><a class="existingWikiWord" href="/nlab/show/Vop%C4%9Bnka%27s+principle">Vopěnka's principle</a></li> </ul> </li> <li> <p>strong axioms</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+separation">axiom of separation</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+replacement">axiom of replacement</a></li> </ul> </li> <li> <p>further</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/reflection+principle">reflection principle</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/axiom+of+inequality+spaces">axiom of inequality spaces</a></p> </li> </ul> </div> <h2 id="removing_axioms">Removing axioms</h2> <ul> <li><a class="existingWikiWord" href="/nlab/show/constructive+mathematics">constructive mathematics</a></li> <li><a class="existingWikiWord" href="/nlab/show/predicative+mathematics">predicative mathematics</a></li> </ul> <div> <p> <a href="/nlab/edit/foundations+-+contents">Edit this sidebar</a> </p> </div></div></div> </div> </div> <h1 id="contents">Contents</h1> <div class='maruku_toc'> <ul> <li><a href='#idea'>Idea</a></li> <li><a href='#Statement'>Statement</a></li> <ul> <li><a href='#axiom_coshep'>Axiom (CoSHEP)</a></li> <li><a href='#axiom_coshep_2'>Axiom (CoSHEP)</a></li> </ul> <li><a href='#consequences'>Consequences</a></li> <li><a href='#Variants'>Variants of the presentation axiom</a></li> <ul> <li><a href='#split_surjections'> Split surjections</a></li> <li><a href='#external_and_internal_versions'>External and internal versions</a></li> <li><a href='#bhk_interpretation_of_the_presentation_axiom'>BHK interpretation of the presentation axiom</a></li> <li><a href='#in_dependent_type_theory'>In dependent type theory</a></li> </ul> <li><a href='#topos'>In a topos</a></li> <ul> <li><a href='#counterexample'>Counterexample</a></li> <li><a href='#counterexample_2'>Counterexample</a></li> </ul> <li><a href='#in_categories_which_are_not_topoi'>In categories which are not topoi</a></li> <li><a href='#further_properties'>Further properties</a></li> <li><a href='#in_higher_category_theory'> In higher category theory</a></li> <li><a href='#justification'>Justification</a></li> <li><a href='#related_concepts'>Related concepts</a></li> <li><a href='#references'>References</a></li> </ul> </div> <h2 id="idea">Idea</h2> <p>In the <a class="existingWikiWord" href="/nlab/show/foundations">foundations</a> of <a class="existingWikiWord" href="/nlab/show/mathematics">mathematics</a>, it's interesting to consider the axiom that the <a class="existingWikiWord" href="/nlab/show/Set">Category of Sets</a> Has <a class="existingWikiWord" href="/nlab/show/projective+object">Enough Projectives</a>; in short: <strong>CoSHEP</strong> (pronounced /ko:-shep/). This is more commonly known as the <strong>presentation axiom</strong>: PAx. It is a weak form of the <a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a>.</p> <h2 id="Statement">Statement</h2> <p>In elementary terms, CoSHEP states</p> <div class="num_defn"> <h6 id="axiom_coshep">Axiom (CoSHEP)</h6> <p>For every <a class="existingWikiWord" href="/nlab/show/set">set</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>, there exists a set <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> and a <a class="existingWikiWord" href="/nlab/show/surjection">surjection</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo>→</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">P \to A</annotation></semantics></math>, such that every surjection <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi><mo>↠</mo><mi>P</mi></mrow><annotation encoding="application/x-tex">X \twoheadrightarrow P</annotation></semantics></math> has a <a class="existingWikiWord" href="/nlab/show/section">section</a>.</p> </div> <p> <div class='num_remark'> <h6>Remark</h6> <p>The full axiom of choice states that every surjection <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi><mo>→</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">X \to A</annotation></semantics></math> has a section; hence in the above <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> may be chosen to be <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> itself.</p> </div> </p> <p>This should be read in view of the definition of <em><a class="existingWikiWord" href="/nlab/show/projective+objects">projective objects</a></em>:</p> <p> <div class='num_defn'> <h6>Definition</h6> <p>An <a class="existingWikiWord" href="/nlab/show/object">object</a> <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> in a <a class="existingWikiWord" href="/nlab/show/category">category</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> is (externally) <a class="existingWikiWord" href="/nlab/show/projective+object">projective</a> iff the <a class="existingWikiWord" href="/nlab/show/hom-functor">hom-functor</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi><mo stretchy="false">(</mo><mi>P</mi><mo>,</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo stretchy="false">)</mo><mo>:</mo><mi>C</mi><mo>→</mo><mi>Set</mi></mrow><annotation encoding="application/x-tex">C(P, -): C \to Set</annotation></semantics></math> takes <a class="existingWikiWord" href="/nlab/show/epimorphism">epis</a> to epis. This is the same as saying: given an epi <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi><mo>:</mo><mi>B</mi><mo>→</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">p: B \to A</annotation></semantics></math> and a map <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><mi>P</mi><mo>→</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">f: P \to A</annotation></semantics></math>, there exists a lift <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>g</mi><mo>:</mo><mi>P</mi><mo>→</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">g: P \to B</annotation></semantics></math> in the sense that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>=</mo><mi>p</mi><mo>∘</mo><mi>g</mi></mrow><annotation encoding="application/x-tex">f = p \circ g</annotation></semantics></math>.</p> </div> </p> <p>Accordingly, in a <a class="existingWikiWord" href="/nlab/show/topos">topos</a> the CoSHEP axiom says equivalently</p> <div class="num_defn"> <h6 id="axiom_coshep_2">Axiom (CoSHEP)</h6> <p>Every object has a <a class="existingWikiWord" href="/nlab/show/projective+presentation">projective presentation</a>. Hence: There are <a href="projective+object#EnoughProjectives">enough projectives</a>.</p> </div> <p>Borrowing from the philosophy of <a class="existingWikiWord" href="/nlab/show/constructive+mathematics">constructivism</a>, we may also call this a <em>complete presentation</em>.</p> <p> <div class='num_remark'> <h6>Remark</h6> <p>The <a class="existingWikiWord" href="/nlab/show/duality">dual</a> axiom, that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> has <a href="injective+object#EnoughInjectives">enough injectives</a> (that is, every set admits an injection into an injective set) is <a class="existingWikiWord" href="/nlab/show/true">true</a> in every <a class="existingWikiWord" href="/nlab/show/topos">topos</a>: every <a class="existingWikiWord" href="/nlab/show/power+object">power object</a> is an <a class="existingWikiWord" href="/nlab/show/injective+object">injective object</a>, and every object <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> embeds in its power object <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mi>X</mi></mrow><annotation encoding="application/x-tex">P X</annotation></semantics></math> via the <a class="existingWikiWord" href="/nlab/show/singleton+subset">singleton</a> map <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">{</mo><mo>⋅</mo><mo stretchy="false">}</mo><mo>:</mo><mi>X</mi><mo>↪</mo><mi>P</mi><mi>X</mi></mrow><annotation encoding="application/x-tex">\{\cdot\}:X\hookrightarrow P X</annotation></semantics></math>.</p> </div> </p> <h2 id="consequences">Consequences</h2> <p>The existence of sufficiently many <a class="existingWikiWord" href="/nlab/show/projective+presentations">projective presentations</a> plays a central role in <a class="existingWikiWord" href="/nlab/show/homological+algebra">homological algebra</a> as a means to construct <a class="existingWikiWord" href="/nlab/show/projective+resolutions">projective resolutions</a> of objects. Tradtionally one often uses the <a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a> to prove that <a class="existingWikiWord" href="/nlab/show/categories+of+modules">categories of modules</a> have <a href="projective+object#EnoughProjectives">enough projectives</a>, on the grounds that the <a class="existingWikiWord" href="/nlab/show/free+modules">free modules</a> are projective.</p> <p>But the weaker assumption of CoSHEP is already sufficient for this purpose: while not every free module will be projective, one can still use CoSHEP to find a <a class="existingWikiWord" href="/nlab/show/projective+presentation">projective presentation</a> for every free module (and thus for every module). This is discussed in more detail <a href="projective+object#EnoughWithCOSHEP">here</a>.</p> <div class="num_prop" id="ImpliesDependentAndCountableChoice"> <h6 id="proposition">Proposition</h6> <p>The following three conditions on a <a class="existingWikiWord" href="/nlab/show/W-pretopos">W-pretopos</a> with <a href="projective+object#EnoughProjectives">enough projectives</a> are equivalent:</p> <ol> <li> <p>The axiom of <a class="existingWikiWord" href="/nlab/show/dependent+choice">dependent choice</a> (DC),</p> </li> <li> <p>The axiom of <a class="existingWikiWord" href="/nlab/show/countable+choice">countable choice</a> (CC),</p> </li> <li> <p>Projectivity of the <a class="existingWikiWord" href="/nlab/show/singleton">singleton</a> (the <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>.</p> </li> </ol> </div> <p>Note that we normally assume (3) for <a class="existingWikiWord" href="/nlab/show/the+category+of+sets">the category of sets</a>, which is true in any (constructively) <a class="existingWikiWord" href="/nlab/show/well-pointed+pretopos">well-pointed pretopos</a> and true <em><a class="existingWikiWord" href="/nlab/show/internalization">internally</a></em> in any pretopos whatsoever, so one normally says that DC and CC simply follow from the existence of enough projectives (CoSHEP). Equivalently, internal DC and internal CC follow from internal CoSHEP.</p> <div class="proof"> <h6 id="proof">Proof</h6> <p>Condition 1 easily implies 2. Condition 2 says precisely that the <a class="existingWikiWord" href="/nlab/show/natural+numbers+object">natural numbers object</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">\mathbb{N}</annotation></semantics></math> is externally projective, and since <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> is a retract of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℕ</mi></mrow><annotation encoding="application/x-tex">\mathbb{N}</annotation></semantics></math>, it is projective under condition 2, so 2 implies 3. It remains to show 3 implies 1.</p> <p>Let <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> be inhabited, so there exists an <a class="existingWikiWord" href="/nlab/show/entire+relation">entire relation</a> given by a jointly monic span</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mn>1</mn><mover><mo>←</mo><mi>epi</mi></mover><mi>U</mi><mover><mo>→</mo><mi>f</mi></mover><mi>X</mi><mo>,</mo></mrow><annotation encoding="application/x-tex">1 \stackrel{epi}{\leftarrow} U \stackrel{f}{\to} X,</annotation></semantics></math></div> <p>and similarly let</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>X</mi><mover><mo>←</mo><mrow><mi>epi</mi><msub><mi>π</mi> <mn>1</mn></msub></mrow></mover><mi>R</mi><mover><mo>→</mo><mrow><msub><mi>π</mi> <mn>2</mn></msub></mrow></mover><mi>X</mi></mrow><annotation encoding="application/x-tex">X \stackrel{epi \pi_1}{\leftarrow} R \stackrel{\pi_2}{\to} X</annotation></semantics></math></div> <p>be an <a class="existingWikiWord" href="/nlab/show/entire+relation">entire binary relation</a>. Let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi><mo>:</mo><mi>P</mi><mo>→</mo><mi>X</mi></mrow><annotation encoding="application/x-tex">p: P \to X</annotation></semantics></math> be a projective cover. Since <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> is assumed projective, the cover <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi><mo>→</mo><mn>1</mn></mrow><annotation encoding="application/x-tex">U \to 1</annotation></semantics></math> admits a section <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>σ</mi><mo>:</mo><mn>1</mn><mo>→</mo><mi>U</mi></mrow><annotation encoding="application/x-tex">\sigma: 1 \to U</annotation></semantics></math>, and the element <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mi>σ</mi><mo>:</mo><mn>1</mn><mo>→</mo><mi>X</mi></mrow><annotation encoding="application/x-tex">f \sigma: 1 \to X</annotation></semantics></math> lifts through <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> to an element <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>x</mi> <mn>0</mn></msub><mo>:</mo><mn>1</mn><mo>→</mo><mi>P</mi></mrow><annotation encoding="application/x-tex">x_0: 1 \to P</annotation></semantics></math>. Next, in the diagram below, <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> lifts through the epi <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>π</mi> <mn>1</mn></msub></mrow><annotation encoding="application/x-tex">\pi_1</annotation></semantics></math> to a map <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>q</mi><mo>:</mo><mi>P</mi><mo>→</mo><mi>R</mi></mrow><annotation encoding="application/x-tex">q: P \to R</annotation></semantics></math>, and then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>π</mi> <mn>2</mn></msub><mi>q</mi></mrow><annotation encoding="application/x-tex">\pi_2 q</annotation></semantics></math> lifts through <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> to a map <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ϕ</mi></mrow><annotation encoding="application/x-tex">\phi</annotation></semantics></math> (since <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 projective):</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd></mtd> <mtd></mtd> <mtd><mi>P</mi></mtd> <mtd><mover><mo>→</mo><mi>ϕ</mi></mover></mtd> <mtd><mi>P</mi></mtd></mtr> <mtr><mtd></mtd> <mtd><mo>↙</mo><mi>p</mi></mtd> <mtd><mo stretchy="false">↓</mo><mi>q</mi></mtd> <mtd></mtd> <mtd><mo stretchy="false">↓</mo><mi>p</mi></mtd></mtr> <mtr><mtd><mi>X</mi></mtd> <mtd><munder><mo>←</mo><mrow><msub><mi>π</mi> <mn>1</mn></msub></mrow></munder></mtd> <mtd><mi>R</mi></mtd> <mtd><munder><mo>→</mo><mrow><msub><mi>π</mi> <mn>2</mn></msub></mrow></munder></mtd> <mtd><mi>X</mi></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex">\array{ & & P & \stackrel{\phi}{\to} & P \\ & \swarrow p & \downarrow q & & \downarrow p \\ X & \underset{\pi_1}{\leftarrow} & R & \underset{\pi_2}{\to} & X } </annotation></semantics></math></div> <p>By the universal property of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℕ</mi></mrow><annotation encoding="application/x-tex">\mathbb{N}</annotation></semantics></math> (see <a class="existingWikiWord" href="/nlab/show/recursion">recursion</a>), there exists a unique map <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>h</mi><mo>:</mo><mi>ℕ</mi><mo>→</mo><mi>P</mi></mrow><annotation encoding="application/x-tex">h: \mathbb{N} \to P</annotation></semantics></math> rendering commutative the diagram</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><mn>1</mn></mtd> <mtd><mover><mo>→</mo><mn>0</mn></mover></mtd> <mtd><mi>ℕ</mi></mtd> <mtd><mover><mo>→</mo><mi>s</mi></mover></mtd> <mtd><mi>ℕ</mi></mtd></mtr> <mtr><mtd><mi>id</mi><mo stretchy="false">↓</mo></mtd> <mtd></mtd> <mtd><mo stretchy="false">↓</mo><mi>h</mi></mtd> <mtd></mtd> <mtd><mo stretchy="false">↓</mo><mi>h</mi></mtd></mtr> <mtr><mtd><mn>1</mn></mtd> <mtd><munder><mo>→</mo><mrow><msub><mi>x</mi> <mn>0</mn></msub></mrow></munder></mtd> <mtd><mi>P</mi></mtd> <mtd><munder><mo>→</mo><mi>ϕ</mi></munder></mtd> <mtd><mi>P</mi></mtd></mtr> <mtr><mtd></mtd> <mtd><mo>↙</mo><mi>p</mi></mtd> <mtd><mo stretchy="false">↓</mo><mi>q</mi></mtd> <mtd></mtd> <mtd><mo stretchy="false">↓</mo><mi>p</mi></mtd></mtr> <mtr><mtd><mi>X</mi></mtd> <mtd><munder><mo>←</mo><mrow><msub><mi>π</mi> <mn>1</mn></msub></mrow></munder></mtd> <mtd><mi>R</mi></mtd> <mtd><munder><mo>→</mo><mrow><msub><mi>π</mi> <mn>2</mn></msub></mrow></munder></mtd> <mtd><mi>X</mi></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex">\array{ 1 & \stackrel{0}{\to} & \mathbb{N} & \stackrel{s}{\to} & \mathbb{N} \\ id \downarrow & & \downarrow h & & \downarrow h \\ 1 & \underset{x_0}{\to} & P & \underset{\phi}{\to} & P \\ & \swarrow p & \downarrow q & & \downarrow p \\ X & \underset{\pi_1}{\leftarrow} & R & \underset{\pi_2}{\to} & X } </annotation></semantics></math></div> <p>Clearly <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">⟨</mo><mi>p</mi><mi>h</mi><mo>,</mo><mi>p</mi><mi>h</mi><mi>s</mi><mo stretchy="false">⟩</mo><mo>:</mo><mi>ℕ</mi><mo>→</mo><mi>X</mi><mo>×</mo><mi>X</mi></mrow><annotation encoding="application/x-tex">\langle p h, p h s \rangle : \mathbb{N} \to X \times X</annotation></semantics></math> factors through <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">⟨</mo><msub><mi>π</mi> <mn>1</mn></msub><mo>,</mo><msub><mi>π</mi> <mn>2</mn></msub><mo stretchy="false">⟩</mo><mo>:</mo><mi>R</mi><mo>→</mo><mi>X</mi><mo>×</mo><mi>X</mi></mrow><annotation encoding="application/x-tex">\langle \pi_1, \pi_2 \rangle : R \to X \times X</annotation></semantics></math>, i.e., <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mo>∀</mo> <mrow><mi>n</mi><mo>:</mo><mi>ℕ</mi></mrow></msub><mo stretchy="false">(</mo><mi>p</mi><mi>h</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>,</mo><mi>p</mi><mi>h</mi><mo stretchy="false">(</mo><mi>n</mi><mo>+</mo><mn>1</mn><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>∈</mo><mi>R</mi></mrow><annotation encoding="application/x-tex">\forall_{n: \mathbb{N}} (p h(n), p h(n+1)) \in R</annotation></semantics></math>, thus proving that dependent choice holds under CoSHEP.</p> </div> <div class="num_example"> <h6 id="example">Example</h6> <p>A topos in which CoSHEP holds but <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> is not projective is <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>Set</mi> <mi>C</mi></msup></mrow><annotation encoding="application/x-tex">Set^C</annotation></semantics></math>, where <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 the category with three objects and exactly two non-identity arrows <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>→</mo><mi>b</mi><mo>←</mo><mi>c</mi></mrow><annotation encoding="application/x-tex">a \to b \leftarrow c</annotation></semantics></math>. For if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi><mo>:</mo><mi>C</mi><mo>→</mo><mi>Set</mi></mrow><annotation encoding="application/x-tex">U: C \to Set</annotation></semantics></math> is a functor with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo><mo>=</mo><mo stretchy="false">{</mo><msub><mi>a</mi> <mn>0</mn></msub><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">U(a) = \{a_0\}</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi><mo stretchy="false">(</mo><mi>b</mi><mo stretchy="false">)</mo><mo>=</mo><mo stretchy="false">{</mo><msub><mi>b</mi> <mn>0</mn></msub><mo>,</mo><msub><mi>b</mi> <mn>1</mn></msub><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">U(b) = \{b_0, b_1\}</annotation></semantics></math>, and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi><mo stretchy="false">(</mo><mi>c</mi><mo stretchy="false">)</mo><mo>=</mo><mo stretchy="false">{</mo><msub><mi>c</mi> <mn>0</mn></msub><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">U(c) = \{c_0\}</annotation></semantics></math>, with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi><mo stretchy="false">(</mo><mi>a</mi><mo>→</mo><mi>b</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><msub><mi>a</mi> <mn>0</mn></msub><mo stretchy="false">)</mo><mo>=</mo><msub><mi>b</mi> <mn>0</mn></msub></mrow><annotation encoding="application/x-tex">U(a \to b)(a_0) = b_0</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi><mo stretchy="false">(</mo><mi>c</mi><mo>→</mo><mi>b</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><msub><mi>c</mi> <mn>0</mn></msub><mo stretchy="false">)</mo><mo>=</mo><msub><mi>b</mi> <mn>1</mn></msub></mrow><annotation encoding="application/x-tex">U(c \to b)(c_0) = b_1</annotation></semantics></math>, then the map <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi><mo>→</mo><mn>1</mn></mrow><annotation encoding="application/x-tex">U \to 1</annotation></semantics></math> is epi but has no section, so <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> is not projective. On the other hand, as noted below, every presheaf topos satisfies CoSHEP, assuming that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> itself does.</p> </div> <p>CoSHEP also implies several weaker forms of choice, such as the <a class="existingWikiWord" href="/nlab/show/axiom+of+multiple+choice">axiom of multiple choice</a> and <a class="existingWikiWord" href="/nlab/show/WISC">WISC</a>. In weakly <a class="existingWikiWord" href="/nlab/show/predicative+mathematics">predicative mathematics</a>, it can be combined with the existence of <a class="existingWikiWord" href="/nlab/show/function+sets">function sets</a> to show the <a class="existingWikiWord" href="/nlab/show/subset+collection">subset collection</a> axiom.</p> <h2 id="Variants">Variants of the presentation axiom</h2> <h3 id="split_surjections"> Split surjections</h3> <p>In the absence of the full <a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a>, there are actually two notions of surjections: <a class="existingWikiWord" href="/nlab/show/surjections">surjections</a>, and <a class="existingWikiWord" href="/nlab/show/split+surjections">split surjections</a>. Hence, we get four possible different statements of the presentation axiom, depending on whether one uses surjections or split surjections:</p> <ol> <li> <p>For every <a class="existingWikiWord" href="/nlab/show/set">set</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>, there exists a set <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> and a <a class="existingWikiWord" href="/nlab/show/surjection">surjection</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo>→</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">P \to A</annotation></semantics></math>, such that every surjection <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi><mo>↠</mo><mi>P</mi></mrow><annotation encoding="application/x-tex">X \twoheadrightarrow P</annotation></semantics></math> has a <a class="existingWikiWord" href="/nlab/show/section">section</a>.</p> </li> <li> <p>For every <a class="existingWikiWord" href="/nlab/show/set">set</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>, there exists a set <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> and a <a class="existingWikiWord" href="/nlab/show/split+surjection">split surjection</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo>→</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">P \to A</annotation></semantics></math>, such that every surjection <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi><mo>↠</mo><mi>P</mi></mrow><annotation encoding="application/x-tex">X \twoheadrightarrow P</annotation></semantics></math> has a <a class="existingWikiWord" href="/nlab/show/section">section</a>.</p> </li> <li> <p>For every <a class="existingWikiWord" href="/nlab/show/set">set</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>, there exists a set <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> and a <a class="existingWikiWord" href="/nlab/show/surjection">surjection</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo>→</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">P \to A</annotation></semantics></math>, such that every split surjection <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi><mo>↠</mo><mi>P</mi></mrow><annotation encoding="application/x-tex">X \twoheadrightarrow P</annotation></semantics></math> has a <a class="existingWikiWord" href="/nlab/show/section">section</a>.</p> </li> <li> <p>For every <a class="existingWikiWord" href="/nlab/show/set">set</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>, there exists a set <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> and a <a class="existingWikiWord" href="/nlab/show/split+surjection">split surjection</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo>→</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">P \to A</annotation></semantics></math>, such that every split surjection <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi><mo>↠</mo><mi>P</mi></mrow><annotation encoding="application/x-tex">X \twoheadrightarrow P</annotation></semantics></math> has a <a class="existingWikiWord" href="/nlab/show/section">section</a>.</p> </li> </ol> <p>By definition of split surjection, every split surjection has a section, so the third and fourth versions of the presentation axioms are simply:</p> <ul> <li> <p>For every <a class="existingWikiWord" href="/nlab/show/set">set</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>, there exists a set <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> and a <a class="existingWikiWord" href="/nlab/show/surjection">surjection</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo>→</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">P \to A</annotation></semantics></math>.</p> </li> <li> <p>For every <a class="existingWikiWord" href="/nlab/show/set">set</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>, there exists a set <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> and a <a class="existingWikiWord" href="/nlab/show/split+surjection">split surjection</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo>→</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">P \to A</annotation></semantics></math>.</p> </li> </ul> <p>These two versions of the presentation axiom are always true: take the set <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> to be <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> and the (split) surjection <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo>→</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">P \to A</annotation></semantics></math> to be the <a class="existingWikiWord" href="/nlab/show/identity+function">identity function</a> on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>.</p> <p>This leaves the first and second version of the presentation axiom as non-trivial axioms that one can add to the <a class="existingWikiWord" href="/nlab/show/foundations">foundations</a>. In general, the version using a split surjection into <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> is stronger than the version using a surjection into <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>, because not every surjection is a split surjection unless the full <a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a> holds. And then the usual <a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a> is simply the presentation axiom where the surjection is required to be a <a class="existingWikiWord" href="/nlab/show/bijection">bijection</a>.</p> <h3 id="external_and_internal_versions">External and internal versions</h3> <p>In addition, every <a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a> has an <a class="existingWikiWord" href="/nlab/show/internal+logic">internal logic</a> defined on its <a class="existingWikiWord" href="/nlab/show/subsingletons">subsingletons</a>:</p> <ul> <li> <p>Any <a class="existingWikiWord" href="/nlab/show/subsingleton">subsingleton</a> represents a proposition</p> </li> <li> <p>The <a class="existingWikiWord" href="/nlab/show/empty+set">empty set</a> represents <a class="existingWikiWord" href="/nlab/show/falsehood">falsehood</a></p> </li> <li> <p>Any <a class="existingWikiWord" href="/nlab/show/singleton">singleton</a> represents <a class="existingWikiWord" href="/nlab/show/truth">truth</a></p> </li> <li> <p>The binary cartesian product of two subsingletons is <a class="existingWikiWord" href="/nlab/show/conjunction">conjunction</a> of propositions</p> </li> <li> <p>The function set between two subsingletons is <a class="existingWikiWord" href="/nlab/show/implication">implication</a> of propositions</p> </li> <li> <p>The function set from a subsingleton to the empty set is <a class="existingWikiWord" href="/nlab/show/negation">negation</a> of propositions</p> </li> <li> <p>Given a family of subsingletons, the indexed <a class="existingWikiWord" href="/nlab/show/cartesian+product">cartesian product</a> of the family of subsingletons is <a class="existingWikiWord" href="/nlab/show/universal+quantification">universal quantification</a></p> </li> <li> <p>One can turn any set into a subsingleton by taking the <a class="existingWikiWord" href="/nlab/show/image">image</a> of the unique function into a <a class="existingWikiWord" href="/nlab/show/singleton">singleton</a>. This is useful for constructing the internal disjunction and existential quantifier:</p> </li> <li> <p>The image of the unique function from the <a class="existingWikiWord" href="/nlab/show/disjoint+union">disjoint union</a> of two subsingletons to any singleton is the <a class="existingWikiWord" href="/nlab/show/disjunction">disjunction</a> of propositions</p> </li> <li> <p>The image of the unique function from the indexed <a class="existingWikiWord" href="/nlab/show/disjoint+union">disjoint union</a> of a family of subsingletons to any singleton is the <a class="existingWikiWord" href="/nlab/show/existential+quantifier">existential quantifier</a></p> </li> <li> <p>Equality is given by the <a class="existingWikiWord" href="/nlab/show/diagonal+subset">diagonal subset</a></p> </li> </ul> <p>Then there also exist internal versions of the presentation axiom, which states that the presentation axiom is true when expressed internally in the set theory, that a particular subsingleton defined using the set theoretic operations above is a singleton.</p> <h3 id="bhk_interpretation_of_the_presentation_axiom">BHK interpretation of the presentation axiom</h3> <p>In addition, there are two different ways to interpret predicate logic in the internal logic of a set theory:</p> <ul> <li> <p>There is the traditional way of interpreting the internal logic, which takes <a class="existingWikiWord" href="/nlab/show/propositions+as+subsingletons">propositions as subsingletons</a>, and uses the <a class="existingWikiWord" href="/nlab/show/disjunction">disjunction</a> for “or” and the <a class="existingWikiWord" href="/nlab/show/existential+quantifier">existential quantifier</a> for “there exists, suitably defined in the internal logic.</p> </li> <li> <p>There is the <a class="existingWikiWord" href="/nlab/show/BHK+interpretation">BHK interpretation</a> of the internal logic, which takes <a class="existingWikiWord" href="/nlab/show/propositions+as+sets">propositions as sets</a> and directly uses binary <a class="existingWikiWord" href="/nlab/show/disjoint+unions">disjoint unions</a> for “or” instead of the disjunction, as well as indexed disjoint unions for “there exist” instead of the existential quantifier.</p> </li> </ul> <p>This means that we get even more versions of the presentation axiom in set theory, depending on where one uses the traditional interpretation of predicate logic and where one uses the BHK interpretation of predicate logic in the internal logic:</p> <ul> <li> <p>For surjections, whether the fibers of the function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><mi>P</mi><mo>→</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">f:P \to A</annotation></semantics></math> are internally inhabited or pointed</p> </li> <li> <p>For split surjections, whether given a function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><mi>P</mi><mo>→</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">f:P \to A</annotation></semantics></math> there exists a section <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>g</mi><mo>:</mo><mi>A</mi><mo>→</mo><mi>P</mi></mrow><annotation encoding="application/x-tex">g:A \to P</annotation></semantics></math>, or whether one has a section-retraction 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><mo>:</mo><mo stretchy="false">(</mo><mi>P</mi><mo>→</mo><mi>A</mi><mo stretchy="false">)</mo><mo>×</mo><mo stretchy="false">(</mo><mi>A</mi><mo>→</mo><mi>P</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(f, g):(P \to A) \times (A \to P)</annotation></semantics></math></p> </li> </ul> <p>All of these combine together to form a huge number of possible axioms of the presentation axiom, ranging from the provable to stronger than the usual presentation axiom.</p> <h3 id="in_dependent_type_theory">In dependent type theory</h3> <p>In dependent type theory, not all types are sets, and sets (and other types) are usually elements of types called universes, so there are even more versions of the presentation axiom, depending on</p> <ul> <li> <p>Whether given a set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>:</mo><mi>U</mi></mrow><annotation encoding="application/x-tex">A:U</annotation></semantics></math> there exists a set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo>:</mo><mi>U</mi></mrow><annotation encoding="application/x-tex">P:U</annotation></semantics></math> or whether one has a pair of sets <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>A</mi><mo>,</mo><mi>P</mi><mo stretchy="false">)</mo><mo>:</mo><mi>U</mi><mo>×</mo><mi>U</mi></mrow><annotation encoding="application/x-tex">(A, P):U \times U</annotation></semantics></math>,</p> </li> <li> <p>Whether one uses sets or types in defining the presentation axiom.</p> </li> </ul> <h2 id="topos">In a topos</h2> <p>When working in the <a class="existingWikiWord" href="/nlab/show/internal+logic">internal logic</a> of a <a class="existingWikiWord" href="/nlab/show/topos">topos</a>, the “internal” meaning of CoSHEP is “every object is covered by an <a class="existingWikiWord" href="/nlab/show/internally+projective+object">internally projective object</a>.” (Compare with the internal axiom of choice: every object is internally projective.) As regards foundational axioms for toposes (in the sort of sense that the axiom of choice is regarded as “foundational”), the internal version of the presentation axiom should be taken as the default version.</p> <div class="num_prop"> <h6 id="proposition_2">Proposition</h6> <p>Suppose that <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> is (externally) projective in <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>. Then <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> satisfies PAx whenever it satisfies internal PAx.</p> </div> <p>Internal PAx does not follows from external PAx; see Counterexample 5.3. However, if <em>every</em> object is projective (AC), then every object is internally projective (IAC).</p> <p>A stronger version of PAx may be worth considering. Say that an object is <strong>stably projective</strong> if its <a class="existingWikiWord" href="/nlab/show/pullback">pullback</a> to any <a class="existingWikiWord" href="/nlab/show/slice+category">slice category</a> is projective. Then stably projective objects are internally projective (proof?). Similarly, if we say that a topos <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>E</mi></mrow><annotation encoding="application/x-tex">E</annotation></semantics></math> satisfies stable PAx if every object is covered by a stably projective object, then a topos satisfies internal PAx if it satisfies stable PAx.</p> <div class="num_example"> <h6 id="example_2">Example</h6> <p>Every <a class="existingWikiWord" href="/nlab/show/presheaf+topos">presheaf topos</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>Set</mi> <mrow><msup><mi>C</mi> <mi>op</mi></msup></mrow></msup></mrow><annotation encoding="application/x-tex">Set^{C^{op}}</annotation></semantics></math> has enough projectives, since any coproduct of representables is projective. If in addition <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> has binary products, then by <a href="/nlab/show/internally+projective+object#presheaf">this result</a>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>Set</mi> <mrow><msup><mi>C</mi> <mi>op</mi></msup></mrow></msup></mrow><annotation encoding="application/x-tex">Set^{C^{op}}</annotation></semantics></math> validates internal PAx.</p> </div> <div class="num_example" id="counter"> <h6 id="counterexample">Counterexample</h6> <p>However, not every presheaf topos validates internal PAx, even though every presheaf topos validates external PAx. As an example, let <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> be the category where <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Ob</mi><mo stretchy="false">(</mo><mi>C</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Ob(C)</annotation></semantics></math> is the disjoint sum <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℕ</mi><mo>∪</mo><mo stretchy="false">{</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\mathbb{N} \cup \{a, b\}</annotation></semantics></math>, and preordered by taking the reflexive transitive closure of relations <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>n</mi><mo>≤</mo><mi>n</mi><mo>+</mo><mn>1</mn></mrow><annotation encoding="application/x-tex">n \leq n+1</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>n</mi><mo>≤</mo><mi>a</mi></mrow><annotation encoding="application/x-tex">n \leq a</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>n</mi><mo>≤</mo><mi>b</mi></mrow><annotation encoding="application/x-tex">n \leq b</annotation></semantics></math>. The claim is that neither <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo>,</mo><mi>a</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">C(-, a)</annotation></semantics></math>, nor any presheaf <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> that maps epimorphically onto <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo>,</mo><mi>a</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">C(-, a)</annotation></semantics></math>, can be internally projective. Indeed, consider the presheaf <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> defined by <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo><mo>=</mo><mi>F</mi><mo stretchy="false">(</mo><mi>b</mi><mo stretchy="false">)</mo><mo>=</mo><mi>∅</mi></mrow><annotation encoding="application/x-tex">F(a) = F(b) = \emptyset</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>=</mo><mo stretchy="false">[</mo><mi>n</mi><mo>,</mo><mn>∞</mn><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">F(n) = [n,\infty)</annotation></semantics></math>, with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi><mo stretchy="false">(</mo><mi>n</mi><mo>+</mo><mn>1</mn><mo>→</mo><mi>n</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">F(n+1 \to n)</annotation></semantics></math> the evident inclusion. Let <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> be the <a class="existingWikiWord" href="/nlab/show/subterminal+object">support</a> 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>, so that we have an epi <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>e</mi><mo>:</mo><mi>F</mi><mo>→</mo><mi>G</mi></mrow><annotation encoding="application/x-tex">e: F \to G</annotation></semantics></math>.</p> <p>The objects <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo>,</mo><mi>a</mi><mo stretchy="false">)</mo><mo>,</mo><mi>C</mi><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">C(-, a), C(-, b)</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 <a class="existingWikiWord" href="/nlab/show/subterminal+object">subterminal</a> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>G</mi><mo>≅</mo><mi>C</mi><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo>,</mo><mi>a</mi><mo stretchy="false">)</mo><mo>∩</mo><mi>C</mi><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><mo>≅</mo><mi>C</mi><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo>,</mo><mi>a</mi><mo stretchy="false">)</mo><mo>×</mo><mi>C</mi><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">G \cong C(-, a) \cap C(-, b) \cong C(-, a) \times C(-, b)</annotation></semantics></math>. The set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>F</mi> <mrow><mi>C</mi><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo>,</mo><mi>a</mi><mo stretchy="false">)</mo></mrow></msup><mo stretchy="false">(</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">F^{C(-, a)}(b)</annotation></semantics></math> is empty because there is no <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo>,</mo><mi>a</mi><mo stretchy="false">)</mo><mo>×</mo><mi>C</mi><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><mo>→</mo><mi>F</mi></mrow><annotation encoding="application/x-tex">C(-, a) \times C(-, b) \to F</annotation></semantics></math> (it would give a section <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>G</mi><mo>→</mo><mi>F</mi></mrow><annotation encoding="application/x-tex">G \to F</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>e</mi><mo>:</mo><mi>F</mi><mo>→</mo><mi>G</mi></mrow><annotation encoding="application/x-tex">e: F \to G</annotation></semantics></math>, but none exists), whereas <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>G</mi> <mrow><mi>C</mi><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo>,</mo><mi>a</mi><mo stretchy="false">)</mo></mrow></msup><mo stretchy="false">(</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">G^{C(-, a)}(b)</annotation></semantics></math> is inhabited by <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo>,</mo><mi>a</mi><mo stretchy="false">)</mo><mo>×</mo><mi>C</mi><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><mo>≅</mo><mi>G</mi></mrow><annotation encoding="application/x-tex">C(-, a) \times C(-, b) \cong G</annotation></semantics></math>. For any <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> covering <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo>,</mo><mi>a</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">C(-, a)</annotation></semantics></math>, the set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>F</mi> <mi>P</mi></msup><mo stretchy="false">(</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">F^P(b)</annotation></semantics></math> is empty (because any section <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>s</mi><mo>:</mo><mi>C</mi><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo>,</mo><mi>a</mi><mo stretchy="false">)</mo><mo>→</mo><mi>P</mi></mrow><annotation encoding="application/x-tex">s: C(-, a) \to P</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo>→</mo><mi>C</mi><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo>,</mo><mi>a</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">P \to C(-, a)</annotation></semantics></math> induces a function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>F</mi> <mi>P</mi></msup><mo stretchy="false">(</mo><mi>b</mi><mo stretchy="false">)</mo><mo>→</mo><msup><mi>F</mi> <mrow><mi>C</mi><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo>,</mo><mi>a</mi><mo stretchy="false">)</mo></mrow></msup><mo stretchy="false">(</mo><mi>b</mi><mo stretchy="false">)</mo><mo>=</mo><mn>0</mn></mrow><annotation encoding="application/x-tex">F^P(b) \to F^{C(-, a)}(b) = 0</annotation></semantics></math>), and the set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>G</mi> <mi>P</mi></msup><mo stretchy="false">(</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">G^P(b)</annotation></semantics></math> is inhabited (the map <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo>→</mo><mi>C</mi><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo>,</mo><mi>a</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">P \to C(-, a)</annotation></semantics></math> induces a map <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>1</mn><mo>≅</mo><msup><mi>G</mi> <mrow><mi>C</mi><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo>,</mo><mi>a</mi><mo stretchy="false">)</mo></mrow></msup><mo stretchy="false">(</mo><mi>b</mi><mo stretchy="false">)</mo><mo>→</mo><msup><mi>G</mi> <mi>P</mi></msup><mo stretchy="false">(</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">1 \cong G^{C(-, a)}(b) \to G^P(b)</annotation></semantics></math>). Thus the map <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>e</mi> <mi>P</mi></msup><mo lspace="verythinmathspace">:</mo><msup><mi>F</mi> <mi>P</mi></msup><mo>→</mo><msup><mi>G</mi> <mi>P</mi></msup></mrow><annotation encoding="application/x-tex">e^P \colon F^P \to G^P</annotation></semantics></math> cannot be epic.</p> </div> <div class="num_example"> <h6 id="counterexample_2">Counterexample</h6> <p>Any topos that violates countable choice, of which there are plenty, must also violate internal PAx.</p> </div> <div class="num_example"> <h6 id="example_3">Example</h6> <p>An interesting example of a topos that has enough projectives and satisfies internal CoSHEP (at least, assuming the axiom of choice in <a class="existingWikiWord" href="/nlab/show/Set">Set</a>), although it violates the full (internal) axiom of choice, is the <a class="existingWikiWord" href="/nlab/show/effective+topos">effective topos</a>, and more generally any <a class="existingWikiWord" href="/nlab/show/realizability+topos">realizability topos</a>. The reason for this is quite similar to the intuitive justification for CoSHEP given above. Technically, it results from the fact that realizability toposes are <a class="existingWikiWord" href="/nlab/show/exact+completions">exact completions</a>; an explanation is given in <a href="/nlab/show/realizability+topos#pax">this remark</a>.</p> </div> <p>For a Grothendieck topos example, the sheaves on the interval <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">[</mo><mn>0</mn><mo>,</mo><mn>1</mn><mo stretchy="false">]</mo></mrow><annotation encoding="application/x-tex">[0,1]</annotation></semantics></math> with its usual topology give a topos in which the internal axiom of countable choice fails, hence internal PAx must also fail.</p> <h2 id="in_categories_which_are_not_topoi">In categories which are not topoi</h2> <div class="num_example"> <h6 id="example_4">Example</h6> <p>According to Peter Scholze in <a href="https://golem.ph.utexas.edu/category/2020/03/pyknoticity_versus_cohesivenes.html#c057798">this comment on the nCafé</a>, an example of a category that satisfies external CoSHEP is the category of <a class="existingWikiWord" href="/nlab/show/condensed+sets">condensed sets</a>, assuming that <a class="existingWikiWord" href="/nlab/show/Set">Set</a> satisfies the axiom of choice. The category of condensed sets do not form a topos, only an <a class="existingWikiWord" href="/nlab/show/infinitary+pretopos">infinitary pretopos</a>.</p> <p>However, internal CoSHEP fails in condensed sets.</p> </div> <h2 id="further_properties">Further properties</h2> <p>Since <a class="existingWikiWord" href="/nlab/show/Set">Set</a> is (essentially regardless of foundations) an <a class="existingWikiWord" href="/nlab/show/exact+category">exact category</a>, if it has <a href="projective+object#EnoughProjectives">enough projectives</a> then it must be the <em>free</em> <a class="existingWikiWord" href="/nlab/show/exact+category">exact category</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>PSet</mi> <mrow><mi>ex</mi><mo stretchy="false">/</mo><mi>lex</mi></mrow></msub></mrow><annotation encoding="application/x-tex">PSet_{ex/lex}</annotation></semantics></math> generated by its <a class="existingWikiWord" href="/nlab/show/subcategory">subcategory</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>PSet</mi></mrow><annotation encoding="application/x-tex">PSet</annotation></semantics></math> of <a class="existingWikiWord" href="/nlab/show/projective+objects">projective objects</a>. By the construction of the <a href="regular+and+exact+completions#TheExLexCompletion">ex/lex completion</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>PSet</mi> <mrow><mi>ex</mi><mo stretchy="false">/</mo><mi>lex</mi></mrow></msub></mrow><annotation encoding="application/x-tex">PSet_{ex/lex}</annotation></semantics></math>, it follows that every set is the quotient of some “pseudo-equivalence relation” in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>PSet</mi></mrow><annotation encoding="application/x-tex">PSet</annotation></semantics></math>; i.e., the result of imposing an equality relation on some completely presented set. See <a class="existingWikiWord" href="/nlab/show/SEAR+plus+epsilon">SEAR+ε</a> for an application of this idea.</p> <div class="num_prop"> <h6 id="proposition_3">Proposition</h6> <p>CoSHEP as a choice principle added to <a class="existingWikiWord" href="/nlab/show/ZF">ZF</a> implies a <a class="existingWikiWord" href="/nlab/show/proper+class">proper class</a> of <a class="existingWikiWord" href="/nlab/show/regular+cardinals">regular cardinals</a>.</p> </div> <div class="proof"> <h6 id="proof_2">Proof</h6> <p>Since CoSHEP implies <a class="existingWikiWord" href="/nlab/show/WISC">WISC</a>, and WISC has this implication (a result of <a class="existingWikiWord" href="/nlab/show/Benno+van+den+Berg">van den Berg</a>).</p> </div> <h2 id="in_higher_category_theory"> In higher category theory</h2> <p>In <a class="existingWikiWord" href="/nlab/show/higher+category+theory">higher category theory</a>, there are different versions of CoSHEP:</p> <ul> <li> <p>For every <a class="existingWikiWord" href="/nlab/show/0-groupoid">0-groupoid</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>, there exists 0-groupoid <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> and <a class="existingWikiWord" href="/nlab/show/effective+epimorphism">effective epimorphism</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo>→</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">P \to A</annotation></semantics></math>, such that for all 0-groupoids <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> there exists effective epimorphism <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi><mo>→</mo><mi>P</mi></mrow><annotation encoding="application/x-tex">X \to P</annotation></semantics></math> with <a class="existingWikiWord" href="/nlab/show/section">section</a>.</p> </li> <li> <p>For every <a class="existingWikiWord" href="/nlab/show/infinity-groupoid">infinity-groupoid</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>, there exists 0-groupoid <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> and <a class="existingWikiWord" href="/nlab/show/effective+epimorphism">effective epimorphism</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo>→</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">P \to A</annotation></semantics></math>, such that for all 0-groupoids <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> there exists effective epimorphism <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi><mo>→</mo><mi>P</mi></mrow><annotation encoding="application/x-tex">X \to P</annotation></semantics></math> with <a class="existingWikiWord" href="/nlab/show/section">section</a>.</p> </li> </ul> <p>The difference between these versions of CoSHEP is that <a class="existingWikiWord" href="/nlab/show/sets+cover">sets cover</a>.</p> <h2 id="justification">Justification</h2> <p>Although perhaps not well known in the literature of <a class="existingWikiWord" href="/nlab/show/constructive+mathematics">constructive mathematics</a>, the CoSHEP axiom may be justified by the sort of reasoning usually accepted to justify the <a class="existingWikiWord" href="/nlab/show/axiom+of+countable+choice">axioms of countable choice</a> and <a class="existingWikiWord" href="/nlab/show/axiom+of+dependent+choice">dependent choice</a>, which it implies, by Proposition <a class="maruku-ref" href="#ImpliesDependentAndCountableChoice"></a> above.</p> <p>To be explicit, every set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> should have a ‘completely presented’ set of ‘canonical’ <a class="existingWikiWord" href="/nlab/show/elements">elements</a>, that is elements given directly as they are constructed without regard for the <a class="existingWikiWord" href="/nlab/show/equality+relation">equality relation</a> imposed upon them. For canonical elements, <a class="existingWikiWord" href="/nlab/show/equality">equality</a> is identity, so the <a class="existingWikiWord" href="/nlab/show/BHK+interpretation">BHK interpretation</a> of logic justifies the axiom of choice for a completely presented set. This set is <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>, and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> is obtained from it as a <a class="existingWikiWord" href="/nlab/show/quotient+set">quotient</a> by the relation of equality on <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>. This argument can be made precise in some forms of <a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a>, which thus justify CoSHEP, much as they are widely known to justify dependent choice.</p> <h2 id="related_concepts">Related concepts</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/projective+object">projective object</a>, <a class="existingWikiWord" href="/nlab/show/projective+presentation">projective presentation</a>, <a class="existingWikiWord" href="/nlab/show/projective+cover">projective cover</a>, <a class="existingWikiWord" href="/nlab/show/projective+resolution">projective resolution</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/projective+module">projective module</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/internally+projective+object">internally projective object</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/injective+object">injective object</a>, <a class="existingWikiWord" href="/nlab/show/injective+presentation">injective presentation</a>, <a class="existingWikiWord" href="/nlab/show/injective+envelope">injective envelope</a>, <a class="existingWikiWord" href="/nlab/show/injective+resolution">injective resolution</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/injective+module">injective module</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/free+object">free object</a>, <a class="existingWikiWord" href="/nlab/show/free+resolution">free resolution</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/free+module">free module</a></li> </ul> </li> <li> <p>flat object, <a class="existingWikiWord" href="/nlab/show/flat+resolution">flat resolution</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/flat+module">flat module</a></li> </ul> </li> </ul> <h2 id="references">References</h2> <p>When <a class="existingWikiWord" href="/nlab/show/Peter+Aczel">Peter Aczel</a> was developing <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>CZF</mi></mrow><annotation encoding="application/x-tex">CZF</annotation></semantics></math> (a constructive predicative version of <a class="existingWikiWord" href="/nlab/show/ZFC">ZFC</a>), he considered this axiom, under the name of the <em>presentation axiom</em>, but ultimately rejected it.</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Peter+Aczel">Peter Aczel</a>, <em>The type theoretic interpretation of constructive set theory</em>. Logic Colloquium ‘77 (Proc. Conf., Wroclaw, 1977), pp. 55–66, Stud. Logic Foundations Math., 96, North-Holland, Amsterdam-New York, 1978. doi:<a href="https://doi.org/10.1016/S0049-237X%2808%2971989-X">10.1016/S0049-237X(08)71989-X</a></li> </ul> <p>The presentation axiom was, however, adopted by <a class="existingWikiWord" href="/nlab/show/Erik+Palmgren">Erik Palmgren</a> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>CETCS</mi></mrow><annotation encoding="application/x-tex">CETCS</annotation></semantics></math> (a constructive predicative version of <a class="existingWikiWord" href="/nlab/show/ETCS">ETCS</a>):</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 <p><strong>163</strong> Issue 10 (2012) 1384–1399, doi:<a href="https://doi.org/10.1016/j.apal.2012.01.011">10.1016/j.apal.2012.01.011</a> arXiv:<a href="https://arxiv.org/abs/1201.6272">1201.6272</a>, <a href="http://www.math.uu.se/~palmgren/cetcs.pdf">author pdf</a>.</p> </li> </ul> <p>Its relationship to some other weak axioms of choice is studied in</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Michael+Rathjen">Michael Rathjen</a>, <em>Choice principles in constructive and classical set theories</em>, In: Z. Chatzidakis, P. Koepke, & W. Pohlers (Eds.), Logic Colloquium ‘02 (Lecture Notes in Logic, pp. 299-326) (2006). Cambridge: Cambridge University Press. doi:<a href="https://doi.org/10.1017/9781316755723.014">10.1017/9781316755723.014</a>. <a href="http://www1.maths.leeds.ac.uk/~rathjen/acend.pdf">author pdf</a>.</li> </ul> <div class="property">category: <a class="category_link" href="/nlab/all_pages/foundational+axiom">foundational axiom</a></div></body></html> </div> <div class="revisedby"> <p> Last revised on February 23, 2024 at 23:23:51. See the <a href="/nlab/history/presentation+axiom" 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/presentation+axiom" accesskey="E" class="navlink" id="edit" rel="nofollow">Edit</a><a href="https://nforum.ncatlab.org/discussion/4368/#Item_15">Discuss</a><span class="backintime"><a href="/nlab/revision/presentation+axiom/51" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/diff/presentation+axiom" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Changes from previous revision</a><a href="/nlab/history/presentation+axiom" accesskey="S" class="navlink" id="history" rel="nofollow">History (51 revisions)</a> <a href="/nlab/show/presentation+axiom/cite" style="color: black">Cite</a> <a href="/nlab/print/presentation+axiom" accesskey="p" id="view_print" rel="nofollow">Print</a> <a href="/nlab/source/presentation+axiom" id="view_source" rel="nofollow">Source</a> </div> </div>  </div>  </body> </html>