# mathlibdocumentation

category_theory.category.Cat

# Category of categories

This file contains the definition of the category Cat of all categories. In this category objects are categories and morphisms are functors between these categories.

## Implementation notes

Though Cat is not a concrete category, we use bundled to define its carrier type.

def category_theory.Cat  :
Type (max (u+1) u (v+1))

Category of categories.

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations

Construct a bundled Cat from the underlying type and the typeclass.

Equations
@[instance]

Category structure on Cat

Equations

Functor that gets the set of objects of a category. It is not called forget, because it is not a faithful functor.

Equations

Any isomorphism in Cat induces an equivalence of the underlying categories.

Equations
@[simp]
theorem category_theory.Type_to_Cat_map (X Y : Type u) (f : X Y) :

Embedding Type into Cat as discrete categories.

This ought to be modelled as a 2-functor!

Equations
@[simp]
theorem category_theory.Type_to_Cat_obj (X : Type u) :

@[instance]

Equations