From 058f3c15a8de046fc44ba5cf3d4cac41bba634cf Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Thu, 10 May 2018 15:28:33 +0200
Subject: [PATCH] Provide example of using pathJ

---
 doc/cubical.tex | 55 +++++++++++++++++++++++++++++++++++++------------
 1 file changed, 42 insertions(+), 13 deletions(-)

diff --git a/doc/cubical.tex b/doc/cubical.tex
index 43446cd..4284542 100644
--- a/doc/cubical.tex
+++ b/doc/cubical.tex
@@ -108,13 +108,10 @@ judgmentally $a$ at either endpoint. This is satisfied by the constant path;
 i.e. the path that stays at $a$ at any index $i$.
 
 It is also surpisingly easy to show functional extensionality with which we can
-construct a path between $f$ and $g$ -- the function defined in the introduction
-(section \S\ref{sec:functional-extensionality}).
-%% module _ {ℓa ℓb} {A : Set ℓa} {B : A → Set ℓb} where
-%%   funExt : {f g : (x : A) → B x} → ((x : A) → f x ≡ g x) → f ≡ g
-Functional extensionality is the proposition, given a type $A \tp \MCU$, a
-family of types $B \tp A \to \MCU$ and functions $f, g \tp \prod_{a \tp A}
-B\ a$:
+construct a path between $f$ and $g$ -- the functions defined in the
+introduction (section \S\ref{sec:functional-extensionality}). Functional
+extensionality is the proposition, given a type $A \tp \MCU$, a family of types
+$B \tp A \to \MCU$ and functions $f, g \tp \prod_{a \tp A} B\ a$:
 %
 \begin{equation}
 \label{eq:funExt}
@@ -263,23 +260,55 @@ at some element $a \tp A$.
 Let a type $A \tp \MCU$ and an element of the type $a \tp A$ be given. $a$ is said to be the base of the induction. Given a family of types:
 %
 $$
-P \tp \prod_{a' \tp A} \prod_{p \tp a ≡ a'} \MCU
+D \tp \prod_{b \tp A} \prod_{p \tp a ≡ b} \MCU
 $$
 %
-And an inhabitant of $P$ at $\refl$:
+And an inhabitant of $D$ at $\refl$:
 %
 $$
-p \tp P\ a\ \refl
+d \tp D\ a\ \refl
 $$
 %
 We have the function:
 %
 \begin{equation}
-\pathJ\ P\ p \tp \prod_{a' \tp A} \prod_{p \tp a ≡ a'} P\ a\ p
+\pathJ\ D\ d \tp \prod_{b \tp A} \prod_{p \tp a ≡ b} D\ a\ p
 \end{equation}
 %
-I will not give an example of using $\pathJ$ here. An application can be found
-later in \ref{eq:pathJ-example}.
+A simple application of $\pathJ$ is for proving that $\var{sym}$ is an
+involution. Namely for any set $A \tp \MCU$, points $a, b \tp A$ and a path
+between them $p \tp a \equiv b$:
+%
+\begin{equation}
+\label{eq:sym-invol}
+\var{sym}\ (\var{sym}\ p) ≡ p
+\end{equation}
+%
+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\ b'\ p' & \defeq \var{sym}\ (\var{sym}\ p') ≡ p'
+\end{align*}
+%
+The base-case will then be:
+%
+\begin{align*}
+d & \tp \var{sym}\ (\var{sym}\ \refl) ≡ \refl \\
+d & \defeq \refl
+\end{align*}
+%
+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
+  \tp
+  \var{sym}\ (\var{sym}\ p) ≡ p
+\end{align*}
+%
+We shall see another application on path-induction in \ref{eq:pathJ-example}.
 
 \subsection{Paths over propositions}
 \label{sec:lemPropF}