Provide example of using pathJ
This commit is contained in:
parent
513d91ae4f
commit
058f3c15a8
|
@ -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$.
|
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
|
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
|
construct a path between $f$ and $g$ -- the functions defined in the
|
||||||
(section \S\ref{sec:functional-extensionality}).
|
introduction (section \S\ref{sec:functional-extensionality}). Functional
|
||||||
%% module _ {ℓa ℓb} {A : Set ℓa} {B : A → Set ℓb} where
|
extensionality is the proposition, given a type $A \tp \MCU$, a family of types
|
||||||
%% funExt : {f g : (x : A) → B x} → ((x : A) → f x ≡ g x) → f ≡ g
|
$B \tp A \to \MCU$ and functions $f, g \tp \prod_{a \tp A} B\ a$:
|
||||||
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}
|
\begin{equation}
|
||||||
\label{eq:funExt}
|
\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:
|
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:
|
We have the function:
|
||||||
%
|
%
|
||||||
\begin{equation}
|
\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}
|
\end{equation}
|
||||||
%
|
%
|
||||||
I will not give an example of using $\pathJ$ here. An application can be found
|
A simple application of $\pathJ$ is for proving that $\var{sym}$ is an
|
||||||
later in \ref{eq:pathJ-example}.
|
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}
|
\subsection{Paths over propositions}
|
||||||
\label{sec:lemPropF}
|
\label{sec:lemPropF}
|
||||||
|
|
Loading…
Reference in a new issue