/Functor/Free/Instance/MonoidalPreorder/
../
Lax.agda
Strong.agda