What about the other fields that still have primed versions?

Actually that's a good point. I've only addressed one. I'll draft this for now and make sure I've got them all.

Well, specifically about that bug anyway. I need to think a bit more about why we still have primed fields in CatEquiv.

(Just to be clear, I meant the other fields of the same Class.)

I tried removing the primes in the other fields and got the wildcat library working, however Coq gets stuck on the Defined of one of the proofs of ExactSequence. Specifically isexact_connect_R.

Not sure what is going on there. I'll keep my changes and submit in a PR after this is merged if you want to take a closer look.

I guess the issue is the one explained in a comment: Since apparently a field of a record can't be the source of a coercion ....

I think it's fine to merge this to at least get rid of one redefinition.

I also had a go at removing InO_internal from ReflectiveSubuniverse but I was not successful.

Rebasing this breaks DisplayedEquiv. @gio256 could you have a look at what is wrong? I wasn't able to fix it.