diff --git a/databases/catdat/data/002_category-properties/004_morphism-behavior.sql b/databases/catdat/data/002_category-properties/004_morphism-behavior.sql
index 03660b87..6d45ea10 100644
--- a/databases/catdat/data/002_category-properties/004_morphism-behavior.sql
+++ b/databases/catdat/data/002_category-properties/004_morphism-behavior.sql
@@ -142,4 +142,20 @@ VALUES
 	'https://ncatlab.org/nlab/show/gaunt+category',
 	'gaunt',
 	FALSE
+),
+(
+	'subobject-trivial',
+	'is',
+	'A category is <i>subobject-trivial</i> if every monomorphism is an isomorphism. Equivalently, the poset of subobjects of any object is trivial. This is no standard terminology. We have added it to the database since it clarifies the relationship between several related properties.',
+	NULL,
+	'quotient-trivial',
+	TRUE
+),
+(
+	'quotient-trivial',
+	'is',
+	'A category is <i>quotient-trivial</i> if every epimorphism is an isomorphism. Equivalently, the poset of quotients of any object is trivial. This is no standard terminology. We have added it to the database since it clarifies the relationship between several related properties.',
+	NULL,
+	'subobject-trivial',
+	TRUE
 );
diff --git a/databases/catdat/data/002_category-properties/100_related-category-properties.sql b/databases/catdat/data/002_category-properties/100_related-category-properties.sql
index c1ac9d71..c609e74e 100644
--- a/databases/catdat/data/002_category-properties/100_related-category-properties.sql
+++ b/databases/catdat/data/002_category-properties/100_related-category-properties.sql
@@ -231,6 +231,8 @@ VALUES
 ('right cancellative', 'groupoid'),
 ('groupoid', 'left cancellative'),
 ('groupoid', 'right cancellative'),
+('groupoid', 'subobject-trivial'),
+('groupoid', 'quotient-trivial'),
 ('wide pullbacks', 'pullbacks'),
 ('wide pushouts', 'pushouts'),
 ('split abelian', 'abelian'),
@@ -339,7 +341,9 @@ VALUES
 ('cofiltered', 'finitely complete'),
 ('cofiltered', 'cofiltered limits'),
 ('mono-regular', 'normal'),
+('mono-regular', 'subobject-trivial'),
 ('epi-regular', 'conormal'),
+('epi-regular', 'quotient-trivial'),
 ('normal', 'zero morphisms'),
 ('normal', 'mono-regular'),
 ('normal', 'kernels'),
@@ -403,4 +407,8 @@ VALUES
 ('CSP', 'zero morphisms'),
 ('CSP', 'unital'),
 ('CSP', 'cofiltered-limit-stable epimorphisms'),
-('finitary algebraic', 'locally strongly finitely presentable');
+('finitary algebraic', 'locally strongly finitely presentable'),
+('subobject-trivial', 'mono-regular'),
+('subobject-trivial', 'groupoid'),
+('quotient-trivial', 'epi-regular'),
+('quotient-trivial', 'groupoid');
diff --git a/databases/catdat/data/003_category-property-assignments/FI.sql b/databases/catdat/data/003_category-property-assignments/FI.sql
index 4a031008..7c34cd27 100644
--- a/databases/catdat/data/003_category-property-assignments/FI.sql
+++ b/databases/catdat/data/003_category-property-assignments/FI.sql
@@ -53,12 +53,6 @@ VALUES
 	TRUE,
 	'If $f : X \to Y$ is an injective map of finite sets, it is the equalizer of the two injective maps $i_1,i_2 : Y \rightrightarrows Y \sqcup_X Y$, and $Y \sqcup_X Y$ is finite.'
 ),
-(
-	'FI',
-	'epi-regular',
-	TRUE,
-	'This is because every epimorphism is actually an isomorphism (see below).'
-),
 (
 	'FI',
 	'semi-strongly connected',
@@ -71,12 +65,6 @@ VALUES
 	TRUE,
 	'IF $X$ is a finite set, the slice category $\mathbf{FI} / X$ is equivalent to the poset of subsets of $X$. This is cartesian closed because $A \cap B \subseteq C$ holds if and only if $B \subseteq (X \setminus A) \cup C$, where $A,B,C \subseteq X$.'
 ),
-(
-	'FI',
-	'cofiltered-limit-stable epimorphisms',
-	TRUE,
-	'This is because every epimorphism is an isomorphism in this category (see below), and isomorphisms are always stable under any type of limit.'
-),
 (
 	'FI',
 	'small',
diff --git a/databases/catdat/data/003_category-property-assignments/FS.sql b/databases/catdat/data/003_category-property-assignments/FS.sql
index bb030e59..5c664d80 100644
--- a/databases/catdat/data/003_category-property-assignments/FS.sql
+++ b/databases/catdat/data/003_category-property-assignments/FS.sql
@@ -41,24 +41,12 @@ VALUES
 	TRUE,
 	'We construct coequalizers as in $\mathbf{FinSet}$ (or $\mathbf{Set}$) and observe that the universal property still holds when we restrict to surjective maps.'
 ),
-(
-	'FS',
-	'mono-regular',
-	TRUE,
-	'Every monomorphism is an isomorphism (see below), hence regular.'
-),
 (
 	'FS',
 	'epi-regular',
 	TRUE,
 	'If $f : X \to Y$ is a surjective map of finite sets, it is the coequalizer of the two projections $p_1, p_2 : X \times_Y X \rightrightarrows X$ in $\mathbf{FinSet}$, but also in $\mathbf{FS}$. Notice that $p_1,p_2$ are surjective. Even though $X \times_Y X$ is not a pullback in $\mathbf{FS}$, we can use this finite set here.'
 ),
-(
-	'FS',
-	'filtered-colimit-stable monomorphisms',
-	TRUE,
-	'This is because every monomorphism is an isomorphism in this category (see below), and isomorphisms are always stable under any type of colimit.'
-),
 (
 	'FS',
 	'multi-terminal object',
diff --git a/databases/catdat/data/003_category-property-assignments/walking_idempotent.sql b/databases/catdat/data/003_category-property-assignments/walking_idempotent.sql
index 6d0c016b..5b82c62f 100644
--- a/databases/catdat/data/003_category-property-assignments/walking_idempotent.sql
+++ b/databases/catdat/data/003_category-property-assignments/walking_idempotent.sql
@@ -37,7 +37,7 @@ VALUES
 ),
 (
 	'walking_idempotent',
-	'mono-regular',
+	'subobject-trivial',
     TRUE,
 	'This is because the identity is the only monomorphism.'
 ),
diff --git a/databases/catdat/data/003_category-property-assignments/walking_pair.sql b/databases/catdat/data/003_category-property-assignments/walking_pair.sql
index 08e119aa..cc16f476 100644
--- a/databases/catdat/data/003_category-property-assignments/walking_pair.sql
+++ b/databases/catdat/data/003_category-property-assignments/walking_pair.sql
@@ -59,18 +59,6 @@ VALUES
 	FALSE,
 	'$0$ is not initial since it has two morphisms to $1$, and $1$ has not initial since it has no morphism to $0$.'
 ),
-(
-	'walking_pair',
-	'binary products',
-	FALSE,
-	'We cannot have $0 \times 1 = 1$ since there is no morphism $1 \to 0$. So assume $0 \times 1 = 0$, say with projections $\mathrm{id}_0 : 0 \to 0$ and $a : 0 \to 1$. By applying the universal property to  $\mathrm{id}_0 : 0 \to 0$ and the other morphism $b : 0 \to 1$, it immediately follows $a=b$, which is a contradiction.'
-),
-(
-	'walking_pair',
-	'equalizers',
-	FALSE,
-	'The two morphisms $a,b : 0 \rightrightarrows 1$ have no equalizer, since it would have to be the identity of $0$, but $a \neq b$.'
-),
 (
 	'walking_pair',
 	'pullbacks',
diff --git a/databases/catdat/data/004_category-implications/004_morphism-behavior-implications.sql b/databases/catdat/data/004_category-implications/004_morphism-behavior-implications.sql
index d54a854e..7d675061 100644
--- a/databases/catdat/data/004_category-implications/004_morphism-behavior-implications.sql
+++ b/databases/catdat/data/004_category-implications/004_morphism-behavior-implications.sql
@@ -41,6 +41,13 @@ VALUES
 	'Any parallel pair of morphisms with a common section (or retraction) must be a pair of equal isomorphisms.',
 	FALSE
 ),
+(
+	'reflexive_pair_trivial_2',
+	'["subobject-trivial"]',
+	'["reflexive coequalizers", "coreflexive equalizers"]',
+	'Any parallel pair of morphisms with a common section (or retraction) must be a pair of equal isomorphisms.',
+	FALSE
+),
 (
 	'groupoid_consequence',
 	'["groupoid"]',
@@ -168,6 +175,13 @@ VALUES
 	'This is trivial.',
 	FALSE
 ),
+(
+	'filtered_monos_iso',
+	'["subobject-trivial", "filtered colimits"]',
+	'["filtered-colimit-stable monomorphisms"]',
+	'This is trivial.',
+	FALSE
+),
 (
 	'thin_groupoids',
 	'["groupoid", "core-thin"]',
@@ -188,4 +202,32 @@ VALUES
 	'["skeletal", "core-thin"]',
 	'This is trivial.',
 	TRUE
+),
+(
+	'thin_subobject-trivial',
+	'["subobject-trivial", "equalizers"]',
+	'["thin"]',
+	'If $f,g : X \rightrightarrows Y$ are morphisms, their equalizer is a monomorphism $E \hookrightarrow X$, hence an isomorphism. But this means $f = g$.',
+	FALSE
+),
+(
+	'subobject-trivial_consequence',
+	'["subobject-trivial"]',
+	'["mono-regular"]',
+	'This is trivial.',
+	FALSE
+),
+(
+	'subobject-trivial_groupoids',
+	'["groupoid"]',
+	'["subobject-trivial"]',
+	'This is trivial.',
+	FALSE
+),
+(
+	'subobject-trivial_criterion',
+	'["right cancellative", "epi-regular"]',
+	'["subobject-trivial"]',
+	'This is because a monomorphism which is also a regular epimorphism is an isomorphism.',
+	FALSE
 );
\ No newline at end of file
diff --git a/databases/catdat/scripts/expected-data/Ab.json b/databases/catdat/scripts/expected-data/Ab.json
index b511fc1b..409d8281 100644
--- a/databases/catdat/scripts/expected-data/Ab.json
+++ b/databases/catdat/scripts/expected-data/Ab.json
@@ -153,5 +153,7 @@
 	"cofiltered-limit-stable epimorphisms": false,
 	"exact cofiltered limits": false,
 	"gaunt": false,
-	"core-thin": false
+	"core-thin": false,
+	"subobject-trivial": false,
+	"quotient-trivial": false
 }
diff --git a/databases/catdat/scripts/expected-data/Set.json b/databases/catdat/scripts/expected-data/Set.json
index 44db92c4..7fe66a78 100644
--- a/databases/catdat/scripts/expected-data/Set.json
+++ b/databases/catdat/scripts/expected-data/Set.json
@@ -153,5 +153,7 @@
 	"cofiltered-limit-stable epimorphisms": false,
 	"exact cofiltered limits": false,
 	"gaunt": false,
-	"core-thin": false
+	"core-thin": false,
+	"subobject-trivial": false,
+	"quotient-trivial": false
 }
diff --git a/databases/catdat/scripts/expected-data/Top.json b/databases/catdat/scripts/expected-data/Top.json
index e70a439c..6806592d 100644
--- a/databases/catdat/scripts/expected-data/Top.json
+++ b/databases/catdat/scripts/expected-data/Top.json
@@ -153,5 +153,7 @@
 	"cofiltered-limit-stable epimorphisms": false,
 	"exact cofiltered limits": false,
 	"gaunt": false,
-	"core-thin": false
+	"core-thin": false,
+	"subobject-trivial": false,
+	"quotient-trivial": false
 }