From 0399d0fc6c81f28a42b0c5beeda83cfbd666c5c7 Mon Sep 17 00:00:00 2001
From: Script Raccoon <scriptraccoon@gmail.com>
Date: Fri, 26 Jun 2026 11:58:34 +0200
Subject: [PATCH] add two trivial functors

---
 .../catdat/data/functors/trivial_groups.yaml  | 27 +++++++++++++++++
 .../catdat/data/functors/trivial_sets.yaml    | 30 +++++++++++++++++++
 2 files changed, 57 insertions(+)
 create mode 100644 databases/catdat/data/functors/trivial_groups.yaml
 create mode 100644 databases/catdat/data/functors/trivial_sets.yaml

diff --git a/databases/catdat/data/functors/trivial_groups.yaml b/databases/catdat/data/functors/trivial_groups.yaml
new file mode 100644
index 00000000..302d2b0e
--- /dev/null
+++ b/databases/catdat/data/functors/trivial_groups.yaml
@@ -0,0 +1,27 @@
+id: trivial_groups
+name: trivial functor from the category of groups
+notation: $!$
+source: Grp
+target: '1'
+description: 'Every category $\C$ has a unique functor $! : \C \to 1$ into the trivial category. Here, we specify that $\C$ is the category of groups. It is a basic example of a full functor which is not faithful.'
+nlab_link: null
+
+tags:
+  - algebra
+
+related_functors:
+  - trivial_sets
+
+satisfied_properties:
+  - property: coreflector
+    proof: 'The constant functor $1 \to \Grp$ with value the trivial group is a left adjoint of $! : \Grp \to 1$ and fully faithful; this is because the trivial group is an initial object of $\Grp$.'
+
+  - property: reflector
+    proof: 'The constant functor $1 \to \Grp$ with value the trivial group is a left adjoint of $! : \Grp \to 1$ and fully faithful; this is because $\{\ast\}$ is a terminal object of $\Grp$.'
+
+  - property: full
+    proof: This follows easily from the fact that <a href="/category/Grp">$\Grp$</a> is strongly connected.
+
+unsatisfied_properties:
+  - property: essentially injective
+    proof: This is trivial.
diff --git a/databases/catdat/data/functors/trivial_sets.yaml b/databases/catdat/data/functors/trivial_sets.yaml
new file mode 100644
index 00000000..31d03551
--- /dev/null
+++ b/databases/catdat/data/functors/trivial_sets.yaml
@@ -0,0 +1,30 @@
+id: trivial_sets
+name: trivial functor from the category of sets
+notation: $!$
+source: Set
+target: '1'
+description: 'Every category $\C$ has a unique functor $! : \C \to 1$ into the trivial category. Here, we specify that $\C$ is the category of sets.'
+nlab_link: null
+
+tags:
+  - set theory
+
+related_functors:
+  - trivial_groups
+
+satisfied_properties:
+  - property: coreflector
+    proof: 'The constant functor $1 \to \Set$ with value $\varnothing$ is a left adjoint of $! : \Set \to 1$ and fully faithful; this is because $\varnothing$ is an initial object of $\Set$.'
+
+  - property: reflector
+    proof: 'The constant functor $1 \to \Set$ with value $\{\ast\}$ is a left adjoint of $! : \Set \to 1$ and fully faithful; this is because $\{\ast\}$ is a terminal object of $\Set$.'
+
+unsatisfied_properties:
+  - property: faithful
+    proof: 'Take any pair of distinct maps of sets $f,g : X \rightrightarrows Y$. They have the same image under the functor.'
+
+  - property: full
+    proof: If $X$ is a non-empty set, there is a (unique) morphism ${!}(X) \to {!}(\varnothing)$, but no morphism $X \to \varnothing$.
+
+  - property: essentially injective
+    proof: This is trivial.