Bundled category and typeclass inference

Stream: new members

[Shanghe Chen]

Hi I am curious in the following code related to bundled category and typeclass inference:

import Mathlib.CategoryTheory.Functor.Basic
import Mathlib.CategoryTheory.ConcreteCategory.Bundled
import Mathlib.CategoryTheory.NatIso

noncomputable section
set_option autoImplicit false
universe v u
open CategoryTheory Functor

variable (C D: Bundled Category.{v, u})
#check C.α -- ↑C : Type u
#check C.str -- C.str : Category.{v, u} ↑C

-- The following three defs failed without this line
instance : Category C := C.str

def id_functor := 𝟭 D

def id_natiso (F: C ⥤ D) := 𝟙 F

def id_functor'(E: Bundled Category.{v, u}) := 𝟭 E

[Shanghe Chen]

Here C, D and E are bundled categories and F is a "bundled" functor between them. I found that if the line instance : Category C := C.str removed, then all the three defs failed. But how this line helps sythesizing/finding the categories that are in fact fields, especially in the case F and E?

[Shanghe Chen]

The mysterious part to me is that the line only gives an instance for C, whereas after it all instances for D and E can be found.

[Joël Riou]

The declaration instance : Category C := ... applies to any C : Bundled Category: this is the way definitions work in Lean.
On the contrary, inside a definition:

example (C D : Bundled Category) : False := by
  letI : Category C := C.str
  -- here, only `C` is equipped with a category structure
  sorry

[Shanghe Chen]

Ah indeed it’s the case. I get it now.

def id_functor := by
  letI : Category D := D.str
  exact 𝟭 D

does also work

[Shanghe Chen]

From https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Structure.20fields.20as.20instances.3F I see that attribute [instance] Bundled.str also works