A formalisation in Cubical Agda of various definitions, constructions and lemmas from the paper "Distributive Laws of Monadic Containers" by Chris Purdy and Stefania Damato.
For an HTML-rendered version of this code, see here.
Requires:
- Agda
v2.6.4 - Cubical
v0.7