Commit 2023-02-11 14:45 ef02d663

View on Github →

feat port/CategoryTheory.EqToHom (#2207)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/EqToHom.lean

added theorem CategoryTheory.Functor.congr_hom

added theorem CategoryTheory.Functor.congr_inv_of_congr_hom

added theorem CategoryTheory.Functor.congr_map

added theorem CategoryTheory.Functor.congr_obj

added theorem CategoryTheory.Functor.conj_eqToHom_iff_hEq

added theorem CategoryTheory.Functor.ext

added theorem CategoryTheory.Functor.hcongr_hom

added theorem CategoryTheory.Functor.hext

added theorem CategoryTheory.Functor.map_comp_hEq

added theorem CategoryTheory.Functor.map_comp_heq'

added theorem CategoryTheory.Functor.postcomp_map_hEq

added theorem CategoryTheory.Functor.postcomp_map_heq'

added theorem CategoryTheory.Functor.precomp_map_hEq

added theorem CategoryTheory.NatTrans.congr

added theorem CategoryTheory.comp_eqToHom_iff

added theorem CategoryTheory.congrArg_cast_hom_left

added theorem CategoryTheory.congrArg_cast_hom_right

added theorem CategoryTheory.congrArg_mpr_hom_left

added theorem CategoryTheory.congrArg_mpr_hom_right

added theorem CategoryTheory.dcongr_arg

added def CategoryTheory.eqToHom

added theorem CategoryTheory.eqToHom_app

added theorem CategoryTheory.eqToHom_comp_iff

added theorem CategoryTheory.eqToHom_map

added theorem CategoryTheory.eqToHom_op

added theorem CategoryTheory.eqToHom_refl

added theorem CategoryTheory.eqToHom_trans

added theorem CategoryTheory.eqToHom_unop

added theorem CategoryTheory.eqToIso.hom

added theorem CategoryTheory.eqToIso.inv

added def CategoryTheory.eqToIso

added theorem CategoryTheory.eqToIso_map

added theorem CategoryTheory.eqToIso_refl

added theorem CategoryTheory.eqToIso_trans

added theorem CategoryTheory.eq_conj_eqToHom

added theorem CategoryTheory.inv_eqToHom