As of 2023-01-18, on newest Agda, the definition in module Verification.Core.Category.StdMonoidal.Category.Definition works relatively fast if the definition of monoidal category is unwrapped: requiring functions and equations instead of requiring functors and natural isos.
Currently, the abstract definition makes Agda in this file, and also in the dependant "monoid in monoidal category" noticeably slower.
As of 2023-01-18, on newest Agda, the definition in module
Verification.Core.Category.StdMonoidal.Category.Definitionworks relatively fast if the definition of monoidal category is unwrapped: requiring functions and equations instead of requiring functors and natural isos.Currently, the abstract definition makes Agda in this file, and also in the dependant "monoid in monoidal category" noticeably slower.