path.tex

\section{Path types}
\label{sec:path}

To define Path constructively,
we may get some inspiration from its topological definition.
Open-up the \href{https://ncatlab.org/nlab/show/path}{``path'' segment in nLab},
there is a mathematical definition of a path, written as:

\[
  \mathbb I \rightarrow X
  \xtag
\]

Topologically, a path in a space $X$ is a continuous map
from an interval (denoted $\mathbb I$) to $X$.
Type theoretically, $\mathbb I$ and $X$ are types,
and $\mathbb I \rightarrow X$ is a function type from $\mathbb I$ to $X$.
As paths represent a relation \textit{between} two terms
(endpoints, but type theoretically),
these two terms should show up in the path type as well
(similar to MLTT identity type).
Therefore the formation rule for path types is naturally:

\[
  \cfrac{
    \Gamma \vdash X~\textbf{type}
    \quad
    \Gamma \vdash a : X
    \quad
    \Gamma \vdash b : X
  }{\Gamma \vdash a =_X b~\textbf{type}}
  \xtag
\]

Up to the time where this note is written,
everyone tries to define constructive HoTT defines path types this way.
They have different introduction and elimination rules,
but all of their introduction rules are
based on the interval type $\mathbb I$
and the elimination rules are slimiar to function application.

We can also define heterogeneous path types
(path between two terms of different types)
by changing the type $X$ into a type family $F$,
indexed by the interval type $\mathbb I$,
to allow paths between terms of different types:

\[
  \cfrac{
    \Gamma \vdash F : (i : \mathbb I) \rightarrow \mathcal U
    \quad
    \Gamma \vdash a : F~\textsf 0
    \quad
    \Gamma \vdash b : F~\textsf 1
  }{\Gamma \vdash a =_F b ~\textbf{type}}
  \xtag \label{eqn:hetero-path}
\]

Heterogeneous paths are used in~\cref{subsec:path-hit}.

\input{i}

\subsection{Path properties}
\label{subsec:path-prop}
\input{latex/path-properties}

\input{transp}

\subsection{Fillers}
\label{subsec:fill}

Recall~\ref{eqn:arend-proof-sym}, we can take the \textsf 1 argument away from
the applicaiton to \textsf{coe}:

\[
  \cfrac{
    \Gamma \vdash p : a =_A b
  }{
    \Gamma \vdash (\textsf{coe}
    (\lambda i. (p~i =_A a))~\refl_a)
    : (i : \mathbb I) \rightarrow p~i =_A a
  }
  \xtag \label{eqn:coe-a-b-path-gen-eta}
\]

Also, we know that the term $t = \textsf{coe} (\lambda i. (p~i =_A a))~\refl_a$
satisfies $t~\textsf 0 \equiv \refl_a$.
Recall $t~\textsf 1 : b =_A a$,
we have the following definitional equalities:

\[
  t~\textsf 0~\textsf 0 \equiv a \xtag \quad
  t~\textsf 0~\textsf 1 \equiv a \xtag
\]
\[
  t~\textsf 1~\textsf 0 \equiv b \xtag \quad
  t~\textsf 1~\textsf 1 \equiv a \xtag
\]

Here we can see $t$ as a higher-dimensional path,
as it's like a function taking more than one intervals,
while satisfying definitional equalities for all permutations of the endpoints.
Since it's two-dimensional, we call $t$ a \textit{square},
of the shape in~\cref{fig:filler}.

\begin{figure}
\begin{center}
  \begin{tikzpicture}[node distance=1.5cm]
    \node(1) {$b$ ($t~\textsf 1~\textsf 0, p~\textsf 1$)};
    \node(2) [right=4cm of 1] {$a$ ($t~\textsf 1~\textsf 1$)};
    \node(4) [below of=1] {$a$ ($\refl_a~\textsf 0, p~\textsf 0$)};
    \node(3) [below of=2] {$a$ ($\refl_a~\textsf 1$)};
    \draw (1) -- (2) node[midway,above] {$t~\textsf 1 : b =_A a$};
    \draw (1) -- (4) node[midway,left ] {$p$};
    \draw (3) -- (2);
    \draw (3) -- (4) node[midway,below] {$\refl_a$};
    \path (1) -- (3) node[midway] {$t$};
  \end{tikzpicture}
\end{center}
\caption{Filler for symmetry}
\label{fig:filler}
\end{figure}

Squares can be seen as paths between paths.
We can generalized this terminology to form topological shapes in any dimensions.
Paths between paths are \textit{homotopies} in HoTT,
while we informally call $t$ a \textit{filler} of the above square
when talking about constructive interpretations.

Note: fillers might be either paths or functions over intervals,
so we can also say $\textsf{path}~t$ is a filler of the same square.
We use the term just to follow the convention.