proposition: Lemma fun_equiv_fmap_from {C D : Category} {F G : C ⟶ D} (eqv : F ≈ G) : ∀ (x y : C) (f : x ~> y), fmap[F] f ∘ from (``eqv x) ≈ from (``eqv y) ∘ fmap[G] f.
proof: Proof. intros. rewrite <- id_left. rewrite ((`2 eqv) _ _). rewrite <- !comp_assoc. rewrite iso_to_from. now cat. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Equations.Prop.Logic