From 6a3e7390d7a4ff26bb856d67a8167b7d9e17f649 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Tue, 8 May 2018 02:01:17 +0200
Subject: [PATCH] Do not use colon directly for typing judgments

---
 doc/cubical.tex        |  4 ++--
 doc/implementation.tex |  2 +-
 doc/introduction.tex   | 10 +++++-----
 3 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/doc/cubical.tex b/doc/cubical.tex
index 96a67ef..d25054d 100644
--- a/doc/cubical.tex
+++ b/doc/cubical.tex
@@ -47,7 +47,7 @@ heterogeneous paths respectively.
 In Cubical Agda judgmental equality is encapsulated with the type:
 %
 $$
-\Path \tp (P : I → \MCU) → P\ 0 → P\ 1 → \MCU
+\Path \tp (P \tp I → \MCU) → P\ 0 → P\ 1 → \MCU
 $$
 %
 $I$ is a special data-type (\TODO{that also has special computational properties
@@ -244,7 +244,7 @@ $\lemPropF$ can be used to boil this complexity down to showing that the
 dependent parts of the type are mere propositions. For instance, saw we have a type:
 %
 $$
-T \defeq \sum_{a : A} P\ a
+T \defeq \sum_{a \tp A} P\ a
 $$
 %
 For some proposition $P \tp A \to \MCU$. If we want to prove $t_0 \equiv t_1$
diff --git a/doc/implementation.tex b/doc/implementation.tex
index a5ae42b..c5f01f7 100644
--- a/doc/implementation.tex
+++ b/doc/implementation.tex
@@ -85,7 +85,7 @@ Moreover, due to substitution for paths we can construct an isomorphism from
 \emph{any} path:
 %
 \begin{equation}
-\var{idToIso} : A ≡ B → A ≊ B
+\var{idToIso} \tp A ≡ B → A ≊ B
 \end{equation}
 %
 The univalence criterion for categories states that this map must be an
diff --git a/doc/introduction.tex b/doc/introduction.tex
index 231097c..a8c19b5 100644
--- a/doc/introduction.tex
+++ b/doc/introduction.tex
@@ -21,10 +21,10 @@ Consider the functions:
 \begin{multicols}{2}
   \noindent
   \begin{equation*}
-    f \defeq (n : \bN) \mapsto (0 + n : \bN)
+    f \defeq (n \tp \bN) \mapsto (0 + n \tp \bN)
   \end{equation*}
   \begin{equation*}
-    g \defeq (n : \bN) \mapsto (n + 0 : \bN)
+    g \defeq (n \tp \bN) \mapsto (n + 0 \tp \bN)
   \end{equation*}
 \end{multicols}
 %
@@ -35,7 +35,7 @@ which is:
 %
 \newcommand{\suc}[1]{\mathit{suc}\ #1}
 \begin{align*}
-  +           & : \bN \to \bN \to \bN      \\
+  +           & \tp \bN \to \bN \to \bN      \\
   n + 0       & \defeq n                   \\
   n + (\suc{m}) & \defeq \suc{(n + m)}
 \end{align*}
@@ -154,7 +154,7 @@ still have univalence and functional extensionality. One option is to postulate
 these as axioms. This approach, however, has other shortcomings, e.g.; you lose
 \nomen{canonicity} (\TODO{Pageno!} \cite{huber-2016}). Canonicity means that any
 well-typed term evaluates to a \emph{canonical} form. For example for a closed
-term $e : \bN$ it will be the case that $e$ reduces to $n$ applications of
+term $e \tp \bN$ it will be the case that $e$ reduces to $n$ applications of
 $\mathit{suc}$ to $0$ for some $n$; $e = \mathit{suc}^n\ 0$. Without canonicity
 terms in the language can get ``stuck'' -- meaning that they do not reduce to a
 canonical form.
@@ -195,7 +195,7 @@ Name & Agda & Notation \\
 \nomen{Type}            & \texttt{Set}         & $\Type$            \\
 \nomen{Set}             & \texttt{Σ Set IsSet} & $\Set$             \\
 Function, morphism, map & \texttt{A → B}       & $A → B$            \\
-Dependent- ditto        & \texttt{(a : A) → B} & $∏_{a \tp A} B$  \\
+Dependent- ditto        & \texttt{(a \tp A) → B} & $∏_{a \tp A} B$  \\
 \nomen{Arrow}           & \texttt{Arrow A B}   & $\Arrow\ A\ B$     \\
 \nomen{Object}          & \texttt{C.Object}    & $̱ℂ.Object$     \\
 Definition              & \texttt{=}           & $̱\defeq$       \\