proposition: Lemma Y_full : let f := fun (a b : C) (h : NT (FunSET a) (FunSET b)) => h a (Id a) in Full_law0'' (F:=FunY) f.
proof: Proof. unfold Full_law0'' in |- *; simpl in |- *; intros a b h. unfold Equal_NT in |- *; simpl in |- *. unfold Ext in |- *; simpl in |- *. unfold NtH_arrow in |- *. unfold FunSET_ob in |- *. intros c f; simpl in |- *. apply Trans with (h c (Id a o f)). apply Pres1. apply Sym; unfold Comp in |- *; simpl in |- *; unfold FunSET_ob in |- *; apply (Prf_idl (c:=C)). apply (Prf_NT_law h f (Id a)). Qed.
imports: HomFunctor_NT CatFunct Functor_dup1