hit.tex

\section{Higher inductive types}
\label{sec:hit}

By the above constructive path type,
we can extend inductive types with path constructors.
Recall that a constructor of an inductive type $T$ is
similar to a function whose return type is $T$,
but does not reduce.

Inductive types with path constructors are called
\textit{higher inductive types} (hereafter as HIT),
which is discussed in Chapter 6 of the HoTT Book.
The integer type $\mathbb Z$ is a good example of HIT.
Given this natural number $\mathbb N$ definition:

\begin{gather*}
  \vdash \mathbb N~\textbf{type}
  \xtag
  \\
  \vdash \textsf{zero} : \mathbb N
  \xtag
  \quad
  \vdash \textsf{succ} : \mathbb N \rightarrow \mathbb N
  \xtag
  \\
\end{gather*}

We can derive the definition of $\mathbb Z$:

\begin{gather*}
  \vdash \mathbb Z~\textbf{type}
  \xtag
  \\
  \vdash \textsf{pos} : \mathbb N \rightarrow \mathbb Z
  \xtag
  \quad
  \vdash \textsf{neg} : \mathbb N \rightarrow \mathbb Z
  \xtag
  \\
  \vdash \textsf{zro} :
  \textsf{pos zero} =_{\mathbb Z} \textsf{neg zero}
  \xtag
\end{gather*}

$\mathbb Z$ has two \textbf{point constructors}
\textsf{pos} and \textsf{neg}, with one \textbf{path constructor}
\textsf{zro} whose two endpoints are \textsf{pos zero} and \textsf{neg zero}.

Path constructors add constraints to the operations defined on HITs.
Taking the $\mathbb Z$ type as an example,
for an arbitrary type $A$ and a function $f : \mathbb Z \rightarrow A$,
the path $p = \textsf{ap}_f(\textsf{zro})$ should to some extent
satisfy the following two equalities
(some model require these equalities to be definitional, some don't):

\[
  p~\textsf 0 =_A f~(\textsf{pos zero})
  \xtag
  \quad
  p~\textsf 1 =_A f~(\textsf{neg zero})
  \xtag
\]

For the general case, given arbitrary HIT $T$, an arbitrary type $A$ and
function $f : T \rightarrow A$, for all path constructors
$p : a =_T b$ of $T$, there should be:

\[
  p~\textsf 0 =_A f~a
  \xtag
  \quad
  p~\textsf 1 =_A f~b
  \xtag
\]

We call this property ``agree on path constructors'',
or ``respect the path constructors''.

Higher inductive types are similar in CTT and CCTT,
while Arend is somehow different from the other two.

\subsection{Axiomatic approach}
\label{subsec:axiomatic}

In the old days, there were no constructive path type.
People use the MLTT identity type and
work with HITs by postulating their existence.
What they're actually postulating is the existence of the path constructors.

There had been a lot of work done based on this approach,
under various proof assistants such as Hoq
(a modified version of Coq, short for HoTT-Coq),
% TODO: is lean based on this?
and Agda (before cubical).

Many HITs can be generalized as a specialized version of a standard
quotient type. If we only postulate a quotient type, we can specialize
it into a number of other HITs to avoid postulating things again.

In the HoTT library~\cite{HottCoq} of Coq, the comments in the quotient
type module provide an ideal syntax for the quotient type definition:

\begin{minted}{coq}
  Inductive quotient : Type :=
  | class_of : A -> quotient
  | related_classes_eq : forall x y,
      (R x y), class_of x = class_of y
  | quotient_set : IsHSet quotient.
\end{minted}

We can read it as ``\textsf{quotient} is a type,
which has a point constructor \textsf{class\_of},
a path constructor \textsf{related\_classes\_eq}
and a proof that \textsf{quotient} is an HSet
(which is also a path constructor)''.
The \href{https://github.com/HoTT/HoTT/blob/b20bb573739284349a968bb219405255c744049d/theories/HIT/quotient.v#L40-L42}
{actual definition}, on the other hand, is:

\begin{minted}{coq}
  Private Inductive quotient
      {sR: is_mere_relation _ R} : Type :=
  | class_of : A -> quotient.
  Axiom related_classes_eq : forall {x y : A}, R x y ->
      class_of x = class_of y.  
  Axiom quotient_set : IsHSet (@quotient sR).
\end{minted}

We can read it as ``\textsf{quotient} is a type paramterized by a relation \textsf R,
and we postulate that the terms belonging to the same equivalent class are equivalent,
and we postulate that \textsf{quotient} is an HSet''.
This axiomatic definition does not ensure that functions defined on
axiomatic HITs agree on their path constructors.
In fact, it doesn't even ensure that terms belonging to the same equivalent
class are equivalent.

\input{latex/hit-agda-old}

\subsection{Conditions}
\label{subsec:conditions}

Arend supports two ways of defining HITs.
One is like Agda's old approach, say, providing path constructors
as something similar to a rewriting rule, namely \textit{conditions}.
They also support CCTT-style HITs, we talk about that together with
CCTT in~\cref{subsec:path-hit}.
However, Arend requires operations defined on HITs to agree on the conditions,
thus it's more consistent to the theoretical model of HITs in HoTT.

For instance, the integer type in Arend can be defined as:

\begin{minted}{arend-lexer.py:ArendLexer -x}
  \data Int
    | pos Nat
    | neg Nat \with {
      | zero => pos zero
    }
\end{minted}

Note that the constructor \textsf{neg} is attached with an additional
condition, saying that when the parameter of
\textsf{neg} appears to be \textsf{zero},
the term constructed by \textsf{neg} in this case should be
(definitionally) equivalent to \textsf{pos zero}.

Consider the following function, which do not agree with this condition:

\begin{minted}{arend-lexer.py:ArendLexer -x}
  \func absolute-value-bad (x : Int) : Nat
    | pos n => suc n
    | neg n => n
\end{minted}

When checking the \textsf{neg} clause, Arend substitutes $n$ with
\textsf{zero} according to the condition, and check if the returned
term, \textsf{zero}, is identical to
\textsf{absolute-value (pos zero)}, which reduces to \textsf{suc zero}.
It seems not, so the function is ill-formed.
Changing the definition to the following will satisfy Arend:

\begin{minted}{arend-lexer.py:ArendLexer -x}
  \func absolute-value-good (x : Int) : Nat
    | pos n => n
    | neg n => n
\end{minted}

This one will also work, because both sides of the condition
are \textsf{suc zero}
(the function name \textsf{absolute-value} indicates that it's finding
the absolute value of the input integer, while the following function
is not actually doing that.
Thus we add the postfix \textsf{-cheat} to it):

\begin{minted}{arend-lexer.py:ArendLexer -x}
  \func absolute-value-cheat (x : Int) : Nat
    | pos n => suc n
    | neg n => suc n
\end{minted}

% The path constructors encoded as conditions
% are still so different from the point constructors.
% They are not listed along with other constructors,
% and when pattern matching against an \textsf{Int},
% only \textsf{pos} and \textsf{neg} are covered.

Conditions are simple, because they're just constraints.
A problem is that when defining operations on condition-based HITs,
the constraints added by conditions should hold definitionally.
In case of the \textsf{absolute-value} function,
$\textsf{absolute-value}(\textsf{neg zero}) \equiv
\textsf{absolute-value}(\textsf{pos zero})$ should hold definitionally.
There are times when definitional equalities are difficult to have,
so conditions may not be the ultimate solution.

As path constructors are called ``constructors'',
we'll have to define them as constructors anyway.

% To form more complicated path constructors
% (which cannot be expressed as a condition),
% we'll need to define the path constructors as constructors explicitly.
% There is a more fancy way to define path constructors,
% that is, to define them as constructors.

\input{latex/hit-agda-new}

\subsubsection{Alternative syntax}

In Arend (also in \RedPRL~and redtt),
path constructors are not written as constructors of path types.
Instead, they specify the endpoints (or \textit{edges})
of the constructor directly.
Here's how Arend define $\mathbb{S}^1$,
where the endpoints of \texttt{loop} is directly specified:

\begin{minted}{arend-lexer.py:ArendLexer -x}
  \data S1
    | base
    | loop I \with {
      | left  => base
      | right => base
    }
\end{minted}

As a consequence, higher-dimensional path constructors are way more
straightforward -- like the \texttt{square} constructor of $T^2$,
whose four edges are directly specified:

\begin{minted}{arend-lexer.py:ArendLexer -x}
  \data T2
    | point
    | line1  I   \with { left => point | right => point }
    | line2  I   \with { left => point | right => point }
    | square I I \with {
      | left,  i => line2 i
      | right, i => line2 i
      | i, left  => line1 i
      | i, right => line1 i
    }
\end{minted}

% Maybe write some redtt/RedPRL code here?