Post #2590496

@constantine@types.pl @trebor@types.pl @olynch@mathstodon.xyz I did write this out in a draft note several years ago, but I never tried it in Agda. This is really cool!