Relationship between typeclass and categorical hierarchy?

Stream: mathlib4

[Markus de Medeiros]

Suppose I have a hierarchy of typeclasses and morphisms

class {T: Type} A T where ...
structure AMor (S T : Type) [A S] [A T] where
class  {F S T : Type} AMorClass F S T [A S] [A T] extends (FunLike F S T) where ...

class {T : Type} B T extends A T where ...

structure CMor (S T : Type) [A S] [A T] extends (AMor S T) where
class  {F S T : Type} CMorClass F S T [A S] [A T] extends (AMorClass F S T) where ...

-- Instances and coercions elided

and then I bundle them to get a category.

def ACatObj := CategoryTheory.bundled A
def BCatObj := CategoryTheory.bundled B
instance CategoryTheory.bundledHom @AMor where ...
instance CategoryTheory.bundledHom @CMor where ...
-- 1/4:
def AAMorCat := ACatObj
instance CategoryTheory.LargeCategory @ACat := CategoryTheory.BundledHom.category @AMor

Aach pairing of (A/B)CatObj and (A/C)Mor forms a subcategory of ACat/AMor (I can prove this for the BCatObj+CMor case). How do I lift the results from my typeclass development, to these categories (eg. using the equations I've developed in terms of A, B, AMor and CMor). Is there some canonical way to mechanize this type of thing in mathlib? I could imagine hand-rolling coercions or functors between categories, but I'm not sure how that would scale if my typeclass hierarchy was deeper.

[Kim Morrison]

See Mathlib.Algebra.Category.Ring.Basic for the prototypical example. It is all pretty manual / boiler-plate-y.

[Eric Wieser]

The bundled approach also fails for things like ModuleCat or FinVec, where the typeclass takes more than a single argument

[Markus de Medeiros]

That's exactly what I was looking for, thanks for the link! Fortunately my structure has only one argument.