/
Cat.lean
52 lines (37 loc) · 1.26 KB
/
Cat.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
/-
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
def of (C : Type u) [category.{v} C] : Cat.{v u} := mk_ob 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