Post #2093352
2026-01-08 18:40 UTC
The bittersweet feeling of getting rid of hundreds of lines of a fiddly proof in Agda to replace it with a nice, short, conceptual proof that’s about 17 lines long (and requires one fewer axiom). Details will follow (when I merge the code), but the main take away has been that the closure properties of orthogonal maps are very powerful (https://samtoth.github.io/agda-synthetic-categories/stt-00BZ/index.xml)
Replies (2)
-
@SamToth@mathstodon.xyz 2026-01-12 21:06
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
-
@FredrikBakke@mathstodon.xyz 2026-01-08 20:05
@SamToth@mathstodon.xyz and the new proof has the dual consequence built in ;)