Work out why test/WildCat/Opposite.v is slow

[Alizter]

We need to work out why Coq is so slow in the following example:

From HoTT Require Import Basics WildCat.Core WildCat.Opposite WildCat.Equiv.

(** * Opposites are definitionally involutive. *)

Definition test1 A : A = (A^op)^op :> Type := 1.
Definition test2 A `{x : IsGraph A} : x = @isgraph_op A^op (@isgraph_op A x) := 1.
Definition test3 A `{x : Is01Cat A} : x = @is01cat_op A^op _ (@is01cat_op A _ x) := 1.
Definition test4 A `{x : Is2Graph A} : x = @is2graph_op A^op _ (@is2graph_op A _ x) := 1.
Definition test5 A `{x : Is1Cat A} : x = @is1cat_op A^op _ _ _ (@is1cat_op A _ _ _ x) := 1.

(** * [core] only partially commutes with taking the opposite category. *)
Definition core1 A `{HasEquivs A} : (core A)^op = core A^op :> Type := 1.
Definition core2 A `{HasEquivs A} : isgraph_op (A:=core A) = isgraph_core (A:=A^op) := 1.
Definition core3 A `{HasEquivs A} : is01cat_op (A:=core A) = is01cat_core (A:=A^op) := 1.
Definition core4 A `{HasEquivs A} : is2graph_op (A:=core A) = is2graph_core (A:=A^op) := 1.

(** This also passes, but we comment it out as it is slow.  When uncommented, to save time, we end with [Admitted.] instead of [Defined.] *)
(*
Definition core5 A `{HasEquivs A} : is1cat_op (A:=core A) = is1cat_core (A:=A^op).
  Time reflexivity. (* ~6s *)
Admitted.
*)

Something fishy is going on in core5, but I haven't been able to workout what.

Some context: #1929 (comment)

[jdchristensen]

I just realized that my comment at #1929 (comment) was confused. In that spot of that PR, what is being used is that op is involutive. Here, core5 is checking that core and op commute. So it's not weird that one of them (here) is slow while the other (in that PR) is fast. This one is probably slow simply because there is a huge amount to unpack. So this can probably be closed. (Although it would be nice if there was a way to make this fast...)

[Alizter]

Yes, looking back I think you are right. The issue here which perplexes me is that all of these examples in the test are instant except for is1cat. I tried for an hour today to get a favourable manual reduction but the term is just so huge. I also tried tweaking the proofs Equiv.v about core so that they are as eta reduced as possible. I cannot workout why this is such a straining example for Coq.