checkpoint

papers/cpp25/formalization.tex

@@ -14,9 +14,9 @@ \section{Formalization}
 The free algebra framework in the formalization is
 parameterized by any h-levels, but it currently only works with sets.
 We also note the axioms of sorting in the formalization is named differently,
-$\issorted$ is $\term{is-sorted}$
-$\isheadleast$ is $\term{is-head-least}$, and
-$\istailsort$ is $\term{is-tail-sort}$.
+% $\issorted$ is $\term{is-sorted}$
+% $\isheadleast$ is $\term{is-head-least}$, and
+% $\istailsort$ is $\term{is-tail-sort}$.
 We give a table of the Agda file names and their corresponding sections in the paper
 at~\cref{appendix:formalizations}.
 

papers/cpp25/free-commutative-monoids.tex

@@ -519,3 +519,9 @@ \subsubsection*{Remark on representation}\label{bag:rep}
 or perform operations on the partitions individually such as two individual permutation in~\cref{bag:cong}.
 This makes it such that when defining divide-and-conquer algorithms such as merge sort,
 $\Bag$ and $\Array$ are more natural to work with than $\List$, $\SList$, and $\PList$.
+
+\redtext{
+    We use $\bag{x,y,\dots}$ to denote $\eta_A(x) \mult \eta_A(y) \mult \dots : \MM(A)$,
+    and $[x, y, \dots]$ to denote $\eta_A(x) \mult \eta_A(y) \mult \dots : \LL(A)$,
+    or $x \cons xs$ to denote $\eta_A(x) \mult xs : \LL(A)$.
+}

papers/cpp25/hott.sty

@@ -60,6 +60,10 @@
 \newcommand{\inr}{\term{inr}}
 \newcommand{\copair}[1]{[#1]}
 
+% FIXME: mathsmaller
+\providecommand{\mathsmaller}{}
+\renewcommand{\mathsmaller}[1]{#1}
+
 % identity type
 \NewDocumentCommand{\id}{E{^_}{{}{}}}{
   \mathrel{
@@ -141,7 +145,7 @@
 % dependent sum
 \NewDocumentCommand{\dsum}{smm}{
   \IfBooleanTF{#1}
-  {\displaystyle\sum\limits_{\mathsmaller{#2}}{#3}}
+  {\sum_{{#2}}{#3}}
   {\textstyle\sum_{({#2})}{#3}}
 }
 \newcommand{\pair}[1]{\ps{#1}}

papers/cpp25/macros.sty

@@ -98,9 +98,12 @@
 
 % sort
 \newcommand{\issortedany}{\term{in-image}}
-\newcommand{\issorted}{\issortedany_s}
-\newcommand{\isheadleast}{\term{image-respects-pair}}
-\newcommand{\istailsort}{\term{image-can-induct}}
+\newcommand{\issorted}[1]{{#1}\in\im{s}}
+\newcommand{\inimage}[1]{{#1}\in\im{s}}
+
+\newcommand{\isheadleast}{\term{im-cut}}
+\newcommand{\istailsort}{\term{im-cons}}
+
 \newcommand{\setord}{\term{Ord}}
 \newcommand{\Ord}{\term{Ord}}
 \newcommand{\setmtol}{\term{M2L}}

papers/cpp25/math.sty

@@ -93,7 +93,7 @@
 
 % sets and bags
 \newcommand{\set}[1]{\{#1\}}
-\newcommand{\bag}[1]{\lbag{#1}\rbag}
+\newcommand{\bag}[1]{{\lbag}{#1}{\rbag}}
 
 % free algebras
 \newcommand{\LL}{\mathcal{L}}
@@ -103,6 +103,7 @@
 % sort
 \newcommand{\sort}{\mathsf{sort}}
 \newcommand{\sect}{\mathscr{s}}
+\newcommand{\leqs}{\preccurlyeq_{s}}
 
 % lattices
 \newcommand{\meet}{\sqcap}