Lean4
/-- Auxiliary definition:
the diagram whose limit gives the morphism space between two objects of the limit category. -/
@[simps]
def homDiagram {F : J ⥤ Cat.{v, v}} (X Y : limit (F ⋙ Cat.objects.{v, v})) : J ⥤ Type v
where
obj j := limit.π (F ⋙ Cat.objects) j X ⟶ limit.π (F ⋙ Cat.objects) j Y
map f
g := by
refine eqToHom ?_ ≫ (F.map f).map g ≫ eqToHom ?_
· exact (congr_fun (limit.w (F ⋙ Cat.objects) f) X).symm
· exact congr_fun (limit.w (F ⋙ Cat.objects) f) Y
map_id
X := by
funext f
letI : Category (objects.obj (F.obj X)) := (inferInstance : Category (F.obj X))
simp [Functor.congr_hom (F.map_id X) f]
map_comp {_ _ Z} f
g := by
funext h
letI : Category (objects.obj (F.obj Z)) := (inferInstance : Category (F.obj Z))
simp [Functor.congr_hom (F.map_comp f g) h, eqToHom_map]
