proposition: Lemma FunY_id_law : Fid_law0'' (C:=Dual C) FunY_map.
proof: Proof. unfold Fid_law0'' in |- *; simpl in |- *. unfold Equal_NT in |- *; simpl in |- *. unfold Ext in |- *; simpl in |- *. unfold NtH_arrow in |- *; simpl in |- *. unfold FunSET_ob in |- *. unfold Id_fun in |- *; simpl in |- *. intros a b f; unfold Comp in |- *; apply (Prf_idl (c:=C)). Qed.
imports: HomFunctor_NT CatFunct Functor_dup1