proposition: Lemma preyoneda {C : Category} {c d: C} {P : C^op ⟶ Sets} (τ : [Hom ─ , c] ⟹ P) : forall f : d ~> c, transform τ d f ≈ fmap[P] f (transform τ c id{C}).
proof: Proof. intro f. rewrite <- (id_left f) at 1. exact (symmetry (naturality τ _ d f) id{C}). 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.Functor.Hom.Yoneda Category.Instance.Sets Category.Construction.Groupoid