proposition: Proposition fmap_respects' (C D : Category) (F : C ⟶ D) : forall (x y : C) (f g: hom x y), f ≈ g -> fmap[F] f ≈ fmap[F] g.
proof: Proof. now apply fmap_respects. Defined.
imports: Category.Lib Category.Theory.Category Category.Theory.Functor Category.Theory.Natural.Transformation Category.Instance.Sets Category.Instance.Fun Category.Structure.Cartesian Category.Lib.Tactics2