Commit 2019-07-22 08:00 7c09ed5e

feat(category_theory/*): define Cat and a fully faithful functor Mon ⥤ Cat (#1235)

• feat(category_theory/*): define Cat and a fully faithful functor Mon ⥤ Cat
• Drop 2 commas
• Drop functor.id_comp etc, add Cat.str instance, adjust module-level comments
• Make α and β arguments of map_hom_equiv explicit This way e α β f is automatically interpreted as (e α β).to_fun f.