fix(category_theory/concrete): access the carrier type by the coercion (

#2473)

This should marginally reduce the pain of using concrete categories, as the underlying types of a bundled object should more uniformly described via a coercion, rather than the `.α` projection.

(There's still some separate pain involving `bundled.map`, but it has an orthogonal fix which I'm working on in another branch.)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/category_theory/concrete_category/bundled.lean

@@ -35,6 +35,8 @@ def of {c : Type u → Type v} (α : Type u) [str : c α] : bundled c := ⟨α,
 instance : has_coe_to_sort (bundled c) :=
 { S := Type u, coe := bundled.α }
 
+@[simp]
+lemma coe_mk (α) (str) : (@bundled.mk c α str : Type u) = α := rfl
 
 /-
 `bundled.map` is reducible so that, if we define a category
@@ -47,7 +49,7 @@ a (semi)ring homomorphism from R.α to S.α, and not merely from
 -/
 /-- Map over the bundled structure -/
 @[reducible] def map (f : Π {α}, c α → d α) (b : bundled c) : bundled d :=
-⟨b.α, f b.str⟩
+⟨b, f b.str⟩
 
 end bundled
 

src/category_theory/concrete_category/bundled_hom.lean

@@ -50,7 +50,7 @@ This instance generates the type-class problem `bundled_hom ?m` (which is why th
 `[nolint]`). Currently that is not a problem, as there are almost no instances of `bundled_hom`. -/
 @[nolint dangerous_instance] instance category : category (bundled c) :=
 by refine
-{ hom := λ X Y, @hom X.1 Y.1 X.str Y.str,
+{ hom := λ X Y, @hom X Y X.str Y.str,
   id := λ X, @bundled_hom.id c hom 𝒞 X X.str,
   comp := λ X Y Z f g, @bundled_hom.comp c hom 𝒞 X Y Z X.str Y.str Z.str g f,
   comp_id' := _,