Nate

@JacquesCarette thanks! Some notes: - I'm also confident that Agda can do this thing, not least because if `triangle-alt` and `pentagram-alt` are used, agda handles the proof in 1,004ms. I'm...

Confirmed that the version with co-patterns still exhibits the issue. It _could_ be something to do with inlining, but if so, it's a case where the inlining is dramatically different...

Wild. Thanks for the tip! That suggests that somehow agda is getting bogged down comparing categories, in a fashion that's (for some reason) radically different between `lunit` and `runit`. In...

Thanks! When I add `{-# OPTIONS --no-syntactic-equality #-}`, `lunit` takes 7,055ms and `runit` takes 30,602ms -- both about 6,000ms longer than they take with the syntactic equality check, but `runit`...

This bug is starting to get troublesome to work around. Unfortunately, my use-case means that I can't get away with `no-eta-equality` on (the analog of) categories, because sometimes I need...

When I try that (on a version of Sigma with `no-eta-equality`), I get: ``` error: [SplitOnNonEtaRecord] Pattern matching on no-eta record type NoEtaSigma (defined at [...]) is not allowed (to...

I'm using K, alas. Are there any other options?

A feature that I expect would work around the performance issue here is some variant of `no-eta-equality` that leaves behind a propositional (non-computing, postulate-like) version of the eta rule, but...

Thanks! (IIUC none of those are compatible with --safe, so they're also not options for me, but I appreciate the tips.)