Inhereting all instances for a definition

Stream: general

[Joey Eremondi]

I'm wondering, when I define a type as a specialization of another (parameterized) type, is there a way to inheret all of the instances from the original one?

For example, if I do:

import Mathlib.CategoryTheory.Arrow
import Mathlib.CategoryTheory.Types
open CategoryTheory

def Fam : Type 1 :=
 Arrow Type

def isoRefl (x : Fam) : x ≅ x := by _

I get the error

failed to synthesize instance
  Category.{?u.21, 1} Fam

even though Arrow Type has a Category instance.

Is there something I have to do to import the instances, or to declare Fam as transparent, so the typeclass checker sees that it's the same as Arrow Type? I could declare it as a notation instead of a definition, but is that the best way to do it?

[Jireh Loreaux]

Use abbrev instead of def

[Jireh Loreaux]

The former has reducible transparency, while the latter is semi-reducible

[Joey Eremondi]

Perfect, thanks!