Post #2747760

The code has now been merged, and if you are interested in some details you can find a short summary of the changes and some of my thoughts here: https://samtoth.github.io/agda-synthetic-categories/stt-00CY