proposition: Lemma YonedaLemma : forall (a : C) (F : Functor C SET), AreBij0'' (YLpsi_tau a F) (YLphi_tau a F).
proof: Proof. intros a F; unfold AreBij0'' in |- *; split; simpl in |- *. intro x; unfold YLphi_arrow in |- *; simpl in |- *; unfold YLpsi_arrow1 in |- *. apply Trans with (Id (F a) x). apply (Prf_Fid_law F a x). apply Refl. intro T; unfold YLpsi_arrow, Equal_NT in |- *; simpl in |- *. intro b; unfold YLpsi_map1, Ext in |- *; simpl in |- *. unfold FunSET_ob in |- *; intro f. unfold YLpsi_arrow1, YLphi_arrow in |- *. generalize (Prf_NT_law T f (Id a)). simpl in |- *; unfold Comp_fun in |- *; simpl in |- *; unfold FunSET_mor1 in |- *; intro H. apply Trans with (T b (Id a o f)). apply Sym; exact H. apply Pres1; apply Idl. Qed.
imports: HomFunctor_NT CatFunct Functor_dup1