The 'parameterized end' (EndF) construction introduced in #422 causes many performance issues that are only solved by --lossy-unification.
This should be fixed so that --lossy-unification is not necessary to use EndF
agda --profile=all src/Categories/Diagram/End/Fubini.agda output: gist
Zulip thread