proposition: Lemma FunY_comp_law : Fcomp_law0'' (C:=Dual C) FunY_map.
proof: Proof. unfold Fcomp_law0'' in |- *; simpl in |- *. unfold Equal_NT in |- *; simpl in |- *. unfold Ext in |- *; simpl in |- *. unfold NtH_arrow in |- *; simpl in |- *. unfold FunSET_ob, DHom in |- *. intros a b c f g d h; apply Sym. exact (Prf_ass g f h). Qed.
imports: HomFunctor_NT CatFunct Functor_dup1