Commit 2020-08-24 01:55 685d9dd3

View on Github →

feat(category_theory): cancel fully faithful functor (#3920) Construct the natural isomorphism between F and G given a natural iso between F ⋙ H and G ⋙ H for a fully faithful H.

Estimated changes

Modified src/category_theory/fully_faithful.lean

added def category_theory.fully_faithful_cancel_right

added theorem category_theory.fully_faithful_cancel_right_hom_app

added theorem category_theory.fully_faithful_cancel_right_inv_app