my forest
finished functions
+343
-5
+5
trees/dm-000Q.tree
+5
trees/dm-000Q.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\title{Dual category}
4
+
\taxon{Definition}
5
+
\p{The \em{dual} of a [category](dm-000G) #{\mathbf{C}}, written #{\mathbf{C}^\mathsf{op}}, is a [category](dm-000G) with the same objects as #{\mathbf{C}} but the arrows are reversed, that is, for each morphism #{A \xrightarrow{m} B} in #{\mathbf{C}}, there is a morphism #{B \xrightarrow{m} A} in #{\mathbf{C}^\mathsf{op}}.}
+1
-1
trees/dt-001O.tree
+1
-1
trees/dt-001O.tree
···
1
1
\import{dt-macros}
2
2
\taxon{Theorem}
3
3
\author{liamoc}
4
-
\title{Alternative definition of continuity}
4
+
\title{Alternative characterisation of continuity}
5
5
\p{A function #{f : A \rightarrow B} on [cpos](dt-001D) #{A} and #{B} is [continuous](dt-001J) iff:
6
6
\ol{
7
7
\li{#{f} is [monotonic](dt-000J), and}
+1
trees/dt-001U.tree
+1
trees/dt-001U.tree
···
1
1
\import{dt-macros}
2
2
\title{Semantics of recursive functions}
3
+
\taxon{Example}
3
4
\author{liamoc}
4
5
\p{Consider the function #{\Phi \in (\mathbb{N}_\bot \rightarrow \mathbb{N}_\bot) \rightarrow (\mathbb{N}_\bot \rightarrow \mathbb{N}_\bot)}, given by:
5
6
##{\Phi(f) = \lambda n.\ \text{if}\ n = 0\ \text{then}\ 1\ \text{else}\ n\cdot f(n-1)}
+1
-3
trees/dt-001Z.tree
+1
-3
trees/dt-001Z.tree
+1
-1
trees/dt-0024.tree
+1
-1
trees/dt-0024.tree
···
4
4
\title{Continuity of split}
5
5
\author{liamoc}
6
6
\p{For [continuous functions](dt-001J) #{f} and #{g}, the [split function](dt-0023) #{\langle f, g \rangle} is [continuous](dt-001J).}
7
-
\proofblock{
7
+
\proofblock{\p{Using the [alternative characterisation of continuity](dt-001O):}
8
8
\ul{
9
9
\li{ \em{#{\langle f, g \rangle} is [monotonic](dt-000J)}. Let #{x \sqsubseteq y \in A}. Then: ##{\begin{array}{lclr}
10
10
\langle f , g \rangle\ x & = & (f(x), g(x)) & \text{(def)}\\
+33
trees/dt-002L.tree
+33
trees/dt-002L.tree
···
1
+
\import{dt-macros}
2
+
\taxon{Construction}
3
+
\title{The cpo of functions}
4
+
\author{liamoc}
5
+
6
+
7
+
\p{If #{A} and #{B} are [cpos](dt-001D), the set of [continuous functions](dt-002F) #{A \contto B} is a [cpo](dt-001D) under the \em{pointwise} ordering:
8
+
##{
9
+
f \sqsubseteq g\;\; \text{iff}\;\; \forall a \in A.\ f(a) \sqsubseteq g(a)
10
+
}
11
+
The intuition of this ordering in terms of information is that we increase the information content of a function overall by increasing the information content of any (or many) argument values. To prove this, we must show:
12
+
\ol{
13
+
\li{ \em{#{A \contto B} has a [least element](dt-000A).} #{\bot_{A \contto B}} is the constant function that returns #{\bot_B}, i.e. #{\lambda a.\ \bot_B}.}
14
+
\li{ \em{#{\bigsqcup X} exists for all [directed](dt-0010) #{X \subseteq A \contto B}}. Our [lub](dt-0017) of a set of continuous functions #{\bigsqcup X} is the function #{\Phi} where: ##{\Phi(a) = \bigsqcup \Set{ f(a) \mid f \in X}}
15
+
We must show a number of properties of this [lub](dt-0017) #{\Phi}. Specifically:
16
+
\ol{
17
+
\li{ \em{#{\bigsqcup \Set{ f(a) \mid f \in X}} exists in #{B}}. \proofblock{We want to show that the set #{\Set{ f(a) \mid f \in X}} is [directed](dt-0010). Take two values #{g(a), h(a) \in \Set{ f(a) \mid f \in X}}. Since #{X} is [directed](dt-0010), there exists a function #{k \in X} such that #{g \sqsubseteq k} and #{h \sqsubseteq k}. By applying the definition of #{\sqsubseteq} for functions above, we have #{g(a) \sqsubseteq k(a)} and #{h(a) \sqsubseteq k(a)}. Thus #{k(a)} is an [upper bound](dm-000C) of these two values #{g(a), h(a)}, and thus #{\Set{ f(a) \mid f \in X}} is [directed](dt-0010), and thus its [lub](dt-0017) exists since #{B} is a [cpo](dt-001D).}}
18
+
\li{ \em{#{ \Phi(a) = \bigsqcup \Set{ f(a) \mid f \in X } } is continuous}. \proofblock{\p{Using the [alternative characterisation of continuity](dt-001O)}
19
+
##{
20
+
\begin{array}{lclr}
21
+
\Phi(\bigsqcup Y) &=& \bigsqcup\{ f(\bigsqcup Y) \mid f \in X \} & \text{(defn. $\Phi$)}\\
22
+
& = & \bigsqcup \{\bigsqcup \{ f(y) \mid y \in Y \} \mid f \in X \} & \text{($f$ is continuous)}\\
23
+
& = & \bigsqcup \{\bigsqcup \{ f(y) \mid f \in X \} \mid y \in Y \} & \text{(swap lubs)}\\
24
+
& = & \bigsqcup \{ \Phi(y) \mid y \in Y \} & \text{(defn. $\Phi$)}\\
25
+
\end{array}
26
+
}
27
+
Monotonicity is similar to prove.}}
28
+
\li{ \em{#{\Phi} is an [upper bound](dm-000C) for #{X \subseteq A \contto B}}. \proofblock{
29
+
Let #{g \in X}. Then for any #{a \in A} we have #{g(a) \in \Set{ f(a) \mid f \in X}}. Now, by 2a and lubs, we have #{g(a) \sqsubseteq \bigsqcup \Set{ f(a) \mid f \in X }}, which by the definition of #{\Phi} gives #{g(a) \sqsubseteq \Phi(a)}. Hence, by the definition of #{\sqsubseteq} on functions, we can conclude #{g \sqsubseteq \Phi}.}}
30
+
\li{ \em{#{\Phi} is the [least upper bound](dt-0017) for #{X}}. \proofblock{ Let #{g \in A \contto B} be an [upper bound](dm-000C) for #{X \subseteq A \contto B}. Then (using #{\sqsubseteq} on functions) #{g(a)} is an [upper bound](dm-000C) for #{\Set{f(a) \mid f \in X}} for all #{a \in A}. Now, by 2a and lubs, we have #{\bigsqcup\Set{f(a) \mid f \in X} \sqsubseteq g(a)}, i.e. #{\Phi(a) \sqsubseteq g(a)}, which, by the definition of #{\sqsubseteq} on functions, allows us to conclude #{\Phi \sqsubseteq g}.}}
31
+
}
32
+
}
33
+
}}
+143
trees/dt-002M.tree
+143
trees/dt-002M.tree
···
1
+
\import{dt-macros}
2
+
\taxon{Example}
3
+
\title{The space #{\mathbb{B}_\bot \contto \mathbb{B}_\bot}}
4
+
\author{liamoc}
5
+
\p{
6
+
\tex{\usepackage{tikz-cd}}{
7
+
\begin{tikzcd}[column sep=1em]
8
+
{\begin{tikzpicture}
9
+
\draw[rounded corners, thick, fill=white] (-0.8,-0.7) rectangle (0.8,1.39);
10
+
\node (tr) at (0.5,0.5) {$\bullet$};
11
+
\node (tl) at (-0.5,0.5) {$\bullet$};
12
+
\node (b) at (0,-0.5) {$\bullet$};
13
+
\draw[thick] (b) -- (tr) (b) -- (tl);
14
+
\draw[thick,draw=blue,->] (b) edge[bend right] (tl)
15
+
(tl) edge[loop above] (tl)
16
+
(tr) edge[bend right=1.3em] (tl);
17
+
\end{tikzpicture}
18
+
}
19
+
&&
20
+
&&
21
+
&&
22
+
{\begin{tikzpicture}
23
+
\draw[rounded corners, thick, fill=white] (-0.8,-0.7) rectangle (0.8,1.39);
24
+
\node (tr) at (0.5,0.5) {$\bullet$};
25
+
\node (tl) at (-0.5,0.5) {$\bullet$};
26
+
\node (b) at (0,-0.5) {$\bullet$};
27
+
\draw[thick] (b) -- (tr) (b) -- (tl);
28
+
\draw[thick,draw=blue,->] (b) edge[bend right] (tr)
29
+
(tl) edge[bend left=1.3em] (tr)
30
+
(tr) edge[loop above] (tr);
31
+
\end{tikzpicture}
32
+
}
33
+
\\
34
+
{\begin{tikzpicture}
35
+
\draw[rounded corners, thick, fill=white] (-0.8,-1.2) rectangle (0.8,0.9);
36
+
\node (tr) at (0.5,0.5) {$\bullet$};
37
+
\node (tl) at (-0.5,0.5) {$\bullet$};
38
+
\node (b) at (0,-0.5) {$\bullet$};
39
+
\draw[thick] (b) -- (tr) (b) -- (tl);
40
+
\draw[thick,draw=blue,->] (b) edge[loop below] (b)
41
+
(tl) edge[loop below] (tl)
42
+
(tr) edge[bend right=1.3em] (tl);
43
+
\end{tikzpicture}
44
+
}\ar[u,ultra thick,-]
45
+
&&
46
+
{\begin{tikzpicture}
47
+
\draw[rounded corners, thick, fill=white] (-0.8,-1.2) rectangle (0.8,0.9);
48
+
\node (tr) at (0.5,0.5) {$\bullet$};
49
+
\node (tl) at (-0.5,0.5) {$\bullet$};
50
+
\node (b) at (0,-0.5) {$\bullet$};
51
+
\draw[thick] (b) -- (tr) (b) -- (tl);
52
+
\draw[thick,draw=blue] (b) edge[loop below,->] (b)
53
+
(tl) edge[loop below,->] (tl)
54
+
(tr) edge[loop below] (tr);
55
+
\end{tikzpicture}
56
+
}
57
+
&&
58
+
{\begin{tikzpicture}
59
+
\draw[rounded corners, thick, fill=white] (-0.8,-1.2) rectangle (0.8,0.9);
60
+
\node (tr) at (0.5,0.5) {$\bullet$};
61
+
\node (tl) at (-0.5,0.5) {$\bullet$};
62
+
\node (b) at (0,-0.5) {$\bullet$};
63
+
\draw[thick] (b) -- (tr) (b) -- (tl);
64
+
\draw[thick,draw=blue,->] (b) edge[loop below] (b)
65
+
(tr) edge[bend left=1.3em] (tl)
66
+
(tl) edge[bend left=1.3em] (tr);
67
+
\end{tikzpicture}
68
+
}
69
+
&&
70
+
{\begin{tikzpicture}
71
+
\draw[rounded corners, thick, fill=white] (-0.8,-1.2) rectangle (0.8,0.9);
72
+
\node (tr) at (0.5,0.5) {$\bullet$};
73
+
\node (tl) at (-0.5,0.5) {$\bullet$};
74
+
\node (b) at (0,-0.5) {$\bullet$};
75
+
\draw[thick] (b) -- (tr) (b) -- (tl);
76
+
\draw[thick,draw=blue,->] (b) edge[loop below] (b)
77
+
(tl) edge[bend left=1.3em] (tr)
78
+
(tr) edge[loop below] (tr);
79
+
\end{tikzpicture}
80
+
}\ar[u,ultra thick,-]
81
+
\\
82
+
{\begin{tikzpicture}
83
+
\draw[rounded corners, thick, fill=white] (-0.8,-1.2) rectangle (0.8,0.9);
84
+
\node (tr) at (0.5,0.5) {$\bullet$};
85
+
\node (tl) at (-0.5,0.5) {$\bullet$};
86
+
\node (b) at (0,-0.5) {$\bullet$};
87
+
\draw[thick] (b) -- (tr) (b) -- (tl);
88
+
\draw[thick,draw=blue,->] (b) edge[loop below] (b)
89
+
(tl) edge[loop right] (tl)
90
+
(tr) edge[bend left] (b);
91
+
\end{tikzpicture}
92
+
}\ar[u,ultra thick,-]\ar[urr,ultra thick,-]
93
+
&&
94
+
{\begin{tikzpicture}
95
+
\draw[rounded corners, thick, fill=white] (-0.8,-1.2) rectangle (0.8,0.9);
96
+
\node (tr) at (0.5,0.5) {$\bullet$};
97
+
\node (tl) at (-0.5,0.5) {$\bullet$};
98
+
\node (b) at (0,-0.5) {$\bullet$};
99
+
\draw[thick] (b) -- (tr) (b) -- (tl);
100
+
\draw[thick,draw=blue,->] (b) edge[loop below] (b)
101
+
(tl) edge[bend right] (b)
102
+
(tr) edge[bend right=1.3em] (tl);
103
+
\end{tikzpicture}
104
+
}\ar[ull,ultra thick,-]\ar[urr,ultra thick,-]
105
+
&&
106
+
{\begin{tikzpicture}
107
+
\draw[rounded corners, thick, fill=white] (-0.8,-1.2) rectangle (0.8,0.9);
108
+
\node (tr) at (0.5,0.5) {$\bullet$};
109
+
\node (tl) at (-0.5,0.5) {$\bullet$};
110
+
\node (b) at (0,-0.5) {$\bullet$};
111
+
\draw[thick] (b) -- (tr) (b) -- (tl);
112
+
\draw[thick,draw=blue,->] (b) edge[loop below] (b)
113
+
(tr) edge[bend left] (b)
114
+
(tl) edge[bend left=1.3em] (tr);
115
+
\end{tikzpicture}
116
+
}\ar[u,ultra thick,-]\ar[urr,ultra thick,-]
117
+
&&
118
+
{\begin{tikzpicture}
119
+
\draw[rounded corners, thick, fill=white] (-0.8,-1.2) rectangle (0.8,0.9);
120
+
\node (tr) at (0.5,0.5) {$\bullet$};
121
+
\node (tl) at (-0.5,0.5) {$\bullet$};
122
+
\node (b) at (0,-0.5) {$\bullet$};
123
+
\draw[thick] (b) -- (tr) (b) -- (tl);
124
+
\draw[thick,draw=blue,->] (b) edge[loop below] (b)
125
+
(tl) edge[bend right] (b)
126
+
(tr) edge[loop left] (tr);
127
+
\end{tikzpicture}
128
+
}\ar[u,ultra thick,-]\ar[ullll,ultra thick,-]
129
+
\\
130
+
&\qquad &&{\begin{tikzpicture}
131
+
\draw[rounded corners, thick, fill=white] (-0.8,-1.2) rectangle (0.8,0.9);
132
+
\node (tr) at (0.5,0.5) {$\bullet$};
133
+
\node (tl) at (-0.5,0.5) {$\bullet$};
134
+
\node (b) at (0,-0.5) {$\bullet$};
135
+
\draw[thick] (b) -- (tr) (b) -- (tl);
136
+
\draw[thick,draw=blue,->] (b) edge[loop below] (b)
137
+
(tl) edge[bend right] (b)
138
+
(tr) edge[bend left] (b);
139
+
\end{tikzpicture}
140
+
}\ar[ul, ultra thick,-] \ar[ur, ultra thick,-] \ar[ulll, ultra thick,-] \ar[urrr, ultra thick,-] &&\qquad
141
+
\end{tikzcd}
142
+
}
143
+
At each step "upwards" on this [cpo](dt-001D), one arrow that ends in #{\bot} now points to a non-#{\bot} value (moving up the [cpo](dt-001D) #{\mathbb{B}_\bot}).}
+11
trees/dt-002N.tree
+11
trees/dt-002N.tree
···
1
+
\import{dt-macros}
2
+
\taxon{Definition}
3
+
\author{liamoc}
4
+
\title{The #{\mathit{apply}} function}
5
+
\p{The #{\mathit{apply}} function simply applies a given function to a given argument:
6
+
##{
7
+
\begin{array}{l}
8
+
\mathit{apply} : ((A \contto B) \times A) \contto B\\
9
+
\mathit{apply} (f, a) = f(a)
10
+
\end{array}
11
+
}}
+12
trees/dt-002O.tree
+12
trees/dt-002O.tree
···
1
+
\import{dt-macros}
2
+
\taxon{Definition}
3
+
\author{liamoc}
4
+
\title{The #{\mathit{curry}} function}
5
+
\p{The function #{\mathit{curry}} transforms a function that takes two arguments all at once (as a [product](dm-0005)) into a function that takes the arguments one at a time. That is, if #{f : A \times B \contto C} then:
6
+
##{
7
+
\begin{array}{l}
8
+
\mathit{curry}(f) : A \contto (B \contto C)\\
9
+
\mathit{curry}(f)(a)(b) = f(a, b)
10
+
\end{array}
11
+
}
12
+
}
+8
trees/dt-002P.tree
+8
trees/dt-002P.tree
+22
trees/dt-002Q.tree
+22
trees/dt-002Q.tree
···
1
+
\import{dt-macros}
2
+
\taxon{Exercise}
3
+
\author{liamoc}
4
+
\p{Show that #{\mathit{apply}} is [continuous](dt-001J).}
5
+
\p{\em{Hint:} A function #{f : A \times B \rightarrow C} is [continuous](dt-001J) iff it is [continuous](dt-001J) in each argument separately, i.e., iff #{\forall a \in A.\ f(a,\cdot) : B \rightarrow C} is continuous, and #{\forall b \in B.\ f(\cdot,b) : A \rightarrow C} is continuous.}
6
+
\solnblock{
7
+
\p{
8
+
First showing #{\mathit{apply}(f,\cdot)} is continuous for some continuous #{f : A \contto B}, using the [alternative characterisation](dt-001O)
9
+
\ol{
10
+
\li{ \em{#{\mathit{apply}(f,\cdot)} is monotonic}: Given #{a, b \in A} where #{a \sqsubseteq b}, we can see that #{\mathit{apply}(f,a) = f(a) \sqsubseteq f(b) = \mathit{apply}(f,b)} by the [monotonicity](dt-000J) of #{f}.
11
+
}
12
+
\li{ \em{#{\mathit{apply}(f,\cdot)} preserves lubs}: Given a [directed](dt-0010) #{X \subseteq A}, we can see that #{\mathit{apply}(f,\bigsqcup X) = f(\bigsqcup X) = \bigsqcup \Set{f(x) \mid x \in X} = \bigsqcup \Set{\mathit{apply}(f,x) \mid x \in X}} follows from the continuity of #{f}.
13
+
}
14
+
}
15
+
Next, showing #{\mathit{apply}(\cdot,a)} is continuous for some fixed #{a \in A}:
16
+
\ol{
17
+
\li{ \em{#{\mathit{apply}(\cdot,a)} is monotonic}: Given #{f, g \in A \contto B} where #{f \sqsubseteq g}, we can see that #{\mathit{apply}(f,a) = f(a) \sqsubseteq g(a) = \mathit{apply}(g,a)} by the [pointwise ordering of functions](dt-002L).
18
+
}
19
+
\li{ \em{#{\mathit{apply}(\cdot,a)} preserves lubs}: Given a [directed](dt-0010) #{X \subseteq A \contto B}, we can see that #{\mathit{apply}(\bigsqcup X, a) = \left(\bigsqcup X\right)(a) = \bigsqcup \Set{f(a) \mid f \in X} = \bigsqcup \Set{\mathit{apply}(f,a) \mid f \in X}} follows from the [lub definition for functions](dt-002L).
20
+
}
21
+
}
22
+
}}
+7
trees/dt-002R.tree
+7
trees/dt-002R.tree
+9
trees/dt-002S.tree
+9
trees/dt-002S.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\taxon{Theorem}
4
+
\title{Continuity of #{\mathit{curry}}}
5
+
\ol{
6
+
\li{#{\mathit{curry}} is [continuous](dt-001J) on #{A \times B \contto C}.}
7
+
\li{#{\mathit{curry}(f)}, given [continuous](dt-001J) #{f : A \times B \contto C}, is [continuous](dt-001J) on #{A}.}
8
+
\li{#{\mathit{curry}(f)(a)}, given [continuous](dt-001J) #{f : A \times B \contto C} and #{a \in A}, is [continuous](dt-001J) on #{B}.}
9
+
}
+15
trees/dt-002T.tree
+15
trees/dt-002T.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\taxon{Definition}
4
+
\title{Universal property for functions}
5
+
\figure{
6
+
\tex{\usepackage{tikz-cd}\usepackage{amssymb}}{
7
+
\begin{tikzcd}[row sep=4em]
8
+
A \times B \ar[d,dashed,labels=description,"\mathit{curry}(f)\times \mathsf{id}_B"] \ar[r,"f"] & C \\
9
+
(B \contto C) \times B \ar[ur, labels=below right,"\mathit{apply}"]
10
+
\end{tikzcd}
11
+
}
12
+
}
13
+
##{
14
+
\mathit{apply} \circ h = f\; \text{iff}\; h = \mathit{curry}(f)\times\mathsf{id}_B
15
+
}
+10
trees/dt-002U.tree
+10
trees/dt-002U.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\taxon{Theorem}
4
+
\title{The currying isomorphism}
5
+
##{
6
+
(A \times B)\contto C \;\;\simeq \;\; A\contto (B\contto C)
7
+
}
8
+
\proofblock{
9
+
\p{Follows from the [universal property for functions](dt-002T) when set up with the [isomorphism](dt-002E) from [curry](dt-002O) and its inverse, the function in \ref{dt-002R}.}
10
+
}
+14
trees/dt-002V.tree
+14
trees/dt-002V.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\taxon{Remark}
4
+
\title{Why the function arrow is not a covariant [bifunctor](dm-000M)}
5
+
\p{
6
+
For the #{\contto} operator on [cpos](dt-001D) (\ref{dt-002F}) to be the object mapping for a [bifunctor](dm-000M) #{\textbf{Cpo} \times \textbf{Cpo} \rightarrow \textbf{Cpo}} like #{\times} is (see \ref{dt-002C}), we would need to define a morphism mapping #{f \contto g} that, given two functions #{f : A \contto B} and #{g : C \contto D}, gives a function #{(A \contto C) \contto (B \contto D)}. But such a function is \em{not implementable}:
7
+
##{
8
+
\begin{array}{l}
9
+
f \contto g : (A \contto C) \contto (B \contto D) \\
10
+
(f \contto g)(h)(b) =\ \textcolor{red}{???}\\
11
+
\end{array}
12
+
}
13
+
In the above hole #{\textcolor{red}{???}}, #{h : A \contto C} and #{b \in B}. Given the value #{b \in B}, none of our functions #{f, g} or #{h} take elements of #{B}, so there would be no way to produce the #{D} value required. This is because our function #{f : A \contto B} goes \em{the wrong way}. If #{f} were a function #{B \contto A}, things would be a lot easier.
14
+
}
+14
trees/dt-002W.tree
+14
trees/dt-002W.tree
···
1
+
\import{dt-macros}
2
+
\title{The function arrow is a bifunctor}
3
+
\author{liamoc}
4
+
\p{The operator #{\contto} introduced in \ref{dt-002F} is is the object mapping for a [binary functor](dm-000M): ##{(\contto) : \mathbf{Cpo}^\mathsf{op} \times \mathbf{Cpo} \rightarrow \mathbf{Cpo}} The [category](dm-000G) #{\mathbf{Cpo}^\mathsf{op}} is the [dual category](dm-000Q) to #{\mathbf{Cpo}}.}
5
+
\p{
6
+
Thus, a morphism #{A \xrightarrow{m} B} in the [category](dm-000G) #{\mathbf{Cpo}^\mathsf{op}} is a [continuous](dt-001J) function #{m : B \contto A}. Thus, the morphism mapping for our [functor](dm-000J) must take two functions #{f : B \contto A} (the morphism from #{\mathbf{Cpo}^\mathsf{op}}) and #{g : C \contto D} (the morphism from #{\mathbf{Cpo}}), and produce #{(A \contto C) \contto (B \contto D)}. As with [products](dt-0026), we will overload the #{\contto} notation for this mapping as well. }
7
+
\transclude{dt-002X}
8
+
\transclude{dt-002Y}
9
+
\scope{
10
+
\put\transclude/toc{false}
11
+
\put\transclude/numbered{false}
12
+
\subtree{\taxon{Upshot}
13
+
\p{Our [category #{\textbf{Cpo}}](dt-002B) has \em{exponentials}.}
14
+
}}
+14
trees/dt-002X.tree
+14
trees/dt-002X.tree
···
1
+
\import{dt-macros}
2
+
\taxon{Definition}
3
+
\author{liamoc}
4
+
\title{Morphism mapping for #{\contto}}
5
+
\p{
6
+
Given #{f : B \contto A} and #{g : C \contto D}, we have:
7
+
##{
8
+
\begin{array}{l}
9
+
f \contto g : (A \contto C) \contto (B \contto D)\\
10
+
f \contto g = \mathit{curry}\ (g \circ \mathit{apply} \circ (\mathsf{id} \times f))\\[2em]
11
+
\text{(or, operationally:)}\\
12
+
(f \contto g)(h) = g \circ h \circ f\\
13
+
\end{array}}
14
+
}
+10
trees/dt-002Y.tree
+10
trees/dt-002Y.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\taxon{Theorem}
4
+
\p{
5
+
The two [functor](dm-000J) laws follow as a consequence of the [universal property](dt-002T) for functions:
6
+
\ol{
7
+
\li{ #{\mathsf{id}_A \contto \mathsf{id}_B = \mathsf{id}_{A \contto B}}}
8
+
\li{ #{(f \circ g) \contto (h \circ i) = (g \contto h) \circ (f \contto i)}}
9
+
}
10
+
}
+12
trees/dt-002Z.tree
+12
trees/dt-002Z.tree
···
1
+
\import{dt-macros}
2
+
\title{Functions}
3
+
\author{liamoc}
4
+
\p{Previously, such as in \ref{dt-001U}, we already implicitly assumed that the set of [continuous functions](dt-002F) on [cpos](dt-001D) #{A \contto B} is itself a [cpo](dt-001D). In this section, we will formalise this construction.}
5
+
\transclude{dt-002L}
6
+
\transclude{dt-002M}
7
+
\transclude{dt-002P}
8
+
\transclude{dt-002T}
9
+
\transclude{dt-002U}
10
+
\transclude{dt-002V}
11
+
\transclude{dm-000Q}
12
+
\transclude{dt-002W}