proposition: Lemma YLpsi_nt_law : forall (a a' : C) (g : a --> a') (F F' : Functor C SET) (T : NT F F') (x : F a) (b : C) (f : a' --> b), YLpsi_tau a' F' ((FMor F g o T a') x) b f =_S (NtH g o_NTv YLpsi_tau a F x o_NTv T) b f.
proof: Proof. intros a a' g F F' T x b f. unfold YLpsi_tau in |- *; simpl in |- *; unfold Comp_fun in |- *; simpl in |- *. unfold YLpsi_arrow1, NtH_arrow in |- *. apply Trans with (T b (FMor F f (FMor F g x))). generalize (Prf_NT_law T f (FMor F g x)). unfold NT_law in |- *; simpl in |- *; unfold Comp_fun in |- *; intro H. apply Sym; apply H. apply Pres1; apply Sym; apply (Prf_Fcomp_law F g f x). Qed.
imports: HomFunctor_NT CatFunct Functor_dup1