my forest
more dt
+336
+4
trees/dm-000G.tree
+4
trees/dm-000G.tree
···
1
+
\taxon{Definition}
2
+
\title{Category}
3
+
\author{liamoc}
4
+
\p{A \em{category} #{C}consists of a collection of things (\em{objects}) and a collection of arrows between these things (\em{morphisms}). If there is a morphism #{A \xrightarrow{f} B} and a morphism #{B \xrightarrow{g} C}, we also have the composed morphism #{A \xrightarrow{g \circ f} C}. This composition operator must be [associative](dm-000F). Additionally each object #{X} has an \em{identity} morphism #{X \xrightarrow{\mathsf{id}_X} X}, such that for an arrow #{X \xrightarrow{a} Y}, #{a \circ \mathsf{id}_X = \mathsf{id}_Y \circ a = a}. }
+6
trees/dm-000H.tree
+6
trees/dm-000H.tree
···
1
+
\title{The [category](dm-000G) #{\mathbf{Set}}}
2
+
\author{liamoc}
3
+
\taxon{Example}
4
+
\p{
5
+
The [category](dm-000G) #{\mathbf{Set}} is the [category](dm-000G) where the objects are (small) \em{sets}, the morphisms are functions between these sets, composition is function composition (#{(g \circ f)(x) \triangleq g(f(x))}) and identity is just the identity function #{\lambda x. x}.
6
+
}
+6
trees/dm-000I.tree
+6
trees/dm-000I.tree
···
1
+
\title{The [category](dm-000G) #{\mathbf{Rel}}}
2
+
\author{liamoc}
3
+
\taxon{Example}
4
+
\p{
5
+
The [category](dm-000G) #{\mathbf{Rel}} is the [category](dm-000G) where the objects are (small) \em{sets}, the morphisms are \em{relations} between these sets, composition is relational composition: ##{g \circ f \triangleq \{ (a,b) \mid \exists i.\ (a,i) \in f \land (i,b) \in g \}} and identity is the diagonal relation (equality).
6
+
}
+11
trees/dm-000J.tree
+11
trees/dm-000J.tree
···
1
+
\title{Functor}
2
+
\author{liamoc}
3
+
\taxon{Definition}
4
+
\p{
5
+
A \em{functor} #{F} from a [category](dm-000G) #{\mathbf{C}} to a [category](dm-000G) #{\mathbf{D}} consists of an \em{object mapping} that maps objects of #{\mathbf{C}} to objects of #{\mathbf{D}}, and a \em{morphism mapping} that maps morphisms of #{\mathbf{C}} to morphisms of #{\mathbf{D}} such that:
6
+
\ul{
7
+
\li{For each #{A \xrightarrow{m} B} in #{\mathbf{C}}, we have a morphism #{F(A) \xrightarrow{F(m)} F(B)} in #{\mathbf{D}}.}
8
+
\li{ For each object #{A} in #{\mathbf{C}}, the equation #{F(\mathsf{id}_A) = \mathsf{id}_{F(A)}} holds in #{\mathbf{D}}. }
9
+
\li{ For a pair of morphism #{A \xrightarrow{f} B \xrightarrow{g} C} in #{\mathbf{C}}, the equation #{F (g \circ f) = F(g) \circ F(f)} holds in #{\mathbf{D}}. }
10
+
}
11
+
}
+6
trees/dm-000K.tree
+6
trees/dm-000K.tree
···
1
+
\title{The [category](dm-000G) #{\mathbf{Cat}}}
2
+
\author{liamoc}
3
+
\taxon{Example}
4
+
\p{
5
+
The [category](dm-000G) #{\mathbf{Cat}} is the [category](dm-000G) where the objects are themselves (small) [categories](dm-000G), the morphisms are structure-preserving maps between these categories, i.e., [functors](dm-000J).
6
+
}
+14
trees/dm-000L.tree
+14
trees/dm-000L.tree
···
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
+
}
+10
trees/dt-001Z.tree
+10
trees/dt-001Z.tree
···
19
19
\transclude{dt-0022}
20
20
\transclude{dt-0023}
21
21
\transclude{dt-0024}
22
+
\p{These building blocks can be used to make many functions on [products](dt-0021) (thereby ensuring [continuity](dt-001J)):
22
23
}
24
+
\transclude{dt-0025}
25
+
\transclude{dt-0026}
26
+
\transclude{dt-0027}
27
+
\transclude{dt-0028}
28
+
\transclude{dt-0029}
29
+
\transclude{dt-002A}
30
+
\transclude{dt-002C}
31
+
}
32
+
23
33
24
34
+42
trees/dt-0025.tree
+42
trees/dt-0025.tree
···
1
+
\import{dt-macros}
2
+
\import{table-macros}
3
+
\taxon{Definition}
4
+
\author{liamoc}
5
+
\title{The #{\mathit{swap}} function}
6
+
\table{
7
+
\tr{
8
+
\td{\tex{\usepackage{string-diagrams}}{\begin{tikzpicture}
9
+
\node[box, box ports west = 2, box ports east = 2, minimum width=3cm, minimum height=3cm] (ZZ) at (-9cm,0) {};
10
+
\draw[thick] (ZZ.west.1) -- (ZZ.east.2);
11
+
\draw[thick] (ZZ.west.2) -- (ZZ.east.1);
12
+
\node[dot] at (ZZ.east.1) {};
13
+
\node[dot] at (ZZ.east.2) {};
14
+
\node[dot] at (ZZ.west.1) {};
15
+
\node[dot] at (ZZ.west.2) {};
16
+
\node at (-6.3cm,0) {\Large $=$};
17
+
\end{tikzpicture} }
18
+
\td{
19
+
\tex{\usepackage{string-diagrams}}{
20
+
\begin{tikzpicture}
21
+
\node[box, box ports west = 1, box ports east = 2, minimum width=3cm, minimum height=3cm] (A) {};
22
+
\node[dot] (ae) at ([yshift=-0.2cm]A.east.1) {};
23
+
\node[dot] (ae2) at ([yshift=0.2cm]A.east.2) {};
24
+
\node[dot] (aw) at ([yshift=0.15cm]A.west.1) {};
25
+
\node[dot] (aw2) at ([yshift=-0.15cm]A.west.1) {};
26
+
\node[dot] (X) at ([xshift=1cm,yshift=0.15cm]A.west.1) {};
27
+
\node[dot] (Y) at ([xshift=0.7cm,yshift=-0.15cm]A.west.1) {};
28
+
\node[box,thick, box ports west=2, box ports east=2] (f) at ([xshift=-1cm]A.east.1) {};
29
+
\node[box,thick, box ports west=2, box ports east=2] (g) at ([xshift=-1cm]A.east.2) {};
30
+
\wires[thick]{
31
+
f = { west.1 = X.north, west.2 = Y.north, east.2=ae.west},
32
+
g = { west.1 = X.south, west.2 = Y.south, east.1=ae2.west},
33
+
X = { west = aw.east },
34
+
Y = { west = aw2.east },
35
+
}{};
36
+
\draw[thick] (f.west.2) -- (f.east.2);
37
+
\draw[thick,-|] (f.west.1) -- ([xshift=0.4cm]f.west.1);
38
+
\draw[thick] (g.west.1) -- (g.east.1);
39
+
\draw[thick,-|] (g.west.2) -- ([xshift=0.4cm]g.west.2);
40
+
\end{tikzpicture}}}
41
+
}\td{#{\begin{array}{l}\mathit{swap} : A \times B \rightarrow B \times A \\ \mathit{swap} = \langle \pi_1 , \pi_0 \rangle \end{array}}}
42
+
}}
+53
trees/dt-0026.tree
+53
trees/dt-0026.tree
···
1
+
\import{dt-macros}
2
+
\import{table-macros}
3
+
\taxon{Definition}
4
+
\title{Product of functions}
5
+
\author{liamoc}
6
+
\p{Given #{f : A \rightarrow C} and #{g : B \rightarrow D}, we overload the #{\times} operator for [products](dm-0005) to denote the combined function #{f \times g : A \times B \rightarrow C \times D}, given below:}
7
+
\table{\tr{\td{
8
+
\tex{\usepackage{string-diagrams}}{
9
+
\begin{tikzpicture}
10
+
\node[box, box ports west = 2, box ports east = 2, minimum width=3cm, minimum height=3cm] (ZZ) at (-9cm,0) {};
11
+
\node[box,thick, box ports west=1, box ports east=1] (ff) at ([xshift=-1.5cm]ZZ.east.1) {f};
12
+
\node[box,thick, box ports west=1, box ports east=1] (gg) at ([xshift=-1.5cm]ZZ.east.2) {g};
13
+
14
+
\draw[thick] (ZZ.east.1) -- (ff.east.1);
15
+
\draw[thick] (ZZ.east.2) -- (gg.east.1);
16
+
\draw[thick] (ZZ.west.1) -- (ff.west.1);
17
+
\draw[thick] (ZZ.west.2) -- (gg.west.1);
18
+
\node[dot] at (ZZ.east.1) {};
19
+
\node[dot] at (ZZ.east.2) {};
20
+
\node[dot] at (ZZ.west.1) {};
21
+
\node[dot] at (ZZ.west.2) {};
22
+
\node at (-6.3cm,0) {\Large $=$};
23
+
\end{tikzpicture}
24
+
}}\td{
25
+
\tex{\usepackage{string-diagrams}}{
26
+
\begin{tikzpicture}
27
+
\node[box, box ports west = 1, box ports east = 2, minimum width=4cm, minimum height=3cm] (A) at (0.5cm,0) {};
28
+
\node[dot] (ae) at ([yshift=-0.0cm]A.east.1) {};
29
+
\node[dot] (ae2) at ([yshift=0.0cm]A.east.2) {};
30
+
\node[dot] (aw) at ([yshift=0.15cm]A.west.1) {};
31
+
\node[dot] (aw2) at ([yshift=-0.15cm]A.west.1) {};
32
+
\node[dot] (X) at ([xshift=1cm,yshift=0.15cm]A.west.1) {};
33
+
\node[dot] (Y) at ([xshift=0.7cm,yshift=-0.15cm]A.west.1) {};
34
+
\node[box,thick, box ports west=2, box ports east=2] (f) at ([xshift=-2cm]A.east.1) {};
35
+
\node[box,thick, box ports west=2, box ports east=2] (g) at ([xshift=-2cm]A.east.2) {};
36
+
\node[box,thick, box ports west=2, box ports east=1] (fff) at ([xshift=-0.75cm]A.east.1) {f};
37
+
\node[box,thick, box ports west=2, box ports east=1] (ggg) at ([xshift=-0.75cm]A.east.2) {g};
38
+
\wires[thick]{
39
+
f = { west.1 = X.north, west.2 = Y.north, east.1=fff.west.1},
40
+
g = { west.1 = X.south, west.2 = Y.south, east.2=ggg.west.2},
41
+
X = { west = aw.east },
42
+
Y = { west = aw2.east },
43
+
fff = { east = A.east.1 },
44
+
ggg = { east = A.east.2 },
45
+
}{};
46
+
\draw[thick] (f.west.1) -- (f.east.1);
47
+
\draw[thick,-|] (f.west.2) -- ([xshift=0.4cm]f.west.2);
48
+
\draw[thick] (g.west.2) -- (g.east.2);
49
+
\draw[thick,-|] (g.west.1) -- ([xshift=0.4cm]g.west.1);
50
+
\end{tikzpicture}
51
+
}}\td{
52
+
\p{##{\begin{array}{l} f \times g : A \times B \rightarrow C \times D \\ f \times g = \langle f \circ \pi_0 , g \circ \pi_1 \rangle \end{array}}}
53
+
}}}
+119
trees/dt-0027.tree
+119
trees/dt-0027.tree
···
1
+
\import{dt-macros}
2
+
\import{table-macros}
3
+
\title{Pictorial Properties}
4
+
\author{liamoc}
5
+
\p{The following properties of our [projection](dt-0020) and [split](dt-0023) functions follow from the pictorial reasoning we see on the right:}
6
+
\table{
7
+
\tr{\td{
8
+
##{\pi_0 \circ \langle f , g \rangle = f}}
9
+
\td{\tex{\usepackage{string-diagrams}}{
10
+
\begin{tikzpicture}
11
+
\node[box, box ports west = 1, box ports east = 1, minimum width=3cm, minimum height=3cm] (ZZ) at (6cm,8cm) {};
12
+
\node[box, box ports west = 1, box ports east = 2, minimum width=4cm, minimum height=3cm] (A) at (0.5cm,8cm) {};
13
+
\node[dot] (ae) at ([yshift=-0.25cm]A.east.1) {};
14
+
% \node[dot] (ae2) at ([yshift=0.25cm]A.east.2) {};
15
+
\node[dot] (aw) at ([yshift=0cm]A.west.1) {};
16
+
\node[dot] (aw2) at ([yshift=-0cm]A.west.1) {};
17
+
\node[dot] (X) at ([xshift=1cm]A.west.1) {};
18
+
\node[box,thick, box ports west=1, box ports east=1] (fff) at ([xshift=-2cm]A.east.1) { f };
19
+
\node[box,thick, box ports west=1, box ports east=1] (ggg) at ([xshift=-2cm]A.east.2) { g };
20
+
\node[box,thick, box ports west=2, box ports east=2, minimum height=2cm] (f) at ([xshift=3.25cm]A.west.1) {};
21
+
% \node[box,thick, box ports west=2, box ports east=2] (g) at ([xshift=-0.75cm]A.east.2) {};
22
+
\wires[thick]{
23
+
fff = { west.1 = X.north, east.1=f.west.1},
24
+
ggg = { west.1 = X.south }, %$ east.2=g.west.2},
25
+
X = { west = aw.east, north = fff.west.1, south = ggg.west.1 },
26
+
fff = { east.1 = f.west.1 },
27
+
ggg = { east.1 = f.west.2 },
28
+
f = { east.1 = ae.west },
29
+
% g = { east.2 = ae2.west },
30
+
}{};
31
+
\draw[thick] (f.west.1) -- (f.east.1);
32
+
\draw[thick,-|] (f.west.2) -- ([xshift=0.4cm]f.west.2);
33
+
% \draw[thick] (g.west.2) -- (g.east.2);
34
+
% \draw[thick,-|] (g.west.1) -- ([xshift=0.4cm]g.west.1);
35
+
36
+
\node[box,thick, box ports west=1, box ports east=1] (ff) at ([xshift=-1.5cm]ZZ.east.1) {f};
37
+
\node at (3.35cm,8cm) {\Large $=$};
38
+
\draw[thick] (ZZ.east.1) -- (ff.east);
39
+
\draw[thick] (ZZ.west.1) -- (ff.west.1);
40
+
\node[dot] at (ZZ.east.1) {};
41
+
\node[dot] at (ZZ.west.1) {};
42
+
\end{tikzpicture} }}}
43
+
\tr{\td{
44
+
##{\pi_1 \circ \langle f , g \rangle = g}}
45
+
\td{\tex{\usepackage{string-diagrams}}{
46
+
\begin{tikzpicture}
47
+
\node[box, box ports west = 1, box ports east = 1, minimum width=3cm, minimum height=3cm] (ZZ) at (6cm,4cm) {};
48
+
\node[box, box ports west = 1, box ports east = 2, minimum width=4cm, minimum height=3cm] (A) at (0.5cm,4cm) {};
49
+
% \node[dot] (ae) at ([yshift=-0.25cm]A.east.1) {};
50
+
\node[dot] (ae2) at ([yshift=0.25cm]A.east.2) {};
51
+
\node[dot] (aw) at ([yshift=0cm]A.west.1) {};
52
+
% \node[dot] (aw2) at ([yshift=-0cm]A.west.1) {};
53
+
\node[dot] (X) at ([xshift=1cm]A.west.1) {};
54
+
\node[box,thick, box ports west=1, box ports east=1] (fff) at ([xshift=-2cm]A.east.1) { f };
55
+
\node[box,thick, box ports west=1, box ports east=1] (ggg) at ([xshift=-2cm]A.east.2) { g };
56
+
\node[box,thick, box ports west=2, box ports east=2, minimum height=2cm] (f) at ([xshift=3.25cm]A.west.1) {};
57
+
% \node[box,thick, box ports west=2, box ports east=2] (g) at ([xshift=-0.75cm]A.east.2) {};
58
+
\wires[thick]{
59
+
fff = { west.1 = X.north, east.1=f.west.1},
60
+
ggg = { west.1 = X.south }, %$ east.2=g.west.2},
61
+
X = { west = aw.east, north = fff.west.1, south = ggg.west.1 },
62
+
fff = { east.1 = f.west.1 },
63
+
ggg = { east.1 = f.west.2 },
64
+
f = { east.2 = ae2.west },
65
+
% g = { east.2 = ae2.west },
66
+
}{};
67
+
\draw[thick] (f.west.2) -- (f.east.2);
68
+
\draw[thick,-|] (f.west.1) -- ([xshift=0.4cm]f.west.1);
69
+
% \draw[thick] (g.west.2) -- (g.east.2);
70
+
% \draw[thick,-|] (g.west.1) -- ([xshift=0.4cm]g.west.1);
71
+
72
+
\node[box,thick, box ports west=1, box ports east=1] (ff) at ([xshift=-1.5cm]ZZ.east.1) {g};
73
+
\node at (3.35cm,4cm) {\Large $=$};
74
+
\draw[thick] (ZZ.east.1) -- (ff.east);
75
+
\draw[thick] (ZZ.west.1) -- (ff.west.1);
76
+
\node[dot] at (ZZ.east.1) {};
77
+
\node[dot] at (ZZ.west.1) {};
78
+
\end{tikzpicture}}}}
79
+
\tr{\td{
80
+
##{\langle \pi_0 \circ h , \pi_1 \circ h \rangle = h}
81
+
}\td{
82
+
\tex{\usepackage{string-diagrams}}{
83
+
\begin{tikzpicture}
84
+
\node[box, box ports west = 1, box ports east = 1, minimum width=3cm, minimum height=3cm] (ZZ) at (6cm,0) {};
85
+
\node[box, box ports west = 1, box ports east = 2, minimum width=4cm, minimum height=3cm] (A) at (0.5cm,0) {};
86
+
\node[dot] (ae) at ([yshift=0.2cm]A.east.1) {};
87
+
\node[dot] (ae2) at ([yshift=-0.2cm]A.east.2) {};
88
+
\node[dot] (aw) at ([yshift=0cm]A.west.1) {};
89
+
\node[dot] (aw2) at ([yshift=-0cm]A.west.1) {};
90
+
\node[dot] (X) at ([xshift=1cm]A.west.1) {};
91
+
\node[box,thick, box ports west=1, box ports east=2] (fff) at ([xshift=-2cm]A.east.1) { h };
92
+
\node[box,thick, box ports west=1, box ports east=2] (ggg) at ([xshift=-2cm]A.east.2) { h };
93
+
\node[box,thick, box ports west=2, box ports east=2] (f) at ([xshift=-0.75cm]A.east.1) {};
94
+
\node[box,thick, box ports west=2, box ports east=2] (g) at ([xshift=-0.75cm]A.east.2) {};
95
+
\wires[thick]{
96
+
fff = { west.1 = X.north, east.1=f.west.1},
97
+
ggg = { west.1 = X.south, east.2=g.west.2},
98
+
X = { west = aw.east, north = fff.west.1, south = ggg.west.1 },
99
+
fff = { east.1 = f.west.1, east.2 = f.west.2 },
100
+
ggg = { east.1 = g.west.1, east.2 = g.west.2 },
101
+
f = { east.1 = ae.west },
102
+
g = { east.2 = ae2.west },
103
+
}{};
104
+
\draw[thick] (f.west.1) -- (f.east.1);
105
+
\draw[thick,-|] (f.west.2) -- ([xshift=0.4cm]f.west.2);
106
+
\draw[thick] (g.west.2) -- (g.east.2);
107
+
\draw[thick,-|] (g.west.1) -- ([xshift=0.4cm]g.west.1);
108
+
109
+
\node[box,thick, box ports west=1, box ports east=2] (ff) at ([xshift=-1.5cm]ZZ.east.1) {h};
110
+
\node at (3.35cm,0) {\Large $=$};
111
+
\draw[thick] ([yshift=0.2cm]ZZ.east.1) -- (ff.east.1);
112
+
\draw[thick] ([yshift=-0.2cm]ZZ.east.1) -- (ff.east.2);
113
+
\draw[thick] (ZZ.west.1) -- (ff.west.1);
114
+
\node[dot] at ([yshift=0.2cm]ZZ.east.1) {};
115
+
\node[dot] at ([yshift=-0.2cm]ZZ.east.1) {};
116
+
\node[dot] at (ZZ.west.1) {};
117
+
\end{tikzpicture}
118
+
}}}
119
+
}
+20
trees/dt-0028.tree
+20
trees/dt-0028.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\taxon{Exercise}
4
+
\p{Prove that the three properties in \ref{dt-0027} are equivalent to the [universal property for products](dt-0029)}
5
+
##{(\pi_0 \circ h = f \land \pi_1 \circ h = g)\ \text{iff}\ h = \langle f , g \rangle}
6
+
\scope{
7
+
\put\transclude/toc{false}
8
+
\put\transclude/numbered{false}
9
+
\put\transclude/expanded{false}
10
+
\subtree{
11
+
\taxon{Solution}
12
+
\p{ Showing in both directions:
13
+
\ol{
14
+
\li{ \em{The three properties follow from the universal property:}
15
+
The first two properties follow from the universal property where #{h} is set to #{\langle f , g \rangle}. The third property follows from the universal property where #{f} is set to #{\pi_0\circ h} and #{g} is set to #{\pi_1\circ h}.}
16
+
\li{\em{The universal property follows from the universal property:}
17
+
In the #{\Rightarrow} direction of the universal property follows from the third property, and the #{\Leftarrow} direction follows from the first two.
18
+
}}}
19
+
}
20
+
}
+14
trees/dt-0029.tree
+14
trees/dt-0029.tree
···
1
+
\import{dt-macros}
2
+
\taxon{Definition}
3
+
\author{liamoc}
4
+
\title{Universal property for [cpo products](dt-0021)}
5
+
##{ (\pi_0 \circ h = f \land \pi_1 \circ h = g)\ \text{iff}\ h = \langle f , g \rangle}
6
+
\p{As [commuting diagram](dm-000L) on the [category](dm-000G) #{\mathbf{Cpo}}:}
7
+
\figure{
8
+
\tex{\usepackage{tikz-cd}}{
9
+
\begin{tikzcd}[row sep=large]
10
+
& A \arrow[dl, "f",labels=above left]\arrow[dr,"g"]\arrow[d,"{\langle f, g \rangle}", dashed, labels=description] & \\
11
+
B & B \times C \ar[l, "{\pi_0}",labels=below] \ar[r, "{\pi_1}",labels=below]& C
12
+
\end{tikzcd}
13
+
}
14
+
}
+10
trees/dt-002A.tree
+10
trees/dt-002A.tree
+6
trees/dt-002B.tree
+6
trees/dt-002B.tree
···
1
+
\title{The [category](dm-000G) #{\mathbf{Cpo}}}
2
+
\author{liamoc}
3
+
\taxon{Example}
4
+
\p{
5
+
The [category](dm-000G) #{\mathbf{Cpo}} is the [category](dm-000G) where the objects are [cpos](dt-001D), the morphisms are [continuous functions](dt-001J) between these [cpos](dt-001D), composition is function composition (#{(g \circ f)(x) \triangleq g(f(x))}) and identity is just the identity function #{\lambda x. x}.
6
+
}
+15
trees/dt-002C.tree
+15
trees/dt-002C.tree
···
1
+
\title{Derived properties of [cpo products](dt-0021)}
2
+
\author{liamoc}
3
+
\p{
4
+
The [universal property](dt-0029) is called such because \em{all} the familiar properties of [products](dt-0021) follow from it – thinking in pictures helps to see how (Indeed, the [universal property](dt-0029) \em{characterises} products up to isomorphism):}
5
+
\ol{
6
+
\li{ #{\pi_0 \circ (f \times g) = f \circ \pi_0}}
7
+
\li{ #{\pi_1 \circ (f \times g) = g \circ \pi_1}}
8
+
\li{ #{(f \times g) \circ \langle h , i \rangle = \langle f \circ h, g \circ i \rangle}}
9
+
\li{ #{\langle f , g \rangle \circ h = \langle f \circ h, g \circ h \rangle}}
10
+
\li{ #{\mathsf{id}_A \times \mathsf{id}_B = \mathsf{id}_{A \times B} \quad (*)}}
11
+
\li{ #{(f \circ g) \times (h \circ i) = (f \circ h) \times (g \circ i) \quad (**)}}
12
+
}
13
+
\p{
14
+
These last two statements #{(*)} and #{(**)} show that #{\times} is a \em{bifunctor} on the [category #{\textbf{Cpo}}](dt-002B), i.e., a [functor](dm-000J) #{\textbf{Cpo} \times \textbf{Cpo} \rightarrow \textbf{Cpo}}.
15
+
}