proposition: Lemma YLphi_nt_law : forall (a a' : C) (g : a --> a') (F F' : Functor C SET) (T : NT F F') (U : NT (FunSET a) F), YLphi_tau a' F' (NtH g o_NTv U o_NTv T) =_S (FMor F g o T a') (YLphi_tau a F U).
proof: Proof. intros a a' g F F' T U. unfold YLphi_tau in |- *; simpl in |- *; unfold YLphi_arrow in |- *; simpl in |- *. unfold NtH_arrow, Comp_fun in |- *. apply Pres1. apply Trans with (U a' (Id a o g)). apply Pres1. simpl in |- *; unfold FunSET_ob in |- *. apply Idrl. apply (Prf_NT_law U g (Id a)). Qed.
imports: HomFunctor_NT CatFunct Functor_dup1