From dae6e202d9ab066e919b3825ec8654a82fbdfde9 Mon Sep 17 00:00:00 2001
From: Eric Giovannini <ecg19@seas.upenn.edu>
Date: Thu, 18 Jan 2024 17:53:52 -0500
Subject: [PATCH] changes to technical background
---
paper-new/technical-background.tex | 9 ++++++---
1 file changed, 6 insertions(+), 3 deletions(-)
diff --git a/paper-new/technical-background.tex b/paper-new/technical-background.tex
index f189287..9268cf3 100644
--- a/paper-new/technical-background.tex
+++ b/paper-new/technical-background.tex
@@ -85,7 +85,7 @@
% Synthetic guarded domain theory allows the resulting logical relation to look almost
% identical to a typical, non-step-indexed logical relation.
-\subsection{Synthetic Guarded Domain Theory}
+\subsection{Synthetic Guarded Domain Theory}\label{sec:sgdt}
One way to avoid the tedious reasoning associated with step-indexing is to work
axiomatically inside of a logical system that can reason about non-well-founded recursive
constructions while abstracting away the specific details of step-indexing required
@@ -126,6 +126,8 @@ If we only ever had one clock, then we would not need to bother defining this no
However, the notion of \emph{clock quantification} is crucial for encoding coinductive types using guarded
recursion, an idea first introduced by Atkey and McBride \cite{atkey-mcbride2013}.
+Most of the developments in this paper will take place in the context of a single clock $k$,
+but in Section \ref{TODO}, we will need to make use of clock quantification.
% Clocked Cubical Type Theory
\subsubsection{Ticked Cubical Type Theory}
@@ -149,8 +151,9 @@ a term $M[t'] : A[t'/t]$. We will also write tick application as $M_t$.
Conversely, if in a context $\Gamma, t : \tick\, k$ we have that $M$ has type $A$,
then in context $\Gamma$ we have $\lambda t.M$ has type $\later A$. % TODO dependent version?
-The statements in this paper have been formalized in a variant of Agda called
-Guarded Cubical Agda \cite{veltri-vezzosi2020}, an implementation of Clocked Cubical Type Theory.
+% TODO mention Agda implementation of Clocked Cubical Type Theory?
+%The statements in this paper have been formalized in a variant of Agda called
+%Guarded Cubical Agda \cite{veltri-vezzosi2020}, an implementation of Clocked Cubical Type Theory.
% TODO axioms (clock irrelevance, tick irrelevance)?
--
GitLab