Commit 2023-02-15 17:16 dfb03545

View on Github →

feat: port CategoryTheory.Types (#2294)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Types.lean

added def CategoryTheory.Functor.sections

added theorem CategoryTheory.FunctorToTypes.comp

added theorem CategoryTheory.FunctorToTypes.hcomp

added theorem CategoryTheory.FunctorToTypes.hom_inv_id_app_apply

added theorem CategoryTheory.FunctorToTypes.inv_hom_id_app_apply

added theorem CategoryTheory.FunctorToTypes.map_comp_apply

added theorem CategoryTheory.FunctorToTypes.map_hom_map_inv_apply

added theorem CategoryTheory.FunctorToTypes.map_id_apply

added theorem CategoryTheory.FunctorToTypes.map_inv_map_hom_apply

added theorem CategoryTheory.FunctorToTypes.naturality

added def CategoryTheory.Iso.toEquiv

added theorem CategoryTheory.Iso.toEquiv_comp

added theorem CategoryTheory.Iso.toEquiv_fun

added theorem CategoryTheory.Iso.toEquiv_id

added theorem CategoryTheory.Iso.toEquiv_symm_fun

added theorem CategoryTheory.epi_iff_surjective

added def CategoryTheory.homOfElement

added theorem CategoryTheory.homOfElement_eq_iff

added theorem CategoryTheory.hom_inv_id_apply

added theorem CategoryTheory.injective_of_mono

added theorem CategoryTheory.inv_hom_id_apply

added theorem CategoryTheory.isIso_iff_bijective

added theorem CategoryTheory.mono_iff_injective

added def CategoryTheory.ofTypeFunctor

added theorem CategoryTheory.ofTypeFunctor_map

added theorem CategoryTheory.ofTypeFunctor_obj

added theorem CategoryTheory.surjective_of_epi

added theorem CategoryTheory.types_comp

added theorem CategoryTheory.types_comp_apply

added theorem CategoryTheory.types_hom

added theorem CategoryTheory.types_id

added theorem CategoryTheory.types_id_apply

added def CategoryTheory.uliftFunctor

added def CategoryTheory.uliftFunctorTrivial

added theorem CategoryTheory.uliftFunctor_map

added def CategoryTheory.uliftTrivial

added def Equiv.toIso

added theorem Equiv.toIso_hom

added theorem Equiv.toIso_inv

added def equivEquivIso

added theorem equivEquivIso_hom

added theorem equivEquivIso_inv

added def equivIsoIso