Commit 2023-02-21 09:26 a702d4a0

View on Github →

feat: port CategoryTheory.Sums.Basic (#2246)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Sums/Basic.lean

added def CategoryTheory.Functor.sum

added theorem CategoryTheory.Functor.sum_map_inl

added theorem CategoryTheory.Functor.sum_map_inr

added theorem CategoryTheory.Functor.sum_obj_inl

added theorem CategoryTheory.Functor.sum_obj_inr

added def CategoryTheory.NatTrans.sum

added theorem CategoryTheory.NatTrans.sum_app_inl

added theorem CategoryTheory.NatTrans.sum_app_inr

added def CategoryTheory.Sum.Swap.equivalence

added def CategoryTheory.Sum.Swap.symmetry

added def CategoryTheory.Sum.inl_

added def CategoryTheory.Sum.inr_

added def CategoryTheory.Sum.swap

added theorem CategoryTheory.Sum.swap_map_inl

added theorem CategoryTheory.Sum.swap_map_inr

added theorem CategoryTheory.Sum.swap_obj_inl

added theorem CategoryTheory.Sum.swap_obj_inr

added theorem CategoryTheory.sum_comp_inl

added theorem CategoryTheory.sum_comp_inr