proposition: Proposition fmap_respects' (x y : D) (f g : x ~> y) : f ≈ g -> fmap[U] f ≈ fmap[U] g.
proof: Proof. Proof using Type. apply fmap_respects. Qed.
imports: Category.Lib Category.Lib.Tactics2 Category.Theory.Category Category.Theory.Isomorphism Category.Construction.Opposite Category.Theory.Functor Category.Theory.Natural.Transformation Category.Functor.Hom Category.Instance.Sets Category.Structure.UniversalProperty Category.Theory.Universal.Arrow