Cat.lean

/-
Copyright (c) 2019 Yury Kudryashov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yury Kudryashov
-/

import category_theory.concrete_category

/-!
# Category of categories

This file contains definition of 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.
-/

universes v u

namespace category_theory

/-- Category of categories. -/
def Cat := bundled category.{v u}

namespace Cat

instance str (C : Cat.{v u}) : category.{v u} C.α := C.str

/-- Construct a bundled `Cat` from the underlying type and the typeclass. -/
def of (C : Type u) [category.{v} C] : Cat.{v u} := bundled.of C

/-- Category structure on `Cat` -/
instance category : large_category.{max v u} Cat.{v u} :=
{ hom := λ C D, C.α ⥤ D.α,
  id := λ C, 𝟭 C.α,
  comp := λ C D E F G, F ⋙ G,
  id_comp' := λ C D F, by cases F; refl,
  comp_id' := λ C D F, by cases F; refl,
  assoc' := by intros; refl }

/-- Functor that gets the set of objects of a category. It is not
called `forget`, because it is not a faithful functor. -/
def objects : Cat.{v u} ⥤ Type u :=
{ obj := bundled.α,
  map := λ C D F, F.obj }

end Cat

end category_theory