fredefox/cat
1
0
Fork 0
Code Issues Pull requests Releases Wiki Activity

Do not use colon directly for typing judgments

Browse source
This commit is contained in:
Frederik Hanghøj Iversen 2018-05-08 02:01:17 +02:00
parent e18730e0e5
commit 6a3e7390d7
3 changed files with 8 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
doc/cubical.tex
View file

@ -47,7 +47,7 @@ heterogeneous paths respectively.
In Cubical Agda judgmental equality is encapsulated with the type: 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 $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: 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$ For some proposition $P \tp A \to \MCU$. If we want to prove $t_0 \equiv t_1$

2
doc/implementation.tex
View file

@ -85,7 +85,7 @@ Moreover, due to substitution for paths we can construct an isomorphism from
\emph{any} path: \emph{any} path:
% %
\begin{equation} \begin{equation}
\var{idToIso} : A ≡ B → A ≊ B \var{idToIso} \tp A ≡ B → A ≊ B
\end{equation} \end{equation}
% %
The univalence criterion for categories states that this map must be an The univalence criterion for categories states that this map must be an

10
doc/introduction.tex
View file

@ -21,10 +21,10 @@ Consider the functions:
\begin{multicols}{2} \begin{multicols}{2}
\noindent \noindent
\begin{equation*} \begin{equation*}
f \defeq (n : \bN) \mapsto (0 + n : \bN) f \defeq (n \tp \bN) \mapsto (0 + n \tp \bN)
\end{equation*} \end{equation*}
\begin{equation*} \begin{equation*}
g \defeq (n : \bN) \mapsto (n + 0 : \bN) g \defeq (n \tp \bN) \mapsto (n + 0 \tp \bN)
\end{equation*} \end{equation*}
\end{multicols} \end{multicols}
% %
@ -35,7 +35,7 @@ which is:
% %
\newcommand{\suc}[1]{\mathit{suc}\ #1} \newcommand{\suc}[1]{\mathit{suc}\ #1}
\begin{align*} \begin{align*}
+ & : \bN \to \bN \to \bN \\ + & \tp \bN \to \bN \to \bN \\
n + 0 & \defeq n \\ n + 0 & \defeq n \\
n + (\suc{m}) & \defeq \suc{(n + m)} n + (\suc{m}) & \defeq \suc{(n + m)}
\end{align*} \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 these as axioms. This approach, however, has other shortcomings, e.g.; you lose
\nomen{canonicity} (\TODO{Pageno!} \cite{huber-2016}). Canonicity means that any \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 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 $\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 terms in the language can get ``stuck'' -- meaning that they do not reduce to a
canonical form. canonical form.
@ -195,7 +195,7 @@ Name & Agda & Notation \\
\nomen{Type} & \texttt{Set} & $\Type$ \\ \nomen{Type} & \texttt{Set} & $\Type$ \\
\nomen{Set} & \texttt{Σ Set IsSet} & $\Set$ \\ \nomen{Set} & \texttt{Σ Set IsSet} & $\Set$ \\
Function, morphism, map & \texttt{A → B} & $A → B$ \\ 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{Arrow} & \texttt{Arrow A B} & $\Arrow\ A\ B$ \\
\nomen{Object} & \texttt{C.Object} & $̱ℂ.Object$ \\ \nomen{Object} & \texttt{C.Object} & $̱ℂ.Object$ \\
Definition & \texttt{=} & $̱\defeq$ \\ Definition & \texttt{=} & $̱\defeq$ \\