January Update 1
Although I did not spend a huge amount of time on the project this week, I thankfully discovered my mistake from last week about \(\mathrm{delay}\)’s linearity, which warrants an update.
Linearity of \(\mathrm{delay}\)
My mistake is rather easy to spot if we consider the double-sorted duploids. In Munch-Maccagnoni’s thesis [1], \({\Uparrow}\) and \(\mathrm{delay}\) (dually \(\Downarrow\) and \(\mathrm{unwrap}\)) are defined on positive (dually negative) objects only, and then get extended to negative (dually positive) objects by defining \({\Uparrow}n = n\) and \(\mathrm{delay}_n = \mathrm{id}_n\) (dually \({\Downarrow}p = p\) and \(\mathrm{unwrap}_p = \mathrm{id}_p\)). Thus we fairly trivially have:
- For \(p \in \mathcal{P}\), \(\mathrm{delay}_p : p \to {\Downarrow}p\) is linear, because its codomain is \(p\).
- For \(n \in \mathcal{N}\), \(\mathrm{delay}_n : n \to {\Downarrow}b\) is linear, because identities are linear.
…and dually for \(\mathrm{unwrap}\). Indeed, the thesis states right above the proposition that I complained about:
Also, extending Proposition II.12, we have, for all objects \(A\), that \(\mathrm{unwrap}_A\) and \(\mathrm{wrap}_A\) are thunkable whereas \(\mathrm{delay}_A\) and \(\mathrm{force}_A\) are linear.
This suggests that the definition of single-sorted duploids from last time could do with a revision:
- A “single-sorted duploid” is a single-sorted preduploid
\(\mathcal{C}\) with the following additional data:
- For every object \(a : \mathrm{ob}\ \mathcal{C}\),
- its upshift \({\Uparrow}a : \mathrm{ob}\ \mathcal{C}\)
- a linear morphism \(\mathrm{force}_a : {\Uparrow}a \to a\)
- a proof that \({\Uparrow}a\) is negative
- a linear inverse for \(\mathrm{force}_a\) called \(\mathrm{delay}_a : a \to {\Uparrow}a\).
- Dually, for every object \(a : \mathrm{ob}\ \mathcal{C}\),
- its downshift \({\Downarrow}a : \mathrm{ob}\ \mathcal{C}\)
- a thunkable morphism \(\mathrm{wrap}_a : a \to {\Downarrow}a\)
- a proof that \({\Downarrow}a\) is positive
- a thunkable inverse for \(\mathrm{wrap}_a\) called \(\mathrm{unwrap}_a : a \to {\Downarrow}a\).
- For every object \(a : \mathrm{ob}\ \mathcal{C}\),
This also makes for a much nicer proof that the shift axioms are homotopy-propositional, as linear inverses and thunkable inverses are each unique if they exist.
I would be curious for a proof that the definition of shifts as universal properties [2] corresponds to the above, but it seemed like far too much data for me to encode into UniMath for the moment.
Organisational Changes
I was never fully happy with the preliminary definitions or organisation in my initial formalisation of the first half of the duploids paper. The degree of boilerplate required to define each type (constructor, projections, h-level lemmas) makes me very anxious about making a mess, as does having to decide whether to use bundled or unbundled representations, and to bundle them in the right order, and to dualize all the definitions and proofs… In other words, I am suffering a lot with my programming language should really just do for me! To stay sane though, the next best thing is to meticulously organise the definitions by modules and rocqdoc headings.
At the moment I have split off “quasiduploid”s (which I have sensibly but pretentiously renamed to “unital magmoids”) into their own file, where I can develop the interesting lemmas about them. Conveniently, any definitions and proofs in UniMath that only use the data of a precategory (objects, morphisms, identity and composition), but not its axioms (identities being identities, composition) generalize perfectly to unital magmoids. Less conveniently, many definitions and lemmas use more data than they need.
I am sure lemma dualization will be a flagship feature of the next great proof assistant, but until then I will leverage Emacs to textually dualize as much as possible with regular expressions (see below). Templates via YASnippet are also tempting for reducing boilerplate, but they would do little for my sanity when reading or modifying the development, which is really the more important part. If there were an invertible version of templates that could be used for display that would be nice, but I did not find one.
(use-package regexpl :defer t)
(defcustom eutro-dualize-alist nil
"Alist of replacements to make in `eutro-dualize-region'."
:type '(alist :key string :value string)
:group 'eutro)
(defun eutro-dualize-region (start end)
"Dualize the region according to `eutro-dualize-alist'."
(interactive
(progn
(cl-assert (use-region-p) nil "No region selected")
(list (region-beginning) (region-end))))
(save-excursion
(goto-char start)
(save-restriction
(narrow-to-region start end)
(regexpl-search-replace-list
(nconc (mapcar (lambda (x) (cons (cdr x) (car x)))
eutro-dualize-alist)
eutro-dualize-alist)))))
(defun eutro-yank-dual ()
"Yank and dualize."
(interactive)
(yank)
(eutro-dualize-region (region-beginning) (region-end)))