save progress on type theory section

papers/icfp24/code.sty

@@ -18,8 +18,8 @@
   basewidth        = {0em,0em},
   morekeywords     = {},
   deletekeywords   = {List},
-  emph             = [1]{Tree,List,SList,PList,Mset,SMC,FMSet,Perm,Maybe,hProp,hSet,Array,Bag,Fin,Sorted},
-  emph             = [2]{leaf,node,swap,trunc,eq,squash,perm-refl,perm-swap},
+  emph             = [1]{Tree,List,SList,PList,Mset,SMC,FMSet,Perm,Maybe,hProp,hSet,Array,Bag,Fin,Sorted,Circle},
+  emph             = [2]{leaf,node,swap,trunc,eq,squash,perm-refl,perm-swap,pos,neg,posneg,base,loop},
   emph             = [3]{i0,i1,hcomp,Nat},
   alsoletter       = {_,-},
   escapeinside     = ||,

papers/icfp24/introduction.tex

@@ -67,7 +67,7 @@ \section{Introduction}
 
         % the points in the sets (here I just create nodes to use them later on to position
         % the circles and the arrows
-        \node (x1) at (-1,0.7) {};
+        \node (x1) at (-1,0.6) {};
         \node (x2) at (-1.3,-0.7) {};
         \node (y1) at (0.8,0.3) {};
         \node (y2) at (1,-0.15) {};
@@ -120,7 +120,7 @@ \section{Introduction}
 in MLTT since oftentimes they can only be modelled via setoids. While setoids would suffice for
 formalizing these structures, they also bring a lot of proof burden which leads to a
 phenomenon (un)affectionately named "setoid hell". We have therefore decided to formalize our proofs
-for this paper in Cubical Agda, which allows us to work with these structures very naturally with
+for this paper in Cubical Agda~\cite{vezzosiCubicalAgdaDependently2019}, which allows us to work with these structures very naturally with
 higher inductive types, and allow for a very simple method to transport proofs between
 different constructions of free algebras by univalence. What also makes Cubical Agda attractive
 is that Cubical Type Theory allows us to enjoy the full power of univalence given by Homotopy Type Theory

papers/icfp24/type-theory.tex

@@ -1,7 +1,126 @@
 \section{Type Theory}
 \label{sec:type-theory}
+As we have explained, our work is formalized in Cubical Agda and Cubical Type Theory,
+which is a variant of Homotopy Type Theory that is designed to preserve
+computational properties of type theory.
+We refer the readers to other works such as~\cite{vezzosiCubicalAgdaDependently2019}
+and~\cite{cohenCubicalTypeTheory2018} for a more in-depth explanation on Cubical Type Theory
+and how we can program in Cubical Agda. Instead, we give a quick overview of relevant features
+in Cubical Type Theory which normal type theory (namely MLTT) lacks, and how these features
+are used within the scope of our work.
 
-We work in Cubical type theory, and formalize in Cubical Agda. We use the following notation\ldots\vc{write this after the technical content is written}
+\subsection{Function extensionality}
+Function extensionality $\term{funExt}$ states that given two functions $f$ and $g$,
+$\term{funExt}: \forall x.\,f(x) = g(x) \to f = g$. MLTT by itself does not have $\term{funExt}$,
+instead it has to be postulated as an axiom, thereby losing canonicity, in other words,
+we would not be able to compute any constructions of elements that involve $\term{funExt}$
+in its construction. In Cubical Type Theory, we can derive $\term{funExt}$
+as a theorem while also preserving canoncity, therefore we can compute with constructions
+involving $\term{funExt}$!
+
+Within the scope of our work, $\term{funExt}$ is heavily used in
+~\ref{mon:array} and~\ref{cmon:bag}, where a $n$-element array $A^n$ is defined as lookup functions
+$\Fin[n] \to A$. Therefore, to prove two arrays are equal, we need to show that two functions would be
+equal, which is impossible to do without $\term{funExt}$. We also would not be able to normalize
+any constructions of arrays which involve $\term{funExt}$ if it is postulated as an axiom, therefore
+the computational property of Cubical Type Theory is really useful for us.
+
+\subsection{Higher Inductive Types}
+Higher inductive types allow us to extend inductive types to not only allow point constructors
+but also path constructors, essentially equalities between elements of the HIT. One such example
+would be the following definition of $\mathbb{Z}$:
+
+\vspace{-1em}
+\begin{code}
+data $\mathbb{Z}$ : UU where
+    pos : (n : $\mathbb{N}$) -> $\mathbb{Z}$
+    neg: (n : $\mathbb{N}$) -> $\mathbb{Z}$
+    posneg : pos 0 == neg 0
+\end{code}
+\vspace{1em}
+
+The integers are often represented with a $\term{pos} : \Nat \to \mathbb{Z}$
+and $\term{negsuc} : \Nat \to \mathbb{Z}$, where natural numbers
+are mapped into the integers via the $\term{pos}$ constructor, and negative numbers are constructed
+by mapping $n : \Nat$ to $-(n + 1)$. The shifting by one is done to avoid having duplicate elements
+for 0, which can easily lead to confusion. HIT allows us to define integers more naturally by saying
+$\term{pos}(0) = \term{neg}(0)$, avoiding the confusing shift-by-one hack.
+
+One can see how we can define a general data type for set quotients. Here is the definition:
+\vspace{-1em}
+\begin{code}
+data _/_ (A : UU) (R : A -> A -> UU) : UU where
+    [_]  : A -> A / R
+    q/ : (a b : A) -> (r : R a b) -> [ a ] == [ b ]
+    trunc : (x y : A / R) -> (p q : x = y) -> p = q
+\end{code}
+\vspace{1em}
+
+The $\term{q/}$ constructor says if $a$ and $b$ can be identified by a relation $R$, then
+they should belong to the same quotient generated by $R$.
+One might also notice the $\term{trunc}$ constructor, which says and proofs of $x =_{A/R} y$ are equal.
+This constructor basically truncates the $\term{\_/\_}$ type down to set, so that we do not have to
+concern ourselves with higher paths generated by the $\term{q/}$ constructor.
+We give a more precise definition of "set" in Homotopy Type Theory and examples of types that are
+higher dimension than sets in~\ref{types:univalence}.
+
+In our work, higher inductive types and set quotients are used extensively to define commutative
+data structures, which we would demonstrate in~\ref{sec:commutative-monoids}. In MLTT we can only
+reason with quotients and commutativity by setoids, which comes with a lot of proof burden
+since we cannot work with the type theory's definition of equalities and functions directly,
+instead we have to define our own equality relation and define our own type for setoid homomorphisms,
+giving rise to the infamous setoid hell.
+
+\subsection{Univalence}\label{types:univalence}
+In MLTT we cannot construct equalities between types. Univalence, the core of Homotopy Type Theory,
+gives us equalities between types by the univalence axiom. To see how this is useful,
+consider $A, B : \mathcal{U}, P : \mathcal{U} \rightarrow \mathcal{U}, A = B$, we can
+get $P(B)$ from $P(A)$ by transport (or substitution).
+
+To explain the univalence axiom, we first need to define equivalence:
+\begin{definition}
+      Given types $A$ and $B$, $A$ is equivalent to $B$ ($A \simeq B$) if there exists an
+  equivalence $A \rightarrow B$.
+  A function $f$ is said to be an equivalence if
+  $\left( \sum_{g :B \rightarrow A} (f \circ g \sim \mathrm{id}_B) \right) \times \left( \sum_{g:B \rightarrow A} (g \circ f \sim \mathrm{id}_A) \right)$.
+\end{definition}
+
+We note that this is very similar to an isomorphism, however an isomorphism would have the same function
+for right inverse and left inverse, i.e. just an inverse function, whereas an equivalence allows
+for different functions for right and left inverse. The univalence axiom states that:
+\begin{definition}[Univalence axiom]
+     $(A = B) \simeq (A \simeq B)$
+\end{definition}
+
+This is directly incompatible with uniqueness of identity proof, which states
+$\forall p, q: x = y, p = q$. For example, consider the boolean type
+$\boolt = \{\term{true}, \term{false}\}$. We can construct two $\boolt = \boolt$
+by univalence:
+\begin{itemize}
+    \item $\term{id} := \lambda \{ \term{true} \mapsto \term{true}, \term{false} \mapsto \term{false} \}$
+    \item $\term{not} := \lambda \{ \term{true} \mapsto \term{false}, \term{false} \mapsto \term{true} \}$
+\end{itemize}
+
+Both functions are equivalences yet they are different, therefore they give rise to different equalities.
+We now introduce to notion of propositions, sets, groupoids, and so on.
+A mere proposition $A$ is a type such that $\forall x, y : A.\, x = y$.
+A set $A$ is a type such that for all $x, y : A$, the type $x = y$ is a mere proposition.
+A groupoid $A$ is a type such that for all $x, y : A$, the type $x = y$ is a set,
+and we can inductively define higher structures:
+A (n+1)-groupoid $A$ is a type such that for all $x, y : A$, the type $x = y$ is a n-groupoid.
+For example, $\unitt, \emptyt$ are propositions, $\unitt, \emptyt, \Nat$,
+the type for all types that are mere propositions $\hProp$ are sets.
+The type for all types that are sets $\hSet$ is a groupoid, and we have demonstrated how an element $\boolt$
+of $\hSet$ has more than one equality. When we are working with groupoids and higher-dimension
+types, the notion of equivalence and isomorphism becomes different.
+
+Within the scope of our work, we want to primarily work with
+sets, therefore we add the truncation constructor whenever necessary so we need not concern ourselves
+with higher-dimension paths (or equalities). Since we have multiple constructions of free monoids
+and free commutative monoids, given in~\ref{sec:monoids} and~\ref{sec:commutative-monoids},
+having univalence allows us to easily transport proofs and functions from one construction to another.
+Another instance where univalence is used is the definition of membership proofs in~\ref{comb:member},
+where we want to show to propositions are commutative: i.e. $\forall p, q: \hProp, p \vee q = q \vee p$.
+Since $p$ and $q$ are types, we need univalence to show $p \vee q = q \vee p$ are in fact equal.
 
-\vc{We use HoTT/Cubical because it gives us: quotients, funext, univalence, these are useful and critical to our development.}
 \vc{Explain Fin here.}