mathlib3

b59f777c - feat(category_theory/eq_to_hom): functor extensionality using heq (#2712)

feat(category_theory/eq_to_hom): functor extensionality using heq (#2712) Used in https://github.com/rwbarton/lean-homotopy-theory. Also proves `faithful.div_comp`, but using it would create an import loop so for now I just leave a comment.