diff --git a/trees/dm/dm-000S.tree b/trees/dm/dm-000S.tree
new file mode 100644
index 0000000..dd95935
--- /dev/null
+++ b/trees/dm/dm-000S.tree
@@ -0,0 +1,4 @@
+\taxon{Definition}
+\author{liamoc}
+\title{Contravariant functor}
+\p{A \em{contravariant} [functor](dm-000J) #{\mathcal{F}} is a [functor](dm-000J) that, instead of associating a morphism #{X \xrightarrow{m} Y} with a morphism #{\mathcal{F}(X) \xrightarrow{\mathcal{F}(m)} \mathcal{F}(Y)}, it instead gives a morphism #{\mathcal{F}(Y) \xrightarrow{\mathcal{F}(m)} \mathcal{F}(X)$}. Alternatively, it can be viewed as a functor from the [dual category](dm-000Q).}
\ No newline at end of file
diff --git a/trees/dt/dt-004M.tree b/trees/dt/dt-004M.tree
index 371c1bc..ab01dce 100644
--- a/trees/dt/dt-004M.tree
+++ b/trees/dt/dt-004M.tree
@@ -2,7 +2,7 @@
 \author{liamoc}
 \title{Untyped higher-order languages}
 \p{
-	If we take [PCF](dt-003T), \em{discard} the type system, #{\syn{fix}}, natural number primitives and any other superfluous features, and just boil our language down to a minimal, Turing-complete subset, we end up with the [untyped #{\lambda}-calculus](dt-004K) — a language consisting only of untyped functions.}
+	If we take [PCF](dt-003T), \em{discard} the type system, [#{\textbf{fix}}](dt-001Q), natural number primitives and any other superfluous features, and just boil our language down to a minimal, Turing-complete subset, we end up with the [untyped #{\lambda}-calculus](dt-004K) — a language consisting only of untyped functions.}
 \transclude{dt-004K}
 \p{Trying to give a semantics to the [untyped #{\lambda} calculus](dt-004K) poses an issue: we can no longer rely on the type of an expression to select an appropriate semantic domain. Instead, we we must pick a \em{single} domain #{D} which, since functions can be applied to themselves, must apparently include the set of functions #{D \contto  D}:
 ##{
diff --git a/trees/dt/dt-004O.tree b/trees/dt/dt-004O.tree
index 14ef8cf..e945d18 100644
--- a/trees/dt/dt-004O.tree
+++ b/trees/dt/dt-004O.tree
@@ -20,4 +20,5 @@
 \transclude{dt-004V}
 \transclude{dt-004W}
 \transclude{dt-004X}
-\transclude{dt-004Y}
\ No newline at end of file
+\transclude{dt-004Y}
+\transclude{dt-0050}
\ No newline at end of file
diff --git a/trees/dt/dt-004Z.tree b/trees/dt/dt-004Z.tree
index 493ec3a..5addd7e 100644
--- a/trees/dt/dt-004Z.tree
+++ b/trees/dt/dt-004Z.tree
@@ -4,4 +4,5 @@
 \p{This lecture is based on material from [[haskellhutt]], [[jlongley]],[[danascott]], [[jstoy]], [[cgunter]], and [[gwinskel]].}
 \transclude{dt-004J}
 \transclude{dt-004O}
+\transclude{dt-0052}
 \p{\strong{TODO: Retraction pairs stuff}}
\ No newline at end of file
diff --git a/trees/dt/dt-0050.tree b/trees/dt/dt-0050.tree
new file mode 100644
index 0000000..46ae7f1
--- /dev/null
+++ b/trees/dt/dt-0050.tree
@@ -0,0 +1,5 @@
+\import{dt-macros}
+\title{Constructing endofunctors}
+\author{liamoc}
+\p{If we have a mapping on [cpos](dt-001D) #{\mathcal{F} : \textbf{Cpo} \rightarrow \textbf{Cpo}} that is made up of the primitives #{\times}, #{+}, #{\otimes}, #{\oplus}, #{\mathbf{1}} and #{(\cdot)_\bot}, we can generate a corresponding \em{morphism mapping} on continuous functions #{\mathcal{F} : (A\contto B) \rightarrow (\mathcal{F}(A)\contto \mathcal{F}(B))} by using the corresponding morphism mappings of each of these operators. Thus any such mapping can be turned into an [endofunctor](dt-004T).}
+\transclude{dt-0051}
diff --git a/trees/dt/dt-0051.tree b/trees/dt/dt-0051.tree
new file mode 100644
index 0000000..2fd8c25
--- /dev/null
+++ b/trees/dt/dt-0051.tree
@@ -0,0 +1,11 @@
+\import{dt-macros}
+\title{Making endofunctors for algebraic data types}
+\taxon{Example}
+\author{liamoc}
+\p{ ##{
+  \begin{array}{llr}
+    \textsf{Object mapping} & \textsf{Morphism mapping}\\[0.2em]
+    \mathcal{F}(X) = X + \mathbf{1} &  \mathcal{F}(f) = f + \mathsf{id}_\mathbf{1} & \quad\quad\text{((co)-natural numbers)} \\
+    \mathcal{F}(X) = \mathbf{1} + (\mathbb{Z}_\bot \times X) & \mathcal{F}(f) = \mathsf{id}_\mathbf{1} + (\mathsf{id}_{\mathbb{Z}_\bot} \times f) & \text{((co)-lists of integers)}\\		
+  \end{array}
+}}
\ No newline at end of file
diff --git a/trees/dt/dt-0052.tree b/trees/dt/dt-0052.tree
new file mode 100644
index 0000000..e22c60a
--- /dev/null
+++ b/trees/dt/dt-0052.tree
@@ -0,0 +1,12 @@
+\import{dt-macros}
+\author{liamoc}
+\title{From #{\textbf{Cpo}} to #{\textbf{Cpo}^{\textbf{R}}}}
+\transclude{dt-0053}
+\transclude{dt-0054}
+\transclude{dt-0055}
+\transclude{dt-0056}
+\transclude{dt-0057}
+\transclude{dt-0058}
+\transclude{dt-0059}
+\transclude{dt-005A}
+\transclude{dt-005B}
diff --git a/trees/dt/dt-0053.tree b/trees/dt/dt-0053.tree
new file mode 100644
index 0000000..5c620c0
--- /dev/null
+++ b/trees/dt/dt-0053.tree
@@ -0,0 +1,13 @@
+\import{dt-macros}
+\taxon{Problem}
+\author{liamoc}
+\title{Contravariance in the function arrow}
+\p{We cannot get morphism mappings in [the category #{\textbf{Cpo}}](dt-002B) as easily as \ref{dt-0050} when our object mapping makes use of the function operators #{\strictto} and #{\contto}, as they are [contravariant](dm-000S) in their first argument. This means the [functor](dm-000J) that they extend to is not #{\textbf{Cpo} \rightarrow \textbf{Cpo}} but #{\textbf{Cpo}^\textsf{op} \rightarrow \textbf{Cpo}}, where #{\textbf{Cpo}^\textsf{op} } is the [dual category](dm-000Q) of #{\textbf{Cpo}}. The morphisms end up the wrong way around. }
+
+\p{As an example, consider #{\mathcal{F}(X) = X\contto\mathbb{Z}_\bot}. Then, recalling [the morphism mapping of the #{\contto} functor](dt-002X):
+##{
+\inferrule{f : A \contto B \quad g : C\contto D}{f\contto g : (B\contto C)\contto (A\contto D)}
+}
+We can generate a morphism mapping for #{\mathcal{F}}: ##{\mathcal{F}(f)\; =\; f\contto\mathsf{id}_{\mathbb{Z}_\bot}\; =\; (\lambda h.\ \mathsf{id}_{\mathbb{Z}_\bot}\circ h \circ f)\; = \;(\lambda h.\ h \circ f)  }
+However, this mapping has the wrong type. For #{f : A\contto B}, then #{\mathcal{F}(f) : (B\contto \mathbb{Z}_\bot) \rightarrow (A\contto \mathbb{Z}_\bot)}, which is #{\mathcal{F}(B)\contto\mathcal{F}(A)}, not the required #{\mathcal{F}(A)\contto \mathcal{F}(B)}. This is because the generated functor is [contravariant](dm-000S), not [covariant](dm-000J).
+}
\ No newline at end of file
diff --git a/trees/dt/dt-0054.tree b/trees/dt/dt-0054.tree
new file mode 100644
index 0000000..4d73867
--- /dev/null
+++ b/trees/dt/dt-0054.tree
@@ -0,0 +1,14 @@
+\import{dt-macros}
+\taxon{Definition}
+\title{Retraction pair}
+\author{liamoc}
+\p{A \em{retraction pair} #{(f,g)} on [cpos](dt-001D) #{A} to #{B} consists of two [continuous](dt-001J) functions #{A \rpair{f}{g} B} 
+ such that:
+\ol{
+\li{#{g \circ f = \mathsf{id}_A\quad}  (i.e. #{\forall x \in A.\ g(f(x)) = x })}
+\li{ #{f \circ g \sqsubseteq \mathsf{id}_B\quad}  (i.e. #{\forall y \in B.\ f(g(y)) \sqsubseteq y })}
+}
+In this retraction pair, #{f} is called a \em{embedding} and #{g} is called a \em{projection}.
+}
+\p{
+Retraction pairs are weakenings of [isomorphisms](dt-002E). Intuitively, going #{A \contto B\contto A}, all information is \em{preserved} due to requirement 1, but going #{B\contto A\contto B}, we \em{may lose} some information (hence the use of #{\sqsubseteq} in requirement 2). }
diff --git a/trees/dt/dt-0055.tree b/trees/dt/dt-0055.tree
new file mode 100644
index 0000000..35aa0c4
--- /dev/null
+++ b/trees/dt/dt-0055.tree
@@ -0,0 +1,46 @@
+\import{dt-macros}
+\import{table-macros}
+\taxon{Example}
+\author{liamoc}
+\title{Examples and counterexamples of retraction pairs}
+\p{Here are two examples of [retraction pairs](dt-0054):
+\figure{
+\tex{\usepackage{tikz-cd}}{
+\begin{tikzcd}
+ & z \ar[dl, thick,->] \\
+ b \ar[r,thick,<->] & y \ar[u,-] \\
+ a\ar[u,-]\ar[r,thick,<->] & x \ar[u,-]	
+\end{tikzcd}
+$\quad\qquad\qquad$
+\begin{tikzcd}
+ & z \ar[dl, thick,<->] \\
+ b & y \ar[dl, thick,->] \ar[u,-] \\
+ a\ar[u,-]\ar[r,thick,<->] & x \ar[u,-]	
+\end{tikzcd}}}
+(this demonstrates that there can be \em{many} [retraction pairs](dt-0054) #{A \rpair{f}{g} B})}
+\p{The following, however, are \em{not} [retraction pairs](dt-0054) #{A \rpair{f}{g} B}:
+\figure{
+\tableW{\tr{\td{
+\tex{\usepackage{tikz-cd}}{
+\begin{tikzcd}
+ & z \ar[dl, thick,<->] \\
+ b \ar[r,thick,<-] & y \ar[u,-] \\
+ a\ar[u,-]\ar[r,thick,<->] & x \ar[u,-]	
+\end{tikzcd}
+}}\td{
+\tex{\usepackage{tikz-cd}}{
+\begin{tikzcd}
+ & z \ar[dl, thick,->] \\
+ b \ar[dr, thick,->] & y \ar[l, thick,->] \ar[u,-] \\
+ a\ar[u,-]\ar[r,thick,<->] & x \ar[u,-]	
+\end{tikzcd}
+}}}
+\tr{
+  \td{
+    (#{y \mapsto b \mapsto z} but #{z \not\sqsubseteq y})
+  }
+  \td{
+    (#{b \mapsto x \mapsto a} but #{a \neq b})
+  }
+}
+}}}
\ No newline at end of file
diff --git a/trees/dt/dt-0056.tree b/trees/dt/dt-0056.tree
new file mode 100644
index 0000000..c81c2d6
--- /dev/null
+++ b/trees/dt/dt-0056.tree
@@ -0,0 +1,13 @@
+\import{dt-macros}
+\title{Composition of retraction pairs}
+\taxon{Definition}
+\author{liamoc}
+\p{We can compose [retraction pairs](dt-0054) by composing their \em{embedding} and \em{projection}:}
+\figure{
+  \tex{\usepackage{tikz-cd}\usepackage{amsmath}\usepackage{amssymb}}{
+    \begin{tikzcd}
+      A \ar[r,"f",yshift=0.2em] & B \ar[l,"g", ,yshift=-0.2em] 
+        \ar[r,"h",yshift=0.2em] & C \ar[l,"i", ,yshift=-0.2em] &\leadsto & 
+      A \ar[r,"h \circ f",yshift=0.2em] & C \ar[l,"g \circ i",yshift=-0.2em] &\quad
+     \end{tikzcd}
+}}
\ No newline at end of file
diff --git a/trees/dt/dt-0057.tree b/trees/dt/dt-0057.tree
new file mode 100644
index 0000000..ea22df0
--- /dev/null
+++ b/trees/dt/dt-0057.tree
@@ -0,0 +1,10 @@
+\import{dt-macros}
+\taxon{Corollary}
+\title{Derived products of retraction pairs}
+\p{It follows from the definition of [retraction pairs](dt-0054) that, for a pair #{\rpair{f}{g}}:
+\ol{
+\li{ #{f} and #{g} are [strict](dt-000K), i.e. #{f(\bot) = \bot} and #{g(\bot) = \bot}.}
+\li{ #{g} is \em{uniquely determined} by #{f} and vice-versa, so if another [retraction pair](dt-0054) #{\rpair{f}{g'}} exists, then #{g = g'}. To see why, remember that #{f} and #{g} must be [continuous](dt-001J) and therefore [monotonic](dt-000J).}
+\li{ #{A} is [isomorphic](dt-002E) to the range of #{f}, i.e. #{A \simeq \Set{ f(x) \mid x \in A} \subseteq B}.} 
+}
+}
\ No newline at end of file
diff --git a/trees/dt/dt-0058.tree b/trees/dt/dt-0058.tree
new file mode 100644
index 0000000..d69283e
--- /dev/null
+++ b/trees/dt/dt-0058.tree
@@ -0,0 +1,5 @@
+\import{dt-macros}
+\taxon{Definition}
+\title{The category #{\textbf{Cpo}^\textbf{R}}}
+\author{liamoc}
+\p{The category #{\textbf{Cpo}^\textbf{R}} is the [category](dm-000G) where the objects are [cpos](dt-001D), the morphisms are [retraction pairs](dt-0054), composition is as in \ref{dt-0056} and identity is just the [retraction pair](dt-0054) #{A \rpair{\lambda x. x}{\lambda x. x} A}.  }
\ No newline at end of file
diff --git a/trees/dt/dt-0059.tree b/trees/dt/dt-0059.tree
new file mode 100644
index 0000000..4c2b36f
--- /dev/null
+++ b/trees/dt/dt-0059.tree
@@ -0,0 +1,8 @@
+\import{dt-macros}
+\author{liamoc}
+\taxon{Definition}
+\title{Information ordering in #{\textbf{Cpo}^\textbf{R}}}
+\p{
+The third point in \ref{dt-0057} suggests a notion of approximation, or [information ordering](dt-000B), for [cpos](dt-001D). Rather than say, as we did in \ref{dt-004O}, that for [cpos](dt-001D) #{A} and #{B}, #{A \sqsubseteq B} iff there exists a [continuous function](dt-001J) #{A\contto B}, we now say:
+\figure{#{A \sqsubseteq B} iff there exists a [retraction pair](dt-0054) #{A \rpair{f}{g} B}}
+}
\ No newline at end of file
diff --git a/trees/dt/dt-005A.tree b/trees/dt/dt-005A.tree
new file mode 100644
index 0000000..7a1767a
--- /dev/null
+++ b/trees/dt/dt-005A.tree
@@ -0,0 +1,4 @@
+\title{Generalising to #{\textbf{Cpo}^\textbf{R}}}
+\author{liamoc}
+\p{All of our other notions for #{\textbf{Cpo}} naturally generalise to a setting with  [retraction pairs](dt-0054) #{\textbf{Cpo}^\textbf{R}}: least elements, [#{\omega}-chains](dt-004Q), [upper bounds](dt-004R), [colimits](dt-004S), [cocontinuous endofunctors](dt-004V) and so on.}
+\transclude{dt-005C}
\ No newline at end of file
diff --git a/trees/dt/dt-005B.tree b/trees/dt/dt-005B.tree
new file mode 100644
index 0000000..09f9f56
--- /dev/null
+++ b/trees/dt/dt-005B.tree
@@ -0,0 +1,18 @@
+\taxon{Theorem}
+\title{Fixed point theorem for endofunctors on #{\textbf{Cpo}^\textbf{R}}}
+\p{Every [cocontinuous endofunctor](TODO) #{\mathcal{F}} on #{\mathbf{Cpo}^\textbf{R}} has a least fixed point, given by the [colimit](TODO) of the ascending [#{\omega}-chain](dt-005C):
+\figure{
+\tex{\usepackage{tikz-cd}}{\begin{tikzcd}
+  \mathbf{1} \ar[r,"f_0",->,yshift=0.2em]\ar[r,"g_0"', <-,yshift=-0.2em]  &
+  \mathcal{F}(\mathbf{1}) \ar[r,"f_1",->,yshift=0.2em]\ar[r,"g_1"', <-,yshift=-0.2em]  &
+  \mathcal{F}(\mathcal{F}(\mathbf{1})) \ar[r,"f_2",->,yshift=0.2em]\ar[r,"g_2"', <-,yshift=-0.2em]  &
+  \mathcal{F}(\mathcal{F}(\mathcal{F}(\mathbf{1}))) \ar[r,-,dashed,yshift=0.2em]\ar[r,dashed,-,yshift=-0.2em]  &
+  \cdots
+\end{tikzcd}}}
+Where the [retraction pairs](dt-0054) #{(f_i, g_i)} are defined by:
+##{
+\begin{array}{lcl}
+(f_0,g_0) & \triangleq & (\lambda x. \bot, \lambda x. \bot)\\
+(f_{i+1},g_{i+1}) & \triangleq & \mathcal{F}(f_i,g_i) \\
+\end{array}
+}}
diff --git a/trees/dt/dt-005C.tree b/trees/dt/dt-005C.tree
new file mode 100644
index 0000000..250eddf
--- /dev/null
+++ b/trees/dt/dt-005C.tree
@@ -0,0 +1,15 @@
+\import{dt-macros}
+\author{liamoc}
+\taxon{Definition}
+\title{#{\omega}-chains of cpos in the category #{\mathbf{Cpo}^\textbf{R}}}
+\p{An [#{\omega}-chain](dt-000W) of [cpos](dt-001D) in the [category #{\mathbf{Cpo}^\textbf{R}}](dt-0058) consists of a family of [cpos](dt-001D) #{\Set{D_i \mid i \in \mathbb{N} }}, together with a family of [retraction pairs](dt-0054) #{ D_i \rpair{f_i}{g_i} D_{i+1}}, shown below:}
+\figure{
+\tex{\usepackage{tikz-cd}}{
+\begin{tikzcd}
+  D_0 \ar[r,"f_0",->,yshift=0.2em]\ar[r,"g_0"', <-,yshift=-0.2em]  &
+  D_1 \ar[r,"f_1",->,yshift=0.2em]\ar[r,"g_1"', <-,yshift=-0.2em]  &
+  D_2 \ar[r,"f_2",->,yshift=0.2em]\ar[r,"g_2"', <-,yshift=-0.2em]  &
+  D_3 \ar[r,-,dashed,yshift=0.2em]\ar[r,dashed,-,yshift=-0.2em]  &
+  \cdots
+\end{tikzcd}
+}}
diff --git a/trees/dt/dt-macros.tree b/trees/dt/dt-macros.tree
index 32c0721..438286f 100644
--- a/trees/dt/dt-macros.tree
+++ b/trees/dt/dt-macros.tree
@@ -1,5 +1,6 @@
 \def\cal[body]{#{\mathcal{\body}}}
 \def\syn[body]{#{\mathsf{\body}}}
+\def\rpair[top][bottom]{#{\xtofrom[\bottom]{\top}}}
 \def\compact[body]{#{\mathsf{K}(\body)}}
 \def\inferrule[top][bottom]{\dfrac{\top}{\bottom}}
 \def\proofblock[body]{\scope{