identity functor in Cat.{u₀,v₀}

Stream: lean4

[Dean Young]

This code gives me an error message:

invalid field 'obj', the environment does not contain 'Quiver.Hom.obj'
  𝟙 C
has type
  C ⟶ C

variable {C : Cat.{u₀,v₀}}
#check (𝟙 C).obj

Is seems it didn't infer the full functor but instead only a quantale. All this time I thought it was inferring the full functor.

[Dean Young]

Here's a similar error:

invalid field notation, type is not of the form (C ...) where C is a constant
  𝟙 (AdjComDom φ)
has type
  CategoryStruct.toQuiver.1 (AdjComDom φ) (AdjComDom φ)

It should have type functor but it's not inferring it.

[Adam Topaz]

#mwe

[Dean Young]

This is the smallest portion of code which produces the "just a quiver" error:

variable {C : Cat}
#check (𝟙 C)
#check (𝟙 C).obj

I just need the identity functor is all but it won't infer it.

[Jason Rute]

It’s not a #mwe if you don’t have all the imports

[Adam Topaz]

import Mathlib.CategoryTheory.Category.Cat

open CategoryTheory

variable (C : Cat)

#check (𝟙 C : C ⥤ C).obj

[Adam Topaz]

The issue you're facing is that Lean4 considers 𝟙 C as a morphism in Cat, as opposed to a functor. Of course morphisms in Cat are defined as the type of functors, but Lean4 has a hard time distinguishing the two without hints. If you want the identity functor as a functor, you can use 𝟭 C. E.g.:

import Mathlib.CategoryTheory.Category.Cat

open CategoryTheory

variable (C : Cat)

example : 𝟙 C = 𝟭 C := rfl