## Stream: Is there code for X?

### Topic: Category of diagrams

#### Adam Topaz (Mar 01 2021 at 22:02):

I'm looking for some construction of "the category of diagrams" along the following lines:

import category_theory.eq_to_hom
import category_theory.whiskering
import category_theory.essential_image

open category_theory

universes v u
variables (C : Type u) [category.{v} C]

@[ext]
structure diagram :=
(J : Type v)
[small_cat : small_category J]
(F : J ⥤ C)

namespace diagram

variable {C}

instance : has_coe_to_sort (diagram C) := ⟨Type v, λ X, X.J⟩
instance {X : diagram C} : small_category X := X.small_cat

@[ext]
structure hom (X Y : diagram C) :=
(i : X ⥤ Y)
(j : X.F.ess_image ⥤ Y.F.ess_image)
(comm : i ⋙ Y.F.to_ess_image ≅ X.F.to_ess_image ⋙ j)

@[simps]
def id (X : diagram C) : hom X X :=
{ i := functor.id _,
j := functor.id _,
comm :=
{ hom := 𝟙 _,
inv := 𝟙 _  } }

@[simps]
def comp {X Y Z : diagram C} (f : hom X Y) (g : hom Y Z) : hom X Z :=
{ i := f.i ⋙ g.i,
j := f.j ⋙ g.j,
comm :=
functor.associator f.i g.i _ ≪≫
iso_whisker_left f.i g.comm ≪≫
(functor.associator _ _ _).symm ≪≫
iso_whisker_right f.comm g.j ≪≫
functor.associator _ f.j g.j }

instance : category (diagram C) :=
{ hom := hom,
id := λ X, id _,
comp := λ X Y Z, comp,
id_comp' := begin
intros a b f,
ext,
{ apply category_theory.functor.ext, tidy },
{ apply category_theory.functor.ext, tidy },
recover,
tidy,
end,
comp_id' := begin
intros a b f,
ext,
{ apply category_theory.functor.ext, tidy },
{ apply category_theory.functor.ext, tidy },
recover,
tidy,
end,
assoc' := begin
intros a b c d f g h,
ext,
{ apply category_theory.functor.ext, tidy },
{ apply category_theory.functor.ext, tidy },
recover,
tidy,
end }

end diagram


And while I'm asking, I also don't really understand why recover is necessary in the last few proofs (I get an error if these lines are removed).
Finally, if someone has any ideas about how to make this construction less "evil" (due to the use of category_theory.functor.ext), that would also be helpful!

#### Scott Morrison (Mar 01 2021 at 23:20):

Isn't this construction just inherently 'evil'? There's a 2-category of diagrams that wouldn't be.

#### Adam Topaz (Mar 01 2021 at 23:21):

Yeah, youre right.

#### Adam Topaz (Mar 01 2021 at 23:23):

I just never imagined that something so mundane like the category of diagrams should really be a 2-category.

#### Adam Topaz (Mar 01 2021 at 23:25):

But I guess whenever you need to talk about commuting diagrams of functors, you're forced into 2-categories.

Last updated: May 16 2021 at 05:21 UTC