Open 4e554c4c opened 2 months ago
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
EndF
--lossy-unification
agda --profile=all src/Categories/Diagram/End/Fubini.agda output: gist Zulip thread
agda --profile=all src/Categories/Diagram/End/Fubini.agda
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-unificationis not necessary to useEndFagda --profile=all src/Categories/Diagram/End/Fubini.agdaoutput: gist Zulip thread