Lean4
/-- The category of functors `WithInitial C ⥤ D` is equivalent to the category
`Comma (const C) (𝟭 (C ⥤ D))`. -/
@[simps!]
def equivComma : (WithInitial C ⥤ D) ≌ Comma (Functor.const C) (𝟭 (C ⥤ D))
where
functor :=
{ obj := mkCommaObject
map := mkCommaMorphism }
inverse :=
{ obj := ofCommaObject
map := ofCommaMorphism }
unitIso :=
NatIso.ofComponents
(fun F ↦
liftUnique (incl ⋙ F) (fun x ↦ F.map (starInitial.to (of x)))
(fun x y f ↦ by
simp only [Functor.comp_obj, Functor.comp_map]
rw [← F.map_comp]
congr 1)
F (Iso.refl _) (Iso.refl _)
(fun x ↦ by
simp only [Iso.refl_symm, Iso.refl_hom, Category.id_comp, Functor.comp_obj, NatTrans.id_app,
Category.comp_id];
rfl))
(fun {x y} f ↦ by ext t; cases t <;> simp [incl])
counitIso := NatIso.ofComponents (fun F ↦ Iso.refl _)
functor_unitIso_comp
x :=
by
simp only [Functor.id_obj, Functor.comp_obj, liftUnique, lift_obj, NatIso.ofComponents_hom_app, Iso.refl_hom,
Category.comp_id]
ext <;> rfl
