remove redundant implications

Author: ScriptRaccoon

database/data/005_implications/001_limits-colimits-existence-implications.sql

@@ -76,20 +76,6 @@ VALUES
 	'If $1$ is a terminal object, then $X \times_1 Y = X \times Y$.',
 	FALSE
 ),
-(
-	'terminal_consequence',
-	'["terminal object"]',
-	'["connected"]',
-	'If $1$ denotes the terminal object, then for any two objects $A,B$ we have the zig-zag $A \rightarrow 1 \leftarrow B$.',
-	FALSE
-),
-(
-	'binary_products_consequence',
-	'["binary products", "inhabited"]',
-	'["connected"]',
-	'For any two objects $A,B$ we have the zig-zag $A \leftarrow A \times B \rightarrow B$.',
-	FALSE
-),
 (
 	'countable_products_consequence',
 	'["countable products"]',

database/data/005_implications/004_morphism-behavior-implications.sql

@@ -55,34 +55,6 @@ VALUES
 	'This is trivial.',
 	FALSE
 ),
-(
-	'groupoid_thin',
-	'["groupoid", "equalizers"]',
-	'["thin"]',
-	'The equalizer of any parallel pair $f,g$ must be an isomorphism, so $f=g$.',
-	FALSE
-),
-(
-	'groupoid_products',
-	'["groupoid", "binary products", "inhabited"]',
-	'["trivial"]',
-	'Let $\mathcal{C}$ be an inhabited groupoid with binary products. Then it is connected, so we may assume $\mathcal{C}=BG$ for a group $G$ with unique object $*$. But then $* \times * = *$, so there are $p,q \in G$ such that $G \to G \times G$, $x \mapsto (px,qx)$ is bijective. From here it is an easy exercise to deduce $G=1$.',
-	FALSE
-),
-(
-	'groupoid_initial',
-	'["groupoid", "initial object"]',
-	'["trivial"]',
-	'This is easy.',
-	FALSE
-),
-(
-	'groupoid_zero',
-	'["groupoid", "zero morphisms", "inhabited"]',
-	'["trivial"]',
-	'This is easy.',
-	FALSE
-),
 (
 	'groupoid_connected',
 	'["groupoid", "connected"]',

database/data/005_implications/008_topos-theory-implications.sql

@@ -41,13 +41,6 @@ VALUES
 	'If a morphism $X \to Y$ exists, we get a morphism $1 \to [X,Y]$, which forces $[X,Y]$ to be a terminal object by assumption. But then any two morphisms $1 \rightrightarrows [X,Y]$ are equal, so that any two morphisms $X \rightrightarrows Y$ are equal.',
 	FALSE
 ),
-(
-	'pointed_ccc_trivial',
-	'["pointed", "cartesian closed"]',
-	'["trivial"]',
-	'We have $X \cong X \times 1 \cong X \times 0 \cong 0$ for every object $X$.',
-	FALSE
-),
 (
 	'topos_definition',
 	'["elementary topos"]',
@@ -69,13 +62,6 @@ VALUES
 	'The universal property of $\top : 0 \to \Omega$ precisely says that every monomorphism $A \to B$ is the kernel of a unique morphism $B \to \Omega$, so it is normal.',
 	FALSE
 ),
-(
-	'subobject_classifier_collapse',
-	'["subobject classifier", "strict terminal object"]',
-	'["trivial"]',
-	'Since $1 \to \Omega$ is an isomorphism, every monomorphism must be an isomorphism. Applying this to the equalizer of a pair of morphisms, we see that the category is thin. But in a thin category, every morphism is a monomorphism. So every object $X$ has a unique isomorphism $X \to 1$.',
-	FALSE
-),
 (
 	'additive_trivial_condition',
 	'["regular subobject classifier", "additive"]',