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

Add additional example of pathJ

Browse source
This commit is contained in:
Frederik Hanghøj Iversen 2018-05-11 13:07:47 +02:00
parent 058f3c15a8
commit 30cf0bb765
2 changed files with 38 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

38
doc/cubical.tex
View file

@ -288,7 +288,7 @@ The proof will be by induction on $p$ and will be based at $a$. That is, $D$
will be the family:
%
\begin{align*}
D & \tp \prod_{b' \tp A} \prod_{p \tp a ≡ b'ma} \MCU \\
D & \tp \prod_{b' \tp A} \prod_{p \tp a ≡ b'} \MCU \\
D\ b'\ p' & \defeq \var{sym}\ (\var{sym}\ p') ≡ p'
\end{align*}
%
@ -303,11 +303,45 @@ The reason $\refl$ proves this is that $\var{sym}\ \refl = \refl$ holds
definitionally. In summary \ref{eq:sym-invol} is inhabited by the term:
%
\begin{align*}
\pathJ\ (λ\ b'\ p' → \var{sym}\ (\var{sym}\ p') ≡ p')\ \var{refl}\ b\ p
\pathJ\ D\ d\ b\ p
\tp
\var{sym}\ (\var{sym}\ p) ≡ p
\end{align*}
%
Another application of $\pathJ$ is for proving associativity of $\trans$. That
is, given a type $A \tp \MCU$, elements of $A$, $a, b, c, d \tp A$ and paths
between them, $p \tp a \equiv b$, $q \tp b \equiv c$ and $r \tp c \equiv d$ we
have the following:
%
\begin{equation}
\label{eq:cum-trans}
\trans\ p\ (\trans\ q\ r) ≡ \trans\ (\trans\ p\ q)\ r
\end{equation}
%
In this case the induction will be based at $c$ (the left-endpoint of $r$) and
over the family:
%
\begin{align*}
T & \tp \prod_{d' \tp A} \prod_{r' \tp c ≡ d'} \MCU \\
T\ d'\ r' & \defeq \trans\ p\ (\trans\ q\ r') ≡ \trans\ (\trans\ p\ q)\ r'
\end{align*}
%
So the base-case is proven with $t$ which is defined as:
%
\begin{align*}
\trans\ p\ (\trans\ q\ \refl) & ≡
\trans\ p\ q \\
& ≡
\trans\ (\trans\ p\ q)\ \refl
\end{align*}
%
Here we have used the proposition $\trans\ p\ \refl \equiv p$ without proof. In
conclusion \ref{eq:cum-trans} is inhabited by the term:
%
\begin{align*}
\pathJ\ T\ t\ d\ r
\end{align*}
%
We shall see another application on path-induction in \ref{eq:pathJ-example}.
\subsection{Paths over propositions}

3
doc/macros.tex
View file

@ -91,4 +91,5 @@
\newcommand\Endo[1]{\varindex{Endo}\ #1}
\newcommand\EndoR{\mathcal{R}}
\newcommand\funExt{\varindex{funExt}}
\newcommand{\suc}[1]{\mathit{suc}\ #1}
\newcommand{\suc}[1]{\varindex{suc}\ #1}
\newcommand{\trans}{\varindex{trans}}