The Clowder Project

Let $\webleft (X,x_{0}\webright )$ be a pointed set.

1. Completeness. The category $\mathsf{Sets}_{*}$ of pointed sets and morphisms between them is complete, having in particular:
   1. Products, described as in Definition 3.2.3.1.1;
   2. Pullbacks, described as in Definition 3.2.4.1.1;
   3. Equalisers, described as in Definition 3.2.5.1.1.
2. Cocompleteness. The category $\mathsf{Sets}_{*}$ of pointed sets and morphisms between them is cocomplete, having in particular:
   1. Coproducts, described as in Definition 3.3.3.1.1;
   2. Pushouts, described as in Definition 3.3.4.1.1;
   3. Coequalisers, described as in Definition 3.3.5.1.1.
3. Failure To Be Cartesian Closed. The category $\mathsf{Sets}_{*}$ is not Cartesian closed.^[1]
4. Morphisms From the Monoidal Unit. We have a bijection of sets^[2]
   \[ \mathsf{Sets}_{*}\webleft (S^{0},X\webright ) \cong X, \]

   natural in $\webleft (X,x_{0}\webright )\in \text{Obj}\webleft (\mathsf{Sets}_{*}\webright )$, internalising also to an isomorphism of pointed sets

   \[ \textbf{Sets}_{*}\webleft (S^{0},X\webright ) \cong \webleft (X,x_{0}\webright ), \]

   again natural in $\webleft (X,x_{0}\webright )\in \text{Obj}\webleft (\mathsf{Sets}_{*}\webright )$.

5. Relation to Partial Functions. We have an equivalence of categories^[3]
   \[ \mathsf{Sets}_{*}\mathrel {\smash {\overset {\scriptscriptstyle \text{eq.}}\cong }}\mathsf{Sets}^{\mathrm{part.}} \]

   between the category of pointed sets and pointed functions between them and the category of sets and partial functions between them, where:

   1. From Pointed Sets to Sets With Partial Functions. The equivalence
      \[ \xi \colon \mathsf{Sets}_{*}\mathbin {\overset {\cong }{\rightarrow }}\mathsf{Sets}^{\mathrm{part.}} \]

      sends:

      1. A pointed set $\webleft (X,x_{0}\webright )$ to $X$.
      2. A pointed function
         \[ f\colon \webleft (X,x_{0}\webright )\to \webleft (Y,y_{0}\webright ) \]

         to the partial function

         \[ \xi _{f}\colon X\to Y \]

         defined on $f^{-1}\webleft (Y\setminus y_{0}\webright )$ and given by

         \[ \xi _{f}\webleft (x\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}f\webleft (x\webright ) \]

         for each $x\in f^{-1}\webleft (Y\setminus y_{0}\webright )$.

   2. From Sets With Partial Functions to Pointed Sets. The equivalence
      \[ \xi ^{-1}\colon \mathsf{Sets}^{\mathrm{part.}}\mathbin {\overset {\cong }{\rightarrow }}\mathsf{Sets}_{*} \]

      sends:

      1. A set $X$ is to the pointed set $\webleft (X,\star \webright )$ with $\star $ an element that is not in $X$.
      2. A partial function
         \[ f\colon X\to Y \]

         defined on $U\subset X$ to the pointed function

         \[ \xi ^{-1}_{f}\colon \webleft (X,x_{0}\webright )\to \webleft (Y,y_{0}\webright ) \]

         defined by

         \[ \xi _{f}\webleft (x\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\begin{cases} f\webleft (x\webright ) & \text{if $x\in U$,}\\ y_{0} & \text{otherwise.} \end{cases} \]

         for each $x\in X$.