Obj component in `Cat`

Stream: mathlib4

[Dean Young]

Mathlib has Cat (which I've imported from Category.Cat). How do you access the object component of a particular term t : Cat?

[Jason Rute]

I think it is exposed via t.α. More specifically, docs#CategoryTheory.Cat is the type made up of every docs#CategoryTheory.Bundled t containing a type α : Type u and some category structure str : Category α on α. So t.α is the carrier (object component) for the category t.str. (Note, the carrier is not a data field in the class docs#CategoryTheory.Category, but a parameter of Category, which is why Cat and Bundle look the way they do.)

[Jason Rute]

import Mathlib.CategoryTheory.Category.Cat

#check fun (t : CategoryTheory.Cat) => ((t.α : Type _), (t.str : CategoryTheory.Category t.α))

[Eric Wieser]

I think you're supposed to just cast, which inserts the .α automatically:

import Mathlib.CategoryTheory.Category.Cat

#check fun t : CategoryTheory.Cat => ((t : Type _), (inferInstance : CategoryTheory.Category t))

[Dean Young]

Thanks this is great.