my forest
minor tweaks
+6
-2
+5
-1
trees/dt/dt-0038.tree
+5
-1
trees/dt/dt-0038.tree
···
1
1
\import{dt-macros}
2
2
\author{liamoc}
3
3
\taxon{Theorem}
4
-
\p{#{+ : \mathbf{Cpo} \times \mathbf{Cpo} \rightarrow \mathbf{Cpo}} is a lawful [bifunctor](dm-000M).
4
+
\p{#{+ : \mathbf{Cpo} \times \mathbf{Cpo} \rightarrow \mathbf{Cpo}} is a lawful [bifunctor](dm-000M), that is:
5
+
\ol{
6
+
\li{ #{ (\lambda a. a) \times (\lambda b. b) = (\lambda x.x)} }
7
+
\li{ #{ (f_1 \circ g_1) \times (f_2 \circ g_2) = (f_1 \times f_2) \circ (g_1 \times g_2)} }
8
+
}
5
9
}
+1
-1
trees/dt/dt-003L.tree
+1
-1
trees/dt/dt-003L.tree
···
5
5
\p{With [the lifting operator](dt-003K), we can relate the lazy constructions like [product](dt-0021) and [sum](dt-0031) with [strict](dt-000K) constructions like [smash product](dt-003G) and [sum](dt-003H) via [isomorphism](dt-002E):
6
6
\ul{
7
7
\li{ #{A\contto B \simeq A_\bot \strictto B}}
8
-
\li{ #{A + B \;\; \simeq A_\bot \oplus B_\bot}}
8
+
\li{ #{A + B \simeq A_\bot \oplus B_\bot}}
9
9
\li{ #{(A \times B)_\bot \simeq A_\bot \otimes B_\bot } }
10
10
}
11
11
}