From 33c4bbf385000dd850f825fc69935f48d169f11b Mon Sep 17 00:00:00 2001
From: Script Raccoon <scriptraccoon@gmail.com>
Date: Sat, 27 Jun 2026 02:30:16 +0200
Subject: [PATCH 1/2] explain dual properties

---
 content/dual-properties.md    | 22 ++++++++++++++++++++++
 src/pages/PropertyPage.svelte |  2 +-
 2 files changed, 23 insertions(+), 1 deletion(-)
 create mode 100644 content/dual-properties.md

diff --git a/content/dual-properties.md b/content/dual-properties.md
new file mode 100644
index 00000000..5c2d8517
--- /dev/null
+++ b/content/dual-properties.md
@@ -0,0 +1,22 @@
+---
+title: Dual properties
+description: A short explanation of what we mean by dual properties in CatDat.
+---
+
+## Dual properties
+
+### Categories
+
+Given a property $P$ of categories, its dual property $P^{\op}$ is defined as follows: a category $\C$ satisfies $P^{\op}$ if and only if its dual category $\C^{\op}$ satisfies $P$.
+
+For example, since a category has an [initial object](/category-property/initial_object) if and only if its dual category has a [terminal object](/category-property/terminal_object), the property "has an initial object" is dual to the property "has a terminal object". In practice, dual properties can be obtained by reversing all arrows.
+
+Notice that $(P^{\op})^{\op} = P$, and that $\C$ satisfies $P$ if and only if $\C^{\op}$ satisfies $P^{\op}$.
+
+### Functors
+
+Given a property $P$ of functors, its dual property $P^{\op}$ is defined as follows: a functor $F : \C \to \D$ satisfies $P^{\op}$ if and only if its dual functor $F^{\op} : \C^{\op} \to \D^{\op}$ satisfies $P$. Notice that taking the dual does not reverse the direction of the functor.
+
+For example, since a functor is [essentially injective](/functor-property/essentially_injective) if and only if its dual is essentially injective, the property "is essentially injective" is self-dual. In particular, it is _not_ dual to the property "is [essentially surjective](/functor-property/essentially_surjective)", which is itself also self-dual.
+
+Again, notice that $(P^{\op})^{\op} = P$, and that $F : \C \to \D$ satisfies $P$ if and only if $F^{\op} : \C^{\op} \to \D^{\op}$ satisfies $P^{\op}$.
diff --git a/src/pages/PropertyPage.svelte b/src/pages/PropertyPage.svelte
index 3272561a..91b8a2d3 100644
--- a/src/pages/PropertyPage.svelte
+++ b/src/pages/PropertyPage.svelte
@@ -55,7 +55,7 @@
 	<ul class="with-margins">
 		{#if property.dual_property_id}
 			<li>
-				<strong>Dual property:</strong>
+				<strong><a href="/content/dual-properties">Dual property:</a></strong>
 				<a href={get_property_url(property.dual_property_id, type)}
 					>{property.dual_property_id}</a
 				>

From 3fa3a3ef2bdd0f338aa6d8fd3a4d82e83a720ace Mon Sep 17 00:00:00 2001
From: Script Raccoon <scriptraccoon@gmail.com>
Date: Sat, 27 Jun 2026 02:32:40 +0200
Subject: [PATCH 2/2] remove redundant explanation for left/right invertible
 functors

---
 databases/catdat/data/functor-properties/left-invertible.yaml  | 2 +-
 databases/catdat/data/functor-properties/right-invertible.yaml | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/databases/catdat/data/functor-properties/left-invertible.yaml b/databases/catdat/data/functor-properties/left-invertible.yaml
index 82282809..95fa1ddb 100644
--- a/databases/catdat/data/functor-properties/left-invertible.yaml
+++ b/databases/catdat/data/functor-properties/left-invertible.yaml
@@ -1,6 +1,6 @@
 id: left-invertible
 relation: is
-description: 'A <i>left inverse</i> of a functor $F : \C \to \D$ is a functor $G : \D \to \C$ satisfying $G \circ F \cong \id_{\C}$. We do not require $G \circ F = \id_{\C}$ here, which is often too strict. A functor is called <i>left-invertible</i> when it has a left inverse. This notion is self-dual in the sense that $F : \C \to \D$ is left-invertible iff $F^{\op} : \C^{\op} \to \D^{\op}$ is left-invertible.'
+description: 'A <i>left inverse</i> of a functor $F : \C \to \D$ is a functor $G : \D \to \C$ satisfying $G \circ F \cong \id_{\C}$. We do not require $G \circ F = \id_{\C}$ here, which is often too strict. A functor is called <i>left-invertible</i> when it has a left inverse.'
 nlab_link: https://ncatlab.org/nlab/show/inverse+functor
 invariant_under_equivalences: true
 dual_property: left-invertible
diff --git a/databases/catdat/data/functor-properties/right-invertible.yaml b/databases/catdat/data/functor-properties/right-invertible.yaml
index b5a8c90e..d0883f87 100644
--- a/databases/catdat/data/functor-properties/right-invertible.yaml
+++ b/databases/catdat/data/functor-properties/right-invertible.yaml
@@ -1,6 +1,6 @@
 id: right-invertible
 relation: is
-description: 'A <i>right inverse</i> of a functor $F : \C \to \D$ is a functor $G : \D \to \C$ satisfying $F \circ G \cong \id_{\D}$. We do not require $F \circ G = \id_{\D}$ here, which is often too strict. A functor is called <i>right-invertible</i> when it has a right inverse. This notion is self-dual in the sense that $F : \C \to \D$ is right-invertible iff $F^{\op} : \C^{\op} \to \D^{\op}$ is right-invertible.'
+description: 'A <i>right inverse</i> of a functor $F : \C \to \D$ is a functor $G : \D \to \C$ satisfying $F \circ G \cong \id_{\D}$. We do not require $F \circ G = \id_{\D}$ here, which is often too strict. A functor is called <i>right-invertible</i> when it has a right inverse.'
 nlab_link: https://ncatlab.org/nlab/show/inverse+functor
 invariant_under_equivalences: true
 dual_property: right-invertible