concrete categories

Stream: PR reviews

[Kim Morrison]

The following two related but independent PRs attempt to make life more confluent in concrete category land.

[Kim Morrison]

• #13055 chore(Algebra/Category): make coe_of a simp lemma in CommGroupCat

[Kim Morrison]

• #13108 chore(Algebra/Category/Ring): simp lemmas for coercions

[Kim Morrison]

In particular, I would like to make coe_of uniformly a @[simp] lemma across all concrete categories, and then install additional simp lemmas about coercions to handle the inevitable cases where we have partial unfolding of of X \hom of Y := X ->+* Y. The rule is basically "coercions of morphisms between of objects should be written as coercions of the underlying type".