Lean4
/-- Transport a comonad structure on a functor along an isomorphism of functors. -/
def transport {F : C ⥤ C} (T : Comonad C) (i : (T : C ⥤ C) ≅ F) : Comonad C
where
toFunctor := F
ε := i.inv ≫ T.ε
δ := i.inv ≫ T.δ ≫ (i.hom ◫ i.hom)
right_counit
X := by
simp only [comp_obj, NatTrans.comp_app, NatTrans.hcomp_app, Functor.map_comp, assoc]
slice_lhs 4 5 => rw [← F.map_comp]
simp only [hom_inv_id_app, Functor.map_id, id_comp, ← i.hom.naturality]
slice_lhs 2 3 => rw [T.right_counit]
simp
coassoc
X :=
by
simp only [comp_obj, NatTrans.comp_app, NatTrans.hcomp_app, Functor.map_comp, assoc, NatTrans.naturality_assoc,
Functor.comp_map, hom_inv_id_app_assoc, NatIso.cancel_natIso_inv_left]
slice_lhs 3 4 => rw [← F.map_comp]
simp only [hom_inv_id_app, Functor.map_id, id_comp, assoc]
rw [← i.hom.naturality_assoc, ← T.coassoc_assoc]
simp only [NatTrans.naturality_assoc]
congr 3
simp only [← Functor.map_comp, i.hom.naturality]
