/Functor/Free/Instance/SymmetricMonoidalPreorder/
../
Lax.agda