porting CategoryTheory.ConcreteCategory.BundledHom

Stream: mathlib4

[Moritz Firsching]

In mathlib4#2740, in mkHasForget₂ two things are not working:

/-- A version of `HasForget₂.mk'` for categories defined using `@BundledHom`. -/
def mkHasForget₂ {d : Type u → Type u} {hom_d : ∀ ⦃α β : Type u⦄ (Iα : d α) (Iβ : d β), Type u}
    [BundledHom hom_d] (obj : ∀ ⦃α⦄, c α → d α)
    (map : ∀ {X Y : Bundled c}, (X ⟶ Y) → ((Bundled.map obj X) ⟶ (Bundled.map obj Y)))
    (h_map : ∀ {X Y : Bundled c} (f : X ⟶ Y), (map f) = f) :
    HasForget₂ (Bundled c) (Bundled d) :=
  HasForget₂.mk' (Bundled.map @obj) (fun _ => rfl) (@map)
    (by intros <;> apply hEq_of_eq <;> apply h_map)
#align category_theory.bundled_hom.mk_has_forget₂ CategoryTheory.BundledHom.mkHasForget₂

Here the error for obj Y is

type mismatch
  obj
has type
  ⦃α : Type u⦄ → c α → d α : Type (u + 1)
but is expected to have type
  c α✝ → ?m.7687 α✝ : Type u

But for obj X there is no type mismatch, although X and Y are of the same type. I suspect fixing this will also fix the other problem in h_map.
What is going on?

[Joël Riou]

It was only a problem with the difference between ⦃α⦄ and {α}. For h_map, looking at the original code in mathlib would help finding that we actually wanted to state ⇑map f = ⇑f, i.e. an equality between the associated coerced functions. I have fixed that.