proposition: Lemma Cayley_Left (x y z w : C) (f : z ~> w) (g : y ~> z) (h : x ~> y) : (∀ a b (k : a ~{C}~> b), id[b] ∘ k = k) -> f ∘ g ∘ h = fmap[From_Cayley] (((fmap[To_Cayley] f ∘ fmap[To_Cayley] g) ∘ fmap[To_Cayley] h)).
proof: Proof. intros. simpl. rewrite H0. reflexivity. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Structure.Cartesian Category.Functor.Hom.Yoneda Category.Instance.Sets