Lean4
/-- Equivalence of categories is transitive. -/
@[trans, simps]
def trans (e : C ≌ D) (f : D ≌ E) : C ≌ E
where
functor := e.functor ⋙ f.functor
inverse := f.inverse ⋙ e.inverse
unitIso :=
e.unitIso ≪≫
isoWhiskerRight (e.functor.rightUnitor.symm ≪≫ isoWhiskerLeft _ f.unitIso ≪≫ (Functor.associator _ _ _).symm) _ ≪≫
Functor.associator _ _ _
counitIso :=
(Functor.associator _ _ _).symm ≪≫
isoWhiskerRight ((Functor.associator _ _ _) ≪≫ isoWhiskerLeft _ e.counitIso ≪≫ f.inverse.rightUnitor) _ ≪≫
f.counitIso
functor_unitIso_comp
X := by
dsimp
simp only [comp_id, id_comp, map_comp, fun_inv_map, comp_obj, id_obj, counitInv, functor_unit_comp_assoc, assoc]
slice_lhs 2 3 => rw [← Functor.map_comp, Iso.inv_hom_id_app]
simp
