diff --git a/draft/draft.tex b/draft/draft.tex
index 5260171..e130c1c 100644
--- a/draft/draft.tex
+++ b/draft/draft.tex
@@ -1849,15 +1849,17 @@ Because assuming we have $\sigma$, for every given $\sigma'$ we can define a $\d
 		\arrow["{{\mathcal{P}p_2}_\subseteq}"', from=3-2, to=3-3]
 	\end{tikzcd}
 \end{equation*}
-$\delta$ is defined as the following:
+To define $\delta$, we define $c\c(\mathcal{P}R^\dagger)\to((\mathcal{P}R^\dagger)\times R)+(\mathcal{P}R)^\dagger$ and $u\c((\mathcal{P}R^\dagger)\times R)+(\mathcal{P}R)^\dagger\to\subseteq;(\mathcal{P}R)^\dagger;\subseteq$ and then we define $\delta=u\comp c$. Here are the definitions for $c$ and $u$:
 \begin{gather*}
-	\delta(w)=
+	c(w)=
 	\begin{cases} 
-		(\alpha(x_1),\alpha(x_2)) & \exists x_1,x_2, \sigma'(x_1,x_2)=w  \\
-		w & \mathsf{o.w}  
-	\end{cases}
+		\inl(w,(x_1,x_2)) & \exists x_1,x_2, \sigma'(x_1,x_2)=w  \\
+		\inr w & \mathsf{o.w}  
+	\end{cases}\\
+	u(\inl w,(x_1,x_2))=(\alpha(x_1),\alpha(x_2))\\
+	u(\inr w)=w
 \end{gather*}
-Now, we want to prove an abstraction of this statement. First, we need to spell out what $\appr;(FR)^\dagger;\appr$ is. We define relation compositions with pullbacks, so we have the following diagram:
+Now, we want to prove a more abstract version of this statement. First, we need to spell out what $\appr;(FR)^\dagger;\appr$ is. We define relation compositions with pullbacks, so we have the following diagram:
 \begin{equation*}
 	\begin{tikzcd}[ampersand replacement=\&]
 		{\appr;(FR)^\dagger;\appr} \& {\appr;(FR)^\dagger} \& {\appr} \& {FX} \\
@@ -1870,15 +1872,15 @@ Now, we want to prove an abstraction of this statement. First, we need to spell
 		\arrow["{{{{{{{\varphi_1}}}}}}}", from=1-2, to=1-3]
 		\arrow["{{{{{{{\varphi_2}}}}}}}", from=1-2, to=2-2]
 		\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-2, to=2-3]
-		\arrow["{{{{{{{i_1}}}}}}}", from=1-3, to=1-4]
-		\arrow["{{{{{{{i_2}}}}}}}", from=1-3, to=2-3]
+		\arrow["{{{{{{{q_1}}}}}}}", from=1-3, to=1-4]
+		\arrow["{{{{{{{q_2}}}}}}}", from=1-3, to=2-3]
 		\arrow["{{{{{{{Fp_1^\dagger}}}}}}}", from=2-2, to=2-3]
 		\arrow["{{{{{{{Fp_2^\dagger}}}}}}}"', from=2-2, to=3-2]
-		\arrow["{{{{{{{i_1}}}}}}}"', from=3-1, to=3-2]
-		\arrow["{{{{{{{i_2}}}}}}}"', from=3-1, to=4-1]
+		\arrow["{{{{{{{q_1}}}}}}}"', from=3-1, to=3-2]
+		\arrow["{{{{{{{q_2}}}}}}}"', from=3-1, to=4-1]
 	\end{tikzcd}
 \end{equation*}
-Additionally, we make the abbreviations that ${Fp_1}_\appr=i_1\comp\varphi_1\comp\pi_1$ and ${Fp_2}_\appr=i_2\comp\pi_2$.
+Additionally, we make the abbreviations that ${Fp_1}_\appr=q_1\comp\varphi_1\comp\pi_1$ and ${Fp_2}_\appr=q_2\comp\pi_2$.
 \begin{prop}
 	Assuming we have a morphism $\sigma'\c R\to(FR)^\dagger$ then exists $\delta\c(FR)^\dagger\to(\appr;(FR)^\dagger;\appr)^\dagger$ such that $\sigma=\delta\comp\sigma'$ that commutes in the following diagram:
 	\begin{equation*}