Synthesize typeclass bundled inside structure

Stream: lean4

[Chris Henson]

Consider the following mwe:

class C : Type
class F [C] : Type

structure bundle where
  instC : C

-- this works fine, but can be cumbersome with a few typeclasses
def f (b : bundle) (f : @F b.instC) : Type := sorry

-- failed to synthesize C
def f' (b : bundle) (f : F) : Type := sorry

Completely possible this is an #xy question, the context is my question here: #mathlib4 > Category of Cartesian closed categories

[Eric Wieser]

attribute [instance] bundle.C might fix it

[Eric Wieser]

Though I think this is overly minimized; in your real example, does instC reference other fields of bundle?

[Chris Henson]

That does seem to work. This is the direction I was headed:

import Mathlib

open CategoryTheory Limits CartesianClosed

structure CCCat.{u, v} where
  obj : Type u
  instCategory: Category.{v, u} obj
  instHasFiniteProducts : HasFiniteProducts.{v, u} obj
  instCartesianClosed : CartesianClosed.{v, u} obj

attribute [instance] CCCat.instCategory
attribute [instance] CCCat.instHasFiniteProducts
attribute [instance] CCCat.instCartesianClosed

structure CCHom (C : CCCat) (D : CCCat) where
  F : C.obj ⥤ D.obj
  instPreservesLimitsOfShape : PreservesLimitsOfShape (Discrete WalkingPair) F
  instCartesianClosedFunctor : CartesianClosedFunctor F

instance : Category CCCat where
  Hom := CCHom
  id := sorry
  comp := sorry
  id_comp := sorry
  comp_id := sorry

[Eric Wieser]

That looks correct to me

[Eric Wieser]

The key thing is that for attribute [instance] Foo.bar to be reasonable, you need Foo.bar (f : Foo) : SomeClass (X f), so that the instance is keyed on the type of f

[Chris Henson]

Makes sense, I see that instance (C : CCCat) : Category C.obj := C.instCategory etc. also works

[Eric Wieser]

That's not quite as good because now you have two names for the same thing!

[Chris Henson]

Yeah yours is better, that's what I went with! attribute is very nice in giving more direct control over what is (or isn't) an instance.