diff --git a/src/cat/gluing/gluing.tex b/src/cat/gluing/gluing.tex
index e69de29..9dda2e1 100644
--- a/src/cat/gluing/gluing.tex
+++ b/src/cat/gluing/gluing.tex
@@ -0,0 +1,47 @@
+\section{Gluing Lemmas}
+\label{section:gluing}
+
+
+
+\begin{lemma}[Gluing for Functions]
+\label{lemma:glue-function}
+    Let $X, Y$ be sets, $\seq{U_i} \subset 2^X$, and $\seqi{f}$ with $f_i: U_i \to Y$ for all $i \in I$. If:
+    \begin{enumerate}
+        \item[(a)] $\bigcup_{i \in I}U_i = X$.
+        \item[(b)] For each $i, j \in I$, either $U_i \cap U_j = \emptyset$, or $f_i|_{U_i \cap U_j} = f_j|_{U_i \cap U_j}$.
+    \end{enumerate}
+
+    then there exists a unique $f: X \to Y$ such that $f|_{U_i} = f_i$ for all $i \in I$.
+\end{lemma}
+\begin{proof}
+    For each $i \in I$, let $\Gamma_i \subset U_i \times Y$ be the graph of $f_i$. Let $\Gamma = \bigcup_{i \in I}\Gamma_i$, then:
+    \begin{enumerate}
+        \item By assumption (a), $\bracs{x|(x, y) \in \Gamma} = \bigcup_{i \in I}U_i = X$.
+        \item For any $x \in X$, there exists $y \in Y$ with $(x, y) \in \Gamma$, and $i \in I$ such that $(x, y) \in \Gamma_i$. If $(x, y') \in \Gamma_j \subset \Gamma$, then $x \in U_i \cap U_j \ne \emptyset$. By assumption (b), $y = y'$.
+    \end{enumerate}
+
+    Thus $\Gamma$ is the graph of a function $f: X \to Y$ with $f|_{U_i} = f_i$ for all $i \in I$.
+\end{proof}
+
+
+\begin{lemma}[Gluing for Linear Functions]
+\label{lemma:glue-linear}
+    Let $E, F$ be vector spaces over a field $K$, $\fF$ be a family of subspaces of $E$, and $\bracs{T_V}_{V \in \fF}$ with $T_V \in \hom(V; F)$ for all $V \in \fF$. If:
+    \begin{enumerate}
+        \item[(a)] $\bigcup_{V \in \fF}V = E$.
+        \item[(b)] For each $V, W \in \fF$, $T_V|_{V \cap W} = T_W|_{V \cap W}$.
+        \item[(c)] $\fF$ is upward-directed with respect to includion.
+    \end{enumerate}
+
+    then there exists a unique $T \in \hom(E; F)$ such that $T|_{V} = T_V$ for all $V \in \fF$.
+\end{lemma}
+\begin{proof}
+    By (a), (b), and \autoref{lemma:glue-function}, there exists a unique $T: E \to F$ such that $T|_V = T_V$ for all $V \in \fF$.
+
+    Let $x, y \in E$ and $\lambda \in \fF$. By assumption (a), there exists $V_x, V_y \in \fF$ with $x \in V_x$ and $y \in V_y$. By assumption (3), there exists $V \in \fF$ with $V \supset V_x \cup V_y$. Hence
+    \[
+    T(\lambda x + y) = T_V(\lambda x + y) = \lambda T_Vx + T_Vy = \lambda Tx + Ty
+    \]
+
+    and $T \in \hom(E; F)$.
+\end{proof}
\ No newline at end of file
diff --git a/src/cat/gluing/index.tex b/src/cat/gluing/index.tex
index bb34815..de6909d 100644
--- a/src/cat/gluing/index.tex
+++ b/src/cat/gluing/index.tex
@@ -1,46 +1,8 @@
-\chapter{Gluing Lemmas}
+\chapter{Functions}
 \label{chap:gluing}
 
-
-\begin{lemma}[Gluing for Functions]
-\label{lemma:glue-function}
-    Let $X, Y$ be sets, $\seq{U_i} \subset 2^X$, and $\seqi{f}$ with $f_i: U_i \to Y$ for all $i \in I$. If:
-    \begin{enumerate}
-        \item[(a)] $\bigcup_{i \in I}U_i = X$.
-        \item[(b)] For each $i, j \in I$, either $U_i \cap U_j = \emptyset$, or $f_i|_{U_i \cap U_j} = f_j|_{U_i \cap U_j}$.
-    \end{enumerate}
-
-    then there exists a unique $f: X \to Y$ such that $f|_{U_i} = f_i$ for all $i \in I$.
-\end{lemma}
-\begin{proof}
-    For each $i \in I$, let $\Gamma_i \subset U_i \times Y$ be the graph of $f_i$. Let $\Gamma = \bigcup_{i \in I}\Gamma_i$, then:
-    \begin{enumerate}
-        \item By assumption (a), $\bracs{x|(x, y) \in \Gamma} = \bigcup_{i \in I}U_i = X$.
-        \item For any $x \in X$, there exists $y \in Y$ with $(x, y) \in \Gamma$, and $i \in I$ such that $(x, y) \in \Gamma_i$. If $(x, y') \in \Gamma_j \subset \Gamma$, then $x \in U_i \cap U_j \ne \emptyset$. By assumption (b), $y = y'$.
-    \end{enumerate}
-
-    Thus $\Gamma$ is the graph of a function $f: X \to Y$ with $f|_{U_i} = f_i$ for all $i \in I$.
-\end{proof}
+The following chapter contains certain tricks in working with functions in an abstract setting. 
 
 
-\begin{lemma}[Gluing for Linear Functions]
-\label{lemma:glue-linear}
-    Let $E, F$ be vector spaces over a field $K$, $\fF$ be a family of subspaces of $E$, and $\bracs{T_V}_{V \in \fF}$ with $T_V \in \hom(V; F)$ for all $V \in \fF$. If:
-    \begin{enumerate}
-        \item[(a)] $\bigcup_{V \in \fF}V = E$.
-        \item[(b)] For each $V, W \in \fF$, $T_V|_{V \cap W} = T_W|_{V \cap W}$.
-        \item[(c)] $\fF$ is upward-directed with respect to includion.
-    \end{enumerate}
-
-    then there exists a unique $T \in \hom(E; F)$ such that $T|_{V} = T_V$ for all $V \in \fF$.
-\end{lemma}
-\begin{proof}
-    By (a), (b), and \autoref{lemma:glue-function}, there exists a unique $T: E \to F$ such that $T|_V = T_V$ for all $V \in \fF$.
-
-    Let $x, y \in E$ and $\lambda \in \fF$. By assumption (a), there exists $V_x, V_y \in \fF$ with $x \in V_x$ and $y \in V_y$. By assumption (3), there exists $V \in \fF$ with $V \supset V_x \cup V_y$. Hence
-    \[
-    T(\lambda x + y) = T_V(\lambda x + y) = \lambda T_Vx + T_Vy = \lambda Tx + Ty
-    \]
-
-    and $T \in \hom(E; F)$.
-\end{proof}
+\input{./gluing.tex}
+\input{./level.tex}
diff --git a/src/cat/gluing/level.tex b/src/cat/gluing/level.tex
new file mode 100644
index 0000000..bfe8877
--- /dev/null
+++ b/src/cat/gluing/level.tex
@@ -0,0 +1,42 @@
+\section{Preimages}
+\label{section:preimage}
+
+\begin{definition}[Preimage Function]
+\label{definition:preimage-function}
+    Let $X, Y$ be sets and $P: 2^Y \to 2^X$, then $P$ is a \textbf{preimage function} if
+    \begin{enumerate}[label=(PF\arabic*)]
+        \item $P(\emptyset) = \emptyset$. 
+        \item For each $\mathcal{S} \subset 2^Y$, $\bigcup_{S \in \mathcal{S}}P(S) = P\paren{\bigcup_{S \in \mathcal{S}}S}$. 
+        \item For each $\mathcal{S} \subset 2^Y$, $\bigcap_{S \in \mathcal{S}}P(S) = P\paren{\bigcap_{S \in \mathcal{S}}}$. 
+    \end{enumerate}
+
+    and $P$ is \textbf{total} if
+    \begin{enumerate}
+        \item[(T)] $P(Y) = X$. 
+    \end{enumerate}
+\end{definition}
+
+\begin{proposition}
+\label{proposition:preimage-gymnastics}
+    Let $X$ and $Y$ be sets, then:
+    \begin{enumerate}
+        \item For any $f: X \to Y$, the mapping $S \mapsto f^{-1}(S)$ is a total preimage function.
+        \item For any total preimage function $P: 2^Y \to 2^X$, there exists a unique $f: X \to Y$ such that $P(S) = f^{-1}(S)$ for all $S \in 2^Y$. 
+    \end{enumerate}
+\end{proposition}
+\begin{proof}
+    (2): Let $x, y \in Y$ with $x \ne y$, then by (PF1) and (PF3), 
+    \[
+    P(\bracs{x}) \cap P(\bracs{y}) = P(\bracs{x} \cap \bracs{y}) = P(\emptyset) = \emptyset
+    \]
+
+    By (T) and (PF2), $X = P(Y) = P\paren{\bigcup_{y \in Y}\bracs{y}} = \bigcup_{y \in Y}P(\bracs{y})$. Therefore $X = \bigsqcup_{y \in Y}P(\bracs{y})$. 
+
+    Therefore for each $x \in X$, there exists a unique $f(x) \in Y$ such that $x \in P(f(x))$. The association $x \mapsto f(x)$ then is the unique desired function. 
+\end{proof}
+
+
+
+
+
+
diff --git a/src/topology/metric/metric.tex b/src/topology/metric/metric.tex
index f9c46fa..03dd888 100644
--- a/src/topology/metric/metric.tex
+++ b/src/topology/metric/metric.tex
@@ -68,6 +68,12 @@
     (2) $\Rightarrow$ (3): Since $\fF$ is Cauchy, there exists $\seq{E_n} \subset \fF$ such that for each $n \in \natp$, $E_n \supset E_{n+1}$ and $\sup_{y, z \in E_n}d(y, z) \le 1/n$. For each $n \in \natp$, let $x_n \in E_n$, then there exists a subsequence $\seq{n_k}$ and $x \in X$ such that $x = \limv{n}x_n$. In which case, $x \in \bigcap_{n \in \natp}\overline{E_n}$. For each $n \in \natp$, $\sup_{y, z\in E_n}d(y, z) \le 1/n$, so $B_X(x, 2/n) \supset E_n$. Therefore $\fF \to x$. 
 \end{proof}
 
+\begin{definition}[Polish Space]
+\label{definition:polish-space}
+    Let $X$ be a topological space, then $X$ is \textbf{Polish} if it is completely metrisable and second countable. 
+\end{definition}
+
+
 
 \begin{theorem}[Banach's Fixed Point Theorem]
 \label{theorem:banach-fixed-point}
@@ -98,3 +104,6 @@
     \]
 \end{proof}
 
+
+
+