Groupoids with multi-terminal objects are thin

Author: ykawase5048

database/data/005_implications/006_trivial-categories-implications.sql

@@ -34,6 +34,13 @@ VALUES
 	'This is trivial.',
 	FALSE
 ),
+(
+	'groupoid_with_multi-terminal',
+	'["groupoid", "multi-terminal object"]',
+	'["thin"]',
+	'Let $f,g\colon A \rightrightarrows B$ be a parallel pair of morphisms. Since the category has a multi-terminal object, the connected component contains $A$ and $B$ has a terminal object. But since the category is a groupoid, both $A$ and $B$ are terminal objects in the connected component, hence $f=g$.',
+	FALSE
+),
 (
 	'trivial_consequence',
 	'["trivial"]',