Directed equality for (co)end calculus

How to run this

Install Nix with flakes enabled, then run nix develop to have a working Agda installation. Alternatively, install the correct Agda version manually.

The file All.agda groups all formalization files for batch typechecking/inspection. Typecheck the code by running Agda in Safe Mode:

$ agda --safe ./All.agda +RTS -M16G  # Recommended flags for Agda.

Warning

Most of the files contained here are particularly slow to typecheck and require considerable memory, and might run out of memory even with >8 GB allocated. The recommended flags for Agda under which this formalization has been tested are +RTS -M16G, which should ensure that eventually every file compiles.

The flake output agda-html can be used to typecheck and build the HTML for the All.agda file (the above flags are already active):

$ nix build '.#agda-html' # This typechecks and creates a browsable HTML output.
$ xdg-open html/All.html  # Open html/All.html in your browser.

Files structure

Each of the theorems in the paper links to a single formalization file, which typically only has a single main definition with secondary definitions given later.

Comments

Naturality of the rules is only shown for the case of exponentials in Dinaturality.NaturalExample, due to the technical limitation of running out of memory for most of the remaining rules. Finding a workaround to fully formalize naturality for every rule is left for future work.

Every file which typechecks is contained in the All file.

The formalization for the left relative adjunction in Dinaturality/Sketch/HomRelativeAdjunction contains only a minimal formalization sketch. See the description at the top of the file.

Files in the folder Failure/ do not typecheck (on purpose), and they are not included in the All file. They are just sanity checks to verify that something is not provable.

Typechecking time

Running agda --safe ./All.agda +RTS -M16G on an AMD Ryzen 7 5800X (16) @ 3.792GHz running Debian 12 on WSL2 (Windows 10.0.19045 x86_64) takes approximately ~30 mins to complete (assuming all libraries have been compiled).

Requirements

• agda 2.6.4.1
• agda-categories 0.2.0
• agda-stdlib 2.0