mathlib

685d9dd3 - feat(category_theory): cancel fully faithful functor (#3920)

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`. Co-authored-by: Thomas Read <thjread@gmail.com>