From 1fe7e8e86d1568afda6606c8c2aa10c54691291f Mon Sep 17 00:00:00 2001
From: Eric Giovannini <ecg19@seas.upenn.edu>
Date: Sat, 13 Jan 2024 16:15:10 -0500
Subject: [PATCH] remove section on topos of trees model
---
paper-new/technical-background.tex | 144 -----------------------------
1 file changed, 144 deletions(-)
diff --git a/paper-new/technical-background.tex b/paper-new/technical-background.tex
index 869fbe2..f189287 100644
--- a/paper-new/technical-background.tex
+++ b/paper-new/technical-background.tex
@@ -154,147 +154,3 @@ Guarded Cubical Agda \cite{veltri-vezzosi2020}, an implementation of Clocked Cub
% TODO axioms (clock irrelevance, tick irrelevance)?
-
-
-\subsubsection{The Topos of Trees Model}
-
-The topos of trees model provides a useful intuition for reasoning in SGDT
-\cite{birkedal-mogelberg-schwinghammer-stovring2011}.
-This section presupposes knowledge of category theory and can be safely skipped without
-disrupting the continuity.
-
-The topos of trees $\calS$ is the presheaf category $\Set^{\omega^o}$.
-%
-We assume a universe $\calU$ of types, with encodings for operations such
-as sum types (written as $\widehat{+}$). There is also an operator
-$\laterhat \colon \later \calU \to \calU$ such that
-$\El(\laterhat(\nxt A)) =\,\, \later \El(A)$, where $\El$ is the type corresponding
-to the code $A$.
-
-An object $X$ is a family $\{X_i\}$ of sets indexed by natural numbers,
-along with restriction maps $r^X_i \colon X_{i+1} \to X_i$ (see Figure \ref{fig:topos-of-trees-object}).
-These should be thought of as ``sets changing over time", where $X_i$ is the view of the set if we have $i+1$
-time steps to reason about it.
-We can also think of an ongoing computation, with $X_i$ representing the potential results of the computation
-after it has run for $i+1$ steps.
-
-\begin{figure}
- % https://q.uiver.app/?q=WzAsNSxbMiwwLCJYXzIiXSxbMCwwLCJYXzAiXSxbMSwwLCJYXzEiXSxbMywwLCJYXzMiXSxbNCwwLCJcXGRvdHMiXSxbMiwxLCJyXlhfMCIsMl0sWzAsMiwicl5YXzEiLDJdLFszLDAsInJeWF8yIiwyXSxbNCwzLCJyXlhfMyIsMl1d
-\[\begin{tikzcd}[ampersand replacement=\&]
- {X_0} \& {X_1} \& {X_2} \& {X_3} \& \dots
- \arrow["{r^X_0}"', from=1-2, to=1-1]
- \arrow["{r^X_1}"', from=1-3, to=1-2]
- \arrow["{r^X_2}"', from=1-4, to=1-3]
- \arrow["{r^X_3}"', from=1-5, to=1-4]
-\end{tikzcd}\]
- \caption{An example of an object in the topos of trees.}
- \label{fig:topos-of-trees-object}
-\end{figure}
-
-A morphism from $\{X_i\}$ to $\{Y_i\}$ is a family of functions $f_i \colon X_i \to Y_i$
-that commute with the restriction maps in the obvious way, that is,
-$f_i \circ r^X_i = r^Y_i \circ f_{i+1}$ (see Figure \ref{fig:topos-of-trees-morphism}).
-
-\begin{figure}
-% https://q.uiver.app/?q=WzAsMTAsWzIsMCwiWF8yIl0sWzAsMCwiWF8wIl0sWzEsMCwiWF8xIl0sWzMsMCwiWF8zIl0sWzQsMCwiXFxkb3RzIl0sWzAsMSwiWV8wIl0sWzEsMSwiWV8xIl0sWzIsMSwiWV8yIl0sWzMsMSwiWV8zIl0sWzQsMSwiXFxkb3RzIl0sWzIsMSwicl5YXzAiLDJdLFswLDIsInJeWF8xIiwyXSxbMywwLCJyXlhfMiIsMl0sWzQsMywicl5YXzMiLDJdLFs2LDUsInJeWV8wIiwyXSxbNyw2LCJyXllfMSIsMl0sWzgsNywicl5ZXzIiLDJdLFs5LDgsInJeWV8zIiwyXSxbMSw1LCJmXzAiLDJdLFsyLDYsImZfMSIsMl0sWzAsNywiZl8yIiwyXSxbMyw4LCJmXzMiLDJdXQ==
-\[\begin{tikzcd}[ampersand replacement=\&]
- {X_0} \& {X_1} \& {X_2} \& {X_3} \& \dots \\
- {Y_0} \& {Y_1} \& {Y_2} \& {Y_3} \& \dots
- \arrow["{r^X_0}"', from=1-2, to=1-1]
- \arrow["{r^X_1}"', from=1-3, to=1-2]
- \arrow["{r^X_2}"', from=1-4, to=1-3]
- \arrow["{r^X_3}"', from=1-5, to=1-4]
- \arrow["{r^Y_0}"', from=2-2, to=2-1]
- \arrow["{r^Y_1}"', from=2-3, to=2-2]
- \arrow["{r^Y_2}"', from=2-4, to=2-3]
- \arrow["{r^Y_3}"', from=2-5, to=2-4]
- \arrow["{f_0}"', from=1-1, to=2-1]
- \arrow["{f_1}"', from=1-2, to=2-2]
- \arrow["{f_2}"', from=1-3, to=2-3]
- \arrow["{f_3}"', from=1-4, to=2-4]
-\end{tikzcd}\]
- \caption{An example of a morphism in the topos of trees.}
- \label{fig:topos-of-trees-morphism}
-\end{figure}
-
-
-The type operator $\later$ is defined on an object $X$ by
-$(\later X)_0 = 1$ and $(\later X)_{i+1} = X_i$.
-The restriction maps are given by $r^\later_0 =\, !$, where $!$ is the
-unique map into $1$, and $r^\later_{i+1} = r^X_i$.
-The morphism $\nxt^X \colon X \to \later X$ is defined pointwise by
-$\nxt^X_0 =\, !$, and $\nxt^X_{i+1} = r^X_i$. It is easily checked that
-this satisfies the commutativity conditions required of a morphism in $\calS$.
-%
-Given a morphism $f \colon \later X \to X$, i.e., a family of functions
-$f_i \colon (\later X)_i \to X_i$ that commute with the restrictions in the appropriate way,
-we define $\fix(f) \colon 1 \to X$ pointwise
-by $\fix(f)_i = f_{i} \circ \dots \circ f_0$.
-This can be visualized as a diagram in the category of sets as shown in
-Figure \ref{fig:topos-of-trees-fix}.
-% Observe that the fixpoint is a \emph{global element} in the topos of trees.
-% Global elements allow us to view the entire computation on a global level.
-
-
-% https://q.uiver.app/?q=WzAsOCxbMSwwLCJYXzAiXSxbMiwwLCJYXzEiXSxbMywwLCJYXzIiXSxbMCwwLCIxIl0sWzAsMSwiWF8wIl0sWzEsMSwiWF8xIl0sWzIsMSwiWF8yIl0sWzMsMSwiWF8zIl0sWzMsNCwiZl8wIl0sWzAsNSwiZl8xIl0sWzEsNiwiZl8yIl0sWzIsNywiZl8zIl0sWzAsMywiISIsMl0sWzEsMCwicl5YXzAiLDJdLFsyLDEsInJeWF8xIiwyXSxbNSw0LCJyXlhfMCJdLFs2LDUsInJeWF8xIl0sWzcsNiwicl5YXzIiXV0=
-% \[\begin{tikzcd}[ampersand replacement=\&]
-% 1 \& {X_0} \& {X_1} \& {X_2} \\
-% {X_0} \& {X_1} \& {X_2} \& {X_3}
-% \arrow["{f_0}", from=1-1, to=2-1]
-% \arrow["{f_1}", from=1-2, to=2-2]
-% \arrow["{f_2}", from=1-3, to=2-3]
-% \arrow["{f_3}", from=1-4, to=2-4]
-% \arrow["{!}"', from=1-2, to=1-1]
-% \arrow["{r^X_0}"', from=1-3, to=1-2]
-% \arrow["{r^X_1}"', from=1-4, to=1-3]
-% \arrow["{r^X_0}", from=2-2, to=2-1]
-% \arrow["{r^X_1}", from=2-3, to=2-2]
-% \arrow["{r^X_2}", from=2-4, to=2-3]
-% \end{tikzcd}\]
-
-% \begin{figure}
-% % https://q.uiver.app/?q=WzAsMTksWzEsMiwiWF8wIl0sWzIsMywiWF8xIl0sWzMsMSwiMSJdLFswLDEsIjEiXSxbMCwyLCJYXzAiXSxbMSwzLCJYXzEiXSxbMSwxLCIxIl0sWzIsMSwiMSJdLFsyLDIsIlhfMCJdLFsyLDQsIlhfMiJdLFszLDIsIlhfMCJdLFszLDMsIlhfMSJdLFszLDQsIlhfMiJdLFszLDUsIlhfMyJdLFs0LDIsIlxcY2RvdHMiXSxbMCwwLCJcXGZpeChmKV8wIl0sWzEsMCwiXFxmaXgoZilfMSJdLFsyLDAsIlxcZml4KGYpXzIiXSxbMywwLCJcXGZpeChmKV8zIl0sWzMsNCwiZl8wIl0sWzAsNSwiZl8xIl0sWzYsMCwiZl8wIl0sWzcsOCwiZl8wIl0sWzgsMSwiZl8xIl0sWzEsOSwiZl8yIl0sWzIsMTAsImZfMCJdLFsxMCwxMSwiZl8xIl0sWzExLDEyLCJmXzIiXSxbMTIsMTMsImZfMyJdXQ==
-% \[\begin{tikzcd}[ampersand replacement=\&]
-% {\fix(f)_0} \& {\fix(f)_1} \& {\fix(f)_2} \& {\fix(f)_3} \\
-% 1 \& 1 \& 1 \& 1 \\
-% {X_0} \& {X_0} \& {X_0} \& {X_0} \& \cdots \\
-% \& {X_1} \& {X_1} \& {X_1} \\
-% \&\& {X_2} \& {X_2} \\
-% \&\&\& {X_3}
-% \arrow["{f_0}", from=2-1, to=3-1]
-% \arrow["{f_1}", from=3-2, to=4-2]
-% \arrow["{f_0}", from=2-2, to=3-2]
-% \arrow["{f_0}", from=2-3, to=3-3]
-% \arrow["{f_1}", from=3-3, to=4-3]
-% \arrow["{f_2}", from=4-3, to=5-3]
-% \arrow["{f_0}", from=2-4, to=3-4]
-% \arrow["{f_1}", from=3-4, to=4-4]
-% \arrow["{f_2}", from=4-4, to=5-4]
-% \arrow["{f_3}", from=5-4, to=6-4]
-% \end{tikzcd}\]
-% \caption{The first few approximations to the guarded fixpoint of $f$.}
-% \label{fig:topos-of-trees-fix-approx}
-% \end{figure}
-
-
-\begin{figure}
- % https://q.uiver.app/?q=WzAsNixbMywwLCIxIl0sWzAsMiwiWF8wIl0sWzIsMiwiWF8xIl0sWzQsMiwiWF8yIl0sWzYsMiwiWF8zIl0sWzgsMiwiXFxkb3RzIl0sWzIsMSwicl5YXzAiXSxbNCwzLCJyXlhfMiJdLFswLDEsIlxcZml4KGYpXzAiLDFdLFswLDIsIlxcZml4KGYpXzEiLDFdLFswLDMsIlxcZml4KGYpXzIiLDFdLFswLDQsIlxcZml4KGYpXzMiLDFdLFswLDUsIlxcY2RvdHMiLDMseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJub25lIn0sImhlYWQiOnsibmFtZSI6Im5vbmUifX19XSxbMywyLCJyXlhfMSJdLFs1LDQsInJeWF8zIl1d
- \[\begin{tikzcd}[ampersand replacement=\&,column sep=2.25em]
- \&\&\& 1 \\
- \\
- {X_0} \&\& {X_1} \&\& {X_2} \&\& {X_3} \&\& \dots
- \arrow["{r^X_0}", from=3-3, to=3-1]
- \arrow["{r^X_2}", from=3-7, to=3-5]
- \arrow["{\fix(f)_0}"{description}, from=1-4, to=3-1]
- \arrow["{\fix(f)_1}"{description}, from=1-4, to=3-3]
- \arrow["{\fix(f)_2}"{description}, from=1-4, to=3-5]
- \arrow["{\fix(f)_3}"{description}, from=1-4, to=3-7]
- \arrow["\cdots"{marking}, draw=none, from=1-4, to=3-9]
- \arrow["{r^X_1}", from=3-5, to=3-3]
- \arrow["{r^X_3}", from=3-9, to=3-7]
- \end{tikzcd}\]
- \caption{The guarded fixpoint of $f$.}
- \label{fig:topos-of-trees-fix}
-\end{figure}
-
-% TODO global elements?
--
GitLab