From 3d79ec6cd105c617bb889ba0ff94087d753204a3 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 11 Mar 2016 21:57:37 +0100
Subject: [PATCH] docs: type-level later

---
 docs/algebra.tex       |  1 +
 docs/constructions.tex | 11 +++++++++++
 docs/iris.sty          |  1 +
 docs/logic.tex         |  4 ++--
 4 files changed, 15 insertions(+), 2 deletions(-)

diff --git a/docs/algebra.tex b/docs/algebra.tex
index 4b0058e62..0c12cef58 100644
--- a/docs/algebra.tex
+++ b/docs/algebra.tex
@@ -40,6 +40,7 @@ Note that $\COFEs$ is cartesian closed.
   A (bi)functor $F : \COFEs \to \COFEs$ is called \emph{locally non-expansive} if its action $F_1$ on arrows is itself a non-expansive map.
   Similarly, $F$ is called \emph{locally contractive} if $F_1$ is a contractive map.
 \end{defn}
+Note that the composition of non-expansive (bi)functors is non-expansive, and the composition of a non-expansive and a contractive (bi)functor is contractive.
 
 \subsection{RA}
 
diff --git a/docs/constructions.tex b/docs/constructions.tex
index 6f8ef788e..91b966859 100644
--- a/docs/constructions.tex
+++ b/docs/constructions.tex
@@ -1,5 +1,16 @@
 % !TEX root = ./appendix.tex
+\section{COFE constructions}
 
+\subsection{Next (type-level later)}
+
+Given a COFE $\cofe$, we define $\latert\cofe$ as follows:
+\begin{align*}
+  \latert\cofe \eqdef{}& \latertinj(\cofe) \\
+  \latertinj(x) \nequiv{n} \latertinj(y) \eqdef{}& n = 0 \lor x \nequiv{n-1} y
+\end{align*}
+$\latert(-)$ is a locally \emph{contractive} bifunctor from $\COFEs$ to $\COFEs$.
+
+\clearpage
 \section{CMRA constructions}
 
 \subsection{Product}
diff --git a/docs/iris.sty b/docs/iris.sty
index 447207c1a..065d62e2b 100644
--- a/docs/iris.sty
+++ b/docs/iris.sty
@@ -101,6 +101,7 @@
 \newcommand{\nequivset}[2]{\ensuremath{\mathrel{\stackrel{#1}{=}_{#2}}}}
 \newcommand{\nequivB}[1]{\ensuremath{\mathrel{\stackrel{#1}{\equiv}}}}
 \newcommand{\latert}{\mathord{\blacktriangleright}}
+\newcommand{\latertinj}{\textlog{next}}
 
 \newcommand{\Sem}[1]{\llbracket #1 \rrbracket}
 
diff --git a/docs/logic.tex b/docs/logic.tex
index 2f77240a2..3642b42f1 100644
--- a/docs/logic.tex
+++ b/docs/logic.tex
@@ -41,7 +41,7 @@ It does not matter whether they fork off an arbitrary expression.
   \end{enumerate}
 \end{defn}
 
-\subsection{The concurrent language}
+\subsection{Concurrent language}
 
 For any language $\Lang$, we define the corresponding thread-pool semantics.
 
@@ -64,7 +64,7 @@ For any language $\Lang$, we define the corresponding thread-pool semantics.
 \end{mathpar}
 
 \clearpage
-\section{The logic}
+\section{Logic}
 
 To instantiate Iris, you need to define the following parameters:
 \begin{itemize}
-- 
GitLab