kan.tex

\section{Kan operations}
\label{sec:kan}

In~\cref{subsec:coe}, we have seen an operation on paths,
that is \textsf{coe}, which returns a path~\footnote
{It's not actually a path in Arend, but a function over intervals.
  We can say it's \textit{almost} a path.}.
Since it returns a path, we may wonder how is the returned path
represented internally.
Ideally, we want \textsf{coe} to be a built-in but reducible function,
which means that it \textbf{computes} when fully applied.
Unfortunately, \textsf{coe} in Arend only computes in certain hard-coded cases,
which is not ideal.
There is a more general operation in CTT and CCTT which allows computation
on path operations, namely \textit{Homogenous composition}.

The idea is in one sentence:

\begin{displayquote}
  For any n-dimensional cube, it has $2 \times n$ faces.
  If we can construct $2 \times n - 1$ of them,
  the last one face can be obtained by doing a homogenous composition.
\end{displayquote}

In case it's two-dimensional, the cube becomes a square,
and it has four faces, which are all one-dimensional paths.
If we can have three of these paths,
we can obtain the last path via homogenous composition.
We can graph this process, as in~\cref{fig:simple-comp}
(assuming $\vdash a, b, c, d : A$).

\begin{figure}
\begin{center}
  \begin{tikzpicture}[node distance=1.5cm]
    \node(1) {$a$};
    \node(2) [right=4cm of 1] {$b$};
    \node(4) [below of=1] {$c$};
    \node(3) [below of=2] {$d$};
    \draw (1) -- (2) node[midway,above] {Obtained by composition};
    \draw (1) -- (4) node[midway,left ] {$p : c =_A a$};
    \draw (3) -- (4) node[midway,below] {$r : c =_A d$};
    \draw (2) -- (3) node[midway,right] {$q : d =_A b$};
  \end{tikzpicture}
\end{center}
\caption{Simple composition}
\label{fig:simple-comp}
\end{figure}

This looks very similar to~\cref{fig:filler}
if we substitute $a$ with $b$ and $b, c, d$ with $a$.
We can also prove path composition by substituting $a$ with $c$.

Here's the surface syntax of homogenous composition.
In~\cite{CCHM}, there are two basic structures that the composition operation
is based on (this note simplifies the definitions in the paper,
since this note talks about the general concept instead of any specific variation):

\begin{align*}
  \varphi &= (i=\textsf 0) \mid (i=\textsf 1)
  & \xtag \\
  u &= [ \; \varphi_1 \mapsto t_1,
      \dots, \varphi_n \mapsto t_n \; ]
  & \xtag
\end{align*}

$\varphi$ is called the \textit{Face lattice},
which stands for a constraint that specifies a face.
$u$ is a list of face-term pair $\varphi \mapsto t$,
where each pair specifies a term $t$ for a face $\varphi$.
Thus we can describe an open shape via $u$.

The composition operation is defined as following:

\newcommand{\comp}{\textsf{hcomp}}

\[
  \cfrac
  {\Gamma \vdash F : \mathbb I \rightarrow \mathcal U \quad
    \Gamma \vdash a : F \ \textsf 0}
  {\Gamma \vdash \comp~F~(\lrangle i u)~a : F \ \textsf 1}
  \xtag
\]

Where, the faces in $u$ should include all of the
side faces.
Also, the terms in $u$ should fill the corresponding faces --
the endpoints need to match.

In naturally language, given
$F$ -- a type indexed by $\mathbb I$,
$a$ -- a term for the bottom face of the cube,
$u$ -- a list of face-term pairs representing all the faces except
$a$ and the top-missing face.
Then, $\comp~F~(\lrangle i u)~a$ produces the top face.
As an example, the ``Obtained by composition'' path in~\cref{fig:simple-comp}
can be written as:

\[
  \lrangle i \comp~(\lambda a. A)~(\lrangle j [
  (i = \textsf 0) \mapsto p~j, (i = \textsf 1) \mapsto q~j ])~r
  \xtag
\]

The above terms does the same job as the following
\textsf{coe}-based operation:

\[
  \lrangle i
  \textsf{coe}~(\lambda j. p~j =_A q~j)~r
\]

However, $\comp$ has well-defined computation rules,
while \textsf{coe} over paths or $\mathbb I$ don't.
$\comp$ does not work for paths or $\mathbb I$ either,
but it does almost everything that \textsf{coe} over paths can do,
by wrapping all the complicated paths into $u$.

\subsection{Derived operations}

In CCTT, there is another variation of $\varphi$:

\[
  \varphi = \dots \mid (i = j)
  \xtag
\]

This face specifies a diagonal.
It provides more computation rules and simplifies some certain
$\comp$ operations.

Similar to the generalization of \textsf{coe} in~\cref{subsec:coe},
there's also a generalized version of $\comp$
where it takes one more $\mathbb I$ parameter $i$,
and return the \textit{slice} of the cube at the position
specified by $i$.
In other words, if we see the square in~\cref{fig:simple-comp} as a path
between the bottom face $r$ and the top face,
the generalized composition can return any point (which is in fact a path) on the path.
The typing rule is similar to:

By having generalized composition,
what we can actually obtain from this generalization
is the filler to the square in~\cref{fig:simple-comp}
(which is usually a high-dimensional path),
while we often take the top face directly.
We may hereafter refer to this generalized composition as \textsf{hfill}.

\[
  \cfrac
  {\Gamma \vdash F : \mathbb I \rightarrow \mathcal U \quad
    \Gamma \vdash a : F \ \textsf 0}
  {\Gamma \vdash \textsf{hfill}~F~(\lrangle i u)~a : (i : \mathbb I) \rightarrow F \ i}
  \xtag
\]

We may also say that \textsf{hfill} is an operation \textit{derived} from
\textsf{hcomp} (instead of \textit{generalized}).

In Cubical Agda, $u$ is represented as a special type of lambda expression,
of type \AgdaFunction{Partial}.

\input{latex/hcomp-agda}