Skip to content

Commit 70d5fa9

Browse files
committed
remove redundant assignments to the walking pair
1 parent dcb4a33 commit 70d5fa9

1 file changed

Lines changed: 0 additions & 12 deletions

File tree

databases/catdat/data/003_category-property-assignments/walking_pair.sql

Lines changed: 0 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -59,18 +59,6 @@ VALUES
5959
FALSE,
6060
'$0$ is not initial since it has two morphisms to $1$, and $1$ has not initial since it has no morphism to $0$.'
6161
),
62-
(
63-
'walking_pair',
64-
'binary products',
65-
FALSE,
66-
'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.'
67-
),
68-
(
69-
'walking_pair',
70-
'equalizers',
71-
FALSE,
72-
'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$.'
73-
),
7462
(
7563
'walking_pair',
7664
'pullbacks',

0 commit comments

Comments
 (0)