Category of diagrams

Stream: Is there code for X?

[Adam Topaz]

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]

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

[Adam Topaz]

Yeah, youre right.

[Adam Topaz]

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

[Adam Topaz]

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