my forest
1\import{dt-macros}
2\author{liamoc}
3\title{Commutative diagrams}
4\p{When working in a [category](dm-000G), we can state many theorems compactly using \em{commutative diagrams}, such as this diagram for products:
5\figure{
6\tex{\usepackage{tikz-cd}}{
7 \begin{tikzcd}[row sep=large]
8 & A \arrow[dl, "f",labels=above left]\arrow[dr,"g"]\arrow[d,"{\langle f, g \rangle}", dashed, labels=description] & \\
9 B & B \times C \ar[l, "{\pi_0}",labels=below] \ar[r, "{\pi_1}",labels=below]& C
10 \end{tikzcd}
11 }
12}
13 In these diagrams, the objects are \em{vertices} in the diagram, and the morphisms are the \em{arrows} in the diagram (we typically omit identity morphisms and morphisms that are just compositions of other morphisms). Looking at the above diagram, we can equate the two paths from #{A} to #{B} and the two paths from #{A} to #{C}, and produce the equations #{\pi_0 \circ \langle f, g \rangle = f} and #{\pi_1 \circ \langle f, g \rangle = g}. We adopt the convention that dotted lines indicate uniqueness, meaning that, from the diagram above, we can also infer the law: ##{\pi_0 \circ h = f \land \pi_1 \circ h = g \implies h = \langle f , g \rangle}
14}