diff --git a/databases/catdat/data/categories/Set.yaml b/databases/catdat/data/categories/Set.yaml
index 96acaef9..12b34127 100644
--- a/databases/catdat/data/categories/Set.yaml
+++ b/databases/catdat/data/categories/Set.yaml
@@ -17,6 +17,7 @@ related_categories:
- Set_f
- SetxSet
- Setne
+ - Set_arrow
satisfied_properties:
- property: locally small
diff --git a/databases/catdat/data/categories/Set_arrow.yaml b/databases/catdat/data/categories/Set_arrow.yaml
new file mode 100644
index 00000000..3a9c2d79
--- /dev/null
+++ b/databases/catdat/data/categories/Set_arrow.yaml
@@ -0,0 +1,71 @@
+id: Set_arrow
+name: category of set functions and commutative squares
+notation: $\Set^{\rightarrow}$
+objects: >-
+ triples $(X, Y, f)$ where $X$ and $Y$ are sets, and $f : X \to Y$ is a function
+morphisms: >-
+ a morphism $(X, Y, f) \to (X', Y', f')$ is a pair of functions $\ell : X \to X'$ and $r : Y \to Y'$ making a commutative square
+ $$\begin{CD}
+ X @>{f}>> Y \\
+ @V{\ell}VV @VV{r}V \\
+ X' @>>{f'}> Y'
+ \end{CD}$$
+description: This category is an example of the arrow category $\Arr(\C)$, where $\C$ is the category of sets. It is also known as the Sierpinski topos, since it is equivalent to the category of sheaves on the Sierpinski space.
+nlab_link: https://ncatlab.org/nlab/show/Sierpinski+topos
+
+tags:
+ - set theory
+
+related_categories:
+ - Set
+ - SetxSet
+ - Sh(X)
+
+satisfied_properties:
+ - property: locally small
+ proof: This is easy.
+
+ - property: semi-strongly connected
+ proof: >-
+ Consider two objects $(X, Y, f)$ and $(X', Y', f')$. If $X'$ is non-empty with element $x'$, we can construct a morphism $(\ell, r) : (X, Y, f) \to (X', Y', f')$ where $\ell$ is the constant function with value $x'$, and $r$ is the constant function with value $f'(x')$; and similarly if $X$ is non-empty we can construct a morphism $(X', Y', f') \to (X, Y, f)$. Otherwise, if $X$ and $X'$ are both empty, we can reduce to the fact that $\Set$ is semi-strongly connected to find $r$ in one direction, and fill in $\ell$ as the unique function $\varnothing \to \varnothing$.
+
+ - property: Grothendieck topos
+ proof: It is equivalent to the category of presheaves on the walking morphism.
+
+ - property: locally strongly finitely presentable
+ proof: It is equivalent to the category of models of the algebraic theory with two sorts, and a single unary operation from one sort to the other.
+
+unsatisfied_properties:
+ - property: skeletal
+ proof: 'Consider $\id_X : X \to X$ and $\id_Y : Y \to Y$ for isomorphic but non-equal sets $X$ and $Y$.'
+
+ - property: generator
+ proof: >-
+ Suppose $\Set^{\rightarrow}$ had a generator. Then by this result, every subterminal object would be either initial or terminal. However, in fact, $0 \to 1$ is a subterminal object which is isomorphic to neither the initial object $0 \to 0$ nor the terminal object $1 \to 1$.
+
+special_objects:
+ initial object:
+ description: the unique function $0 \to 0$
+ terminal object:
+ description: the unique function $1 \to 1$
+ coproducts:
+ description: component-wise defined disjoint union, equipped with the disjoint union of the functions
+ products:
+ description: component-wise defined cartesian product, equipped with the product function
+
+special_morphisms:
+ isomorphisms:
+ description: pairs $(\ell, r)$ where $\ell$ and $r$ are both bijections
+ proof: This is easy.
+ monomorphisms:
+ description: pairs $(\ell, r)$ where $\ell$ and $r$ are both injective
+ proof: For the non-trivial direction, use the fact that the domain functor taking an object $(X, Y, f)$ to $X$ and a morphism $(\ell, r)$ to $\ell$ is representable by $1 \to 1$; and moreover, the codomain functor taking an object $(X, Y, f)$ to $Y$ and a morphism $(\ell, r)$ to $r$ is representable by $0 \to 1$.
+ epimorphisms:
+ description: pairs $(\ell, r)$ where $\ell$ and $r$ are both surjective
+ proof: For the non-trivial direction, use the fact that the category is epi-regular, so any epimorphism is a coequalizer; and the fact that coequalizers can be calculated component-wise.
+ regular monomorphisms:
+ description: same as monomorphisms
+ proof: This is because the category is mono-regular.
+ regular epimorphisms:
+ description: same as epimorphisms
+ proof: This is because the category is epi-regular.
diff --git a/databases/catdat/data/categories/SetxSet.yaml b/databases/catdat/data/categories/SetxSet.yaml
index e16932f7..a8d324b5 100644
--- a/databases/catdat/data/categories/SetxSet.yaml
+++ b/databases/catdat/data/categories/SetxSet.yaml
@@ -11,6 +11,7 @@ tags:
related_categories:
- Set
+ - Set_arrow
- Sh(X)
satisfied_properties:
diff --git a/databases/catdat/data/categories/Sh(X).yaml b/databases/catdat/data/categories/Sh(X).yaml
index 75c56ed1..e5459ab9 100644
--- a/databases/catdat/data/categories/Sh(X).yaml
+++ b/databases/catdat/data/categories/Sh(X).yaml
@@ -13,6 +13,7 @@ tags:
related_categories:
- Set
- SetxSet
+ - Set_arrow
- Sh(X,Ab)
comments:
diff --git a/databases/catdat/data/macros.yaml b/databases/catdat/data/macros.yaml
index ef3c6a26..844eb044 100644
--- a/databases/catdat/data/macros.yaml
+++ b/databases/catdat/data/macros.yaml
@@ -121,3 +121,4 @@
\Isom: \mathbf{Isom}
\Pair: \mathbf{Pair}
\Span: \mathbf{Span}
+\Arr: \mathbf{Arr}