begin discussion section

paper-new/discussion.tex

+\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

paper-new/paper.tex

@@ -144,6 +144,8 @@
 %\input{denotational-model}
 \input{concrete-model}
 
+\input{discussion}
+
 % \section{Discussion}\label{sec:discussion}
 
 % \subsection{Synthetic Ordering}