\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{presentation axiom}

\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

\hypertarget{foundations}{}\paragraph*{{Foundations}}\label{foundations}

[[!include foundations - contents]]

\hypertarget{contents}{}\section*{{Contents}}\label{contents}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{Statement}{Statement}\dotfill \pageref*{Statement} \linebreak
\noindent\hyperlink{justification}{Justification}\dotfill \pageref*{justification} \linebreak
\noindent\hyperlink{consequences}{Consequences}\dotfill \pageref*{consequences} \linebreak
\noindent\hyperlink{topos}{In a topos}\dotfill \pageref*{topos} \linebreak
\noindent\hyperlink{further_properties}{Further properties}\dotfill \pageref*{further_properties} \linebreak
\noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

In the [[foundations]] of [[mathematics]], it's interesting to consider the axiom that the [[Set|Category of Sets]] Has [[projective object|Enough Projectives]]; in short: \textbf{CoSHEP} (pronounced /ko:-shep/). This is more commonly known as the \textbf{presentation axiom}: PAx. It is a weak form of the [[axiom of choice]].

\hypertarget{Statement}{}\subsection*{{Statement}}\label{Statement}

In elementary terms, CoSHEP states

\begin{defn}
\label{}\hypertarget{}{}
For every [[set]] $A$, there exists a set $P$ and a [[surjection]] $P \to A$, such that every surjection $X \twoheadrightarrow P$ has a [[section]].

\end{defn}
\begin{remark}
\label{}\hypertarget{}{}
The full axiom of choice states that every surjection $X \to A$ has a section; hence in the above $P$ may be chosen to be $A$ itself.

\end{remark}
This should be read in view of the definition of \emph{[[projective objects]]}:

\begin{defn}
\label{}\hypertarget{}{}
An [[object]] $P$ in a [[category]] $C$ is (externally) [[projective object|projective]] iff the [[hom-functor]] $C(P, -): C \to Set$ takes [[epimorphism|epis]] to epis. This is the same as saying: given an epi $p: B \to A$ and a map $f: P \to A$, there exists a lift $g: P \to B$ in the sense that $f = p \circ g$.

\end{defn}
Accordingly, in a [[topos]] the CoSHEP axiom says equivalently

\begin{defn}
\label{}\hypertarget{}{}
Every object has a [[projective presentation]]. Hence: There are \href{projective+object#EnoughProjectives}{enough projectives}.

\end{defn}
Borrowing from the philosophy of [[constructive mathematics|constructivism]], we may also call this a \emph{complete presentation}.

\begin{remark}
\label{}\hypertarget{}{}
The [[duality|dual]] axiom, that $Set$ has \href{injective+object#EnoughInjectives}{enough injectives} (that is, every set admits an injection into an injective set) is [[true]] in every [[topos]]: every [[power object]] is an [[injective object]], and every object $X$ embeds in its power object $P X$ via the [[singleton subset|singleton]] map $\{\cdot\}:X\hookrightarrow P X$.

\end{remark}
\hypertarget{justification}{}\subsection*{{Justification}}\label{justification}

Although perhaps not well known in the literature of [[constructive mathematics]], the CoSHEP axiom may be justified by the sort of reasoning usually accepted to justify the [[axiom of countable choice|axioms of countable choice]] and [[axiom of dependent choice|dependent choice]] (which it implies, by Proposition \ref{ImpliesDependentAndCountableChoice} below).

To be explicit, every set $A$ should have a `completely presented' set of `canonical' [[elements]], that is elements given directly as they are constructed without regard for the [[equality relation]] imposed upon them. For canonical elements, [[equality]] is identity, so the [[BHK interpretation]] of logic justifies the axiom of choice for a completely presented set. This set is $P$, and $A$ is obtained from it as a [[quotient set|quotient]] by the relation of equality on $A$. This argument can be made precise in many forms of [[type theory]] (including those of Martin-L\"o{}f and Thierry Coquand), which thus justify CoSHEP, much as they are widely known to justify dependent choice.

\hypertarget{consequences}{}\subsection*{{Consequences}}\label{consequences}

The existence of sufficiently many [[projective presentations]] plays a central role in [[homological algebra]] as a means to construct [[projective resolutions]] of objects. Tradtionally one often uses the [[axiom of choice]] to prove that [[categories of modules]] have \href{projective+object#EnoughProjectives}{enough projectives}, on the grounds that the [[free modules]] are projective.

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 [[projective presentation]] for every free module (and thus for every module). This is discussed in more detail \href{projective+object#EnoughWithCOSHEP}{here}.

\begin{prop}
\label{ImpliesDependentAndCountableChoice}\hypertarget{ImpliesDependentAndCountableChoice}{}
The following three conditions on a [[W-pretopos]] with \href{projective+object#EnoughProjectives}{enough projectives} are equivalent:

\begin{enumerate}%
\item The axiom of [[dependent choice]] (DC),


\item The axiom of [[countable choice]] (CC),


\item Projectivity of the [[singleton]] (the [[terminal object]]) $1$.



\end{enumerate}
\end{prop}
Note that we normally assume (3) for [[the category of sets]], which is true in any (constructively) [[well-pointed pretopos]] and true \emph{[[internalization|internally]]} 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.

\begin{proof}
Condition 1 easily implies 2. Condition 2 says precisely that the [[natural numbers object]] $\mathbb{N}$ is externally projective, and since $1$ is a retract of $\mathbb{N}$, it is projective under condition 2, so 2 implies 3. It remains to show 3 implies 1.

Let $X$ be inhabited, so there exists an [[entire relation]] given by a jointly monic span

\begin{displaymath}
1 \stackrel{epi}{\leftarrow} U \stackrel{f}{\to} X,
\end{displaymath}
and similarly let

\begin{displaymath}
X \stackrel{epi \pi_1}{\leftarrow} R \stackrel{\pi_2}{\to} X
\end{displaymath}
be an [[entire relation|entire binary relation]]. Let $p: P \to X$ be a projective cover. Since $1$ is assumed projective, the cover $U \to 1$ admits a section $\sigma: 1 \to U$, and the element $f \sigma: 1 \to X$ lifts through $p$ to an element $x_0: 1 \to P$. Next, in the diagram below, $p$ lifts through the epi $\pi_1$ to a map $q: P \to R$, and then $\pi_2 q$ lifts through $p$ to a map $\phi$ (since $P$ is projective):

\begin{displaymath}
\itexarray{
 & & P  & \stackrel{\phi}{\to} & P \\
 & \swarrow p & \downarrow q & & \downarrow p \\
X & \underset{\pi_1}{\leftarrow} & R & \underset{\pi_2}{\to} & X
}
\end{displaymath}
By the universal property of $\mathbb{N}$ (see [[recursion]]), there exists a unique map $h: \mathbb{N} \to P$ rendering commutative the diagram

\begin{displaymath}
\itexarray{
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
}
\end{displaymath}
Clearly $\langle p h, p h s \rangle : \mathbb{N} \to X \times X$ factors through $\langle \pi_1, \pi_2 \rangle : R \to X \times X$, i.e., $\forall_{n: \mathbb{N}} (p h(n), p h(n+1)) \in R$, thus proving that dependent choice holds under CoSHEP.

\end{proof}
\begin{example}
\label{}\hypertarget{}{}
A topos in which CoSHEP holds but $1$ is not projective is $Set^C$, where $C$ is the category with three objects and exactly two non-identity arrows $a \to b \leftarrow c$. For if $U: C \to Set$ is a functor with $U(a) = \{a_0\}$, $U(b) = \{b_0, b_1\}$, and $U(c) = \{c_0\}$, with $U(a \to b)(a_0) = b_0$ and $U(c \to b)(c_0) = b_1$, then the map $U \to 1$ is epi but has no section, so $1$ is not projective. On the other hand, as noted below, every presheaf topos satisfies CoSHEP, assuming that $Set$ itself does.

\end{example}
CoSHEP also implies several weaker forms of choice, such as the [[axiom of multiple choice]] and [[WISC]]. In weakly [[predicative mathematics]], it can be combined with the existence of [[function sets]] to show the [[subset collection]] axiom.

\hypertarget{topos}{}\subsection*{{In a topos}}\label{topos}

When working in the [[internal logic]] of a [[topos]], the ``internal'' meaning of CoSHEP is ``every object is covered by an [[internally projective object]].'' (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.

\begin{prop}
\label{}\hypertarget{}{}
Suppose that $1$ is (externally) projective in $E$. Then $E$ satisfies PAx whenever it satisfies internal PAx.

\end{prop}
Internal PAx does not follows from external PAx; see Counterexample 5.3. However, if \emph{every} object is projective (AC), then every object is internally projective (IAC).

A stronger version of PAx may be worth considering. Say that an object is \textbf{stably projective} if its [[pullback]] to any [[slice category]] is projective. Then stably projective objects are internally projective (proof?). Similarly, if we say that a topos $E$ satisfies stable PAx if every object is covered by a stably projective object, then a topos satisfies internal PAx if it satisfies stable PAx.

\begin{example}
\label{}\hypertarget{}{}
Every [[presheaf topos]] $Set^{C^{op}}$ has enough projectives, since any coproduct of representables is projective. If in addition $C$ has binary products, then by \href{/nlab/show/internally+projective+object#presheaf}{this result}, $Set^{C^{op}}$ validates internal PAx.

\end{example}
\begin{example}
\label{counter}\hypertarget{counter}{}
However, not every presheaf topos validates internal PAx, even though every presheaf topos validates external PAx. As an example, let $C$ be the category where $Ob(C)$ is the disjoint sum $\mathbb{N} \cup \{a, b\}$, and preordered by taking the reflexive transitive closure of relations $n \leq n+1$, $n \leq a$, $n \leq b$. The claim is that neither $C(-, a)$, nor any presheaf $P$ that maps epimorphically onto $C(-, a)$, can be internally projective. Indeed, consider the presheaf $F$ defined by $F(a) = F(b) = \emptyset$ and $F(n) = [n,\infty)$, with $F(n+1 \to n)$ the evident inclusion. Let $G$ be the [[subterminal object|support]] of $F$, so that we have an epi $e: F \to G$.

The objects $C(-, a), C(-, b)$, and $G$ are [[subterminal object|subterminal]] and $G \cong C(-, a) \cap C(-, b) \cong C(-, a) \times C(-, b)$. The set $F^{C(-, a)}(b)$ is empty because there is no $C(-, a) \times C(-, b) \to F$ (it would give a section $G \to F$ of $e: F \to G$, but none exists), whereas $G^{C(-, a)}(b)$ is inhabited by $C(-, a) \times C(-, b) \cong G$. For any $P$ covering $C(-, a)$, the set $F^P(b)$ is empty (because any section $s: C(-, a) \to P$ of $P \to C(-, a)$ induces a function $F^P(b) \to F^{C(-, a)}(b) = 0$), and the set $G^P(b)$ is inhabited (the map $P \to C(-, a)$ induces a map $1 \cong G^{C(-, a)}(b) \to G^P(b)$). Thus the map $e^P \colon F^P \to G^P$ cannot be epic.

\end{example}
\begin{example}
\label{}\hypertarget{}{}
Any topos that violates countable choice, of which there are plenty, must also violate internal PAx.

\end{example}
\begin{example}
\label{}\hypertarget{}{}
An interesting example of a topos that has enough projectives and satisfies internal CoSHEP (at least, assuming the axiom of choice in [[Set]]), although it violates the full (internal) axiom of choice, is the [[effective topos]], and more generally any [[realizability topos]]. 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 [[exact completions]]; an explanation is given in \href{/nlab/show/realizability+topos#pax}{this remark}.

\end{example}
\hypertarget{further_properties}{}\subsection*{{Further properties}}\label{further_properties}

Since [[Set]] is (essentially regardless of foundations) an [[exact category]], if it has \href{projective+object#EnoughProjectives}{enough projectives} then it must be the \emph{free} [[exact category]] $PSet_{ex/lex}$ generated by its [[subcategory]] $PSet$ of [[projective objects]]. By the construction of the \href{regular+and+exact+completions#TheExLexCompletion}{ex/lex completion} $PSet_{ex/lex}$, it follows that every set is the quotient of some ``pseudo-equivalence relation'' in $PSet$; i.e., the result of imposing an equality relation on some completely presented set. See [[SEAR+ε]] for an application of this idea.

\begin{prop}
\label{}\hypertarget{}{}
CoSHEP as a choice principle added to [[ZF]] implies a [[proper class]] of [[regular cardinals]].

\end{prop}
\begin{proof}
Since CoSHEP implies [[WISC]], and WISC has this implication (a result of [[Benno van den Berg|van den Berg]]).

\end{proof}
\hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts}

\begin{itemize}%
\item [[projective object]], [[projective presentation]], [[projective cover]], [[projective resolution]]

\begin{itemize}%
\item [[projective module]]


\item [[internally projective object]]



\end{itemize}

\item [[injective object]], [[injective presentation]], [[injective envelope]], [[injective resolution]]

\begin{itemize}%
\item [[injective module]]

\end{itemize}

\item [[free object]], [[free resolution]]

\begin{itemize}%
\item [[free module]]

\end{itemize}

\item flat object, [[flat resolution]]

\begin{itemize}%
\item [[flat module]]

\end{itemize}


\end{itemize}
\hypertarget{references}{}\subsection*{{References}}\label{references}

When [[Peter Aczel]] was developing $CZF$ (a constructive predicative version of [[ZFC]]), he considered this axiom, under the name of the \emph{presentation axiom}, but ultimately rejected it.

\begin{itemize}%
\item Peter Aczel. \emph{The type theoretic interpretation of constructive set theory}. Logic Colloquium `77 (Proc. Conf., Wroclaw, 1977), pp. 55--66, Stud. Logic Foundations Math., 96, North-Holland, Amsterdam-New York, 1978. Cited in Palmgren, below.

\end{itemize}
The presentation axiom was, however, adopted by [[Erik Palmgren]] in $CETCS$ (a constructive predicative version of [[ETCS]]):

\begin{itemize}%
\item Erik Palmgren. \emph{Constructivist and Structuralist Foundations: Bishop's and Lawvere's Theories of Sets}. \href{http://www.math.uu.se/~palmgren/cetcs.pdf}{pdf}.

\end{itemize}
Its relationship to some other weak axioms of choice is studied in

\begin{itemize}%
\item [[Michael Rathjen]], \emph{Choice principles in constructive and classical set theories}.

\end{itemize}
category: foundational axiom

[[!redirects presentation axiom]] [[!redirects PAX]] [[!redirects PAx]] [[!redirects pax]] [[!redirects COSHEP]] [[!redirects CoSHEP]] [[!redirects coshep]]



\end{document}