Remove reversible coercions throughout the library

[patrick-nicodemus]

A record projection marked as :> declares it as a "reversible coercion" in the absence of further annotations: https://rocq-prover.org/doc/V9.0.0/refman/addendum/implicit-coercions.html#reversible-coercions

In a recent PR I changed all record projections from Coercion to :> because the syntax is more concise and I wanted to eliminate the boilerplate. There was only one breakage due to this change: if equiv_fun : Equiv >-> Funclass is declared reversible, then

(** The classifying space functor and the fundamental group functor form an adjunction ([pType] needs to be restricted to the subcategory of 0-connected pointed types). Note that the full adjunction should also be natural in [X], but this was not needed yet. *)
Theorem equiv_bg_pi1_adjoint `{Univalence} (X : pType)
  `{IsConnected 0 X} (G : Group)
  : (Pi 1 X $-> G) <~> (X $-> B G).
Proof.
  rapply natequiv_bg_pi1_adjoint.
Defined.

the rapply spins indefinitely when it tries to solve refine (natequiv_bg_pi1_adjoint _). Replacing it with

Definition equiv_bg_pi1_adjoint `{Univalence} (X : pType)
  `{IsConnected 0 X} (G : Group)
  : (Pi 1 X $-> G) <~> (X $-> B G).
  := natequiv_bg_pi1_adjoint _ _.

solves the problem.

Is this a change we should make? The syntax is more concise but I'm concerned that all these reversible coercions might add complexity to unification. On the other hand there was only one breakage.

[Alizter]

I think changing all of these to reversible coercions might seem harmless but they can cause problems down the road. I would rather we take a more conservative approach and use #[reversible=no] everywhere instead. That way we can switch them to be reversible with proper motivation in each case. We should do some more timing to work out if a specific coercion being reversible causes problems. I suspect that will be the case.

[patrick-nicodemus]

In that case IMO the change isn't worth making. My motivation was to eliminate boilerplate, but if the annotation is to be added everywhere then the notation is not much more concise.

[Alizter]

It could also be argued that Coercion is much easier to see compared to :> and is perhaps good to emphasise. We don't want coercions introduced without good reasons.

[jdchristensen]

I'd also lean toward just leaving the Coercion lines as they are.

[patrick-nicodemus]

As @jdchristensen suggested in a recent PR, several uses of :> in the codebase were added without realizing that they are reversible, and if we are not intentionally using them for anything then they might as well be removed to cut down on unnecessary complexity, so I have repurposed this issue to track that goal.