From bcac2b02f56d26c35b81c55e3c9cfd88fd61d872 Mon Sep 17 00:00:00 2001
From: Eric Giovannini <ecg19@seas.upenn.edu>
Date: Thu, 18 Jan 2024 17:59:44 -0500
Subject: [PATCH] begin discussion section

---
 paper-new/discussion.tex | 26 ++++++++++++++++++++++++++
 paper-new/paper.tex      |  2 ++
 2 files changed, 28 insertions(+)
 create mode 100644 paper-new/discussion.tex

diff --git a/paper-new/discussion.tex b/paper-new/discussion.tex
new file mode 100644
index 0000000..3e392fe
--- /dev/null
+++ b/paper-new/discussion.tex
@@ -0,0 +1,26 @@
+\section{Discussion}
+
+\subsection{Related Work}
+% Discuss Joey Eremondi's thesis on gradual dependent types
+
+\subsection{Mechanization}
+% Discuss Guarded Cubical Agda and mechanization efforts
+
+\subsection{Benefits and Drawbacks of the Synthetic Approach}
+
+\subsection{Synthetic Ordering}
+
+While the use of synthetic guarded domain theory allows us to very
+conveniently work with non-well-founded recursive constructions while
+abstracting away the precise details of step-indexing, we do work with
+the error ordering in a mostly analytic fashion in that gradual types
+are interpreted as sets equipped with an ordering relation, and all
+terms must be proven to be monotone.
+%
+It is possible that a combination of synthetic guarded domain theory
+with \emph{directed} type theory would allow for an a synthetic
+treatment of the error ordering as well.
+
+\subsection{Future Work}
+
+% Cite GrEff paper
\ No newline at end of file
diff --git a/paper-new/paper.tex b/paper-new/paper.tex
index f499375..2083da0 100644
--- a/paper-new/paper.tex
+++ b/paper-new/paper.tex
@@ -144,6 +144,8 @@
 %\input{denotational-model}
 \input{concrete-model}
 
+\input{discussion}
+
 % \section{Discussion}\label{sec:discussion}
 
 % \subsection{Synthetic Ordering}
-- 
GitLab