Lean4
/-- A natural transformation `α : F ⟶ G` between functors `F G : C ⥤ Cat` which is final on each
fiber `(α.app X)` induces an equivalence of fiberwise colimits of `map α ⋙ H` and `H` for each
functor `H : Grothendieck G ⥤ Type`. -/
def fiberwiseColimitMapCompEquivalence {C : Type u₁} [Category.{v₁} C] {F G : C ⥤ Cat.{v₂, u₂}} (α : F ⟶ G)
[∀ X, Final (α.app X)] (H : Grothendieck G ⥤ Type u₂) : fiberwiseColimit (map α ⋙ H) ≅ fiberwiseColimit H :=
NatIso.ofComponents
(fun X =>
HasColimit.isoOfNatIso
((Functor.associator _ _ _).symm ≪≫ isoWhiskerRight (ιCompMap α X) H ≪≫ Functor.associator _ _ _) ≪≫
Final.colimitIso (α.app X) (ι G X ⋙ H))
(fun f =>
colimit.hom_ext <| fun d =>
by
simp only [map, Cat.comp_obj, comp_obj, ι_obj, fiberwiseColimit_obj, fiberwiseColimit_map, ιNatTrans, ιCompMap,
Iso.trans_hom, Category.assoc, ι_colimMap_assoc, NatTrans.comp_app, whiskerRight_app, Functor.comp_map,
Cat.eqToHom_app, map_id, Category.comp_id, associator_hom_app, colimit.ι_pre_assoc,
HasColimit.isoOfNatIso_ι_hom_assoc, Iso.symm_hom, isoWhiskerRight_hom, associator_inv_app,
NatIso.ofComponents_hom_app, Iso.refl_hom, Final.ι_colimitIso_hom, Category.id_comp,
Final.ι_colimitIso_hom_assoc, colimit.ι_pre]
have := Functor.congr_obj (α.naturality f) d
dsimp at this
congr
apply eqToHom_heq_id_dom)
