proposition: Lemma FunY_map_law : Map_law0'' (NtH (C:=C) (b:=a) (a:=b)).
proof: Proof. unfold Map_law0'', NtH in |- *; simpl in |- *. unfold Equal_NT in |- *; simpl in |- *. unfold Ext in |- *; simpl in |- *. unfold NtH_arrow in |- *; simpl in |- *. unfold FunSET_ob in |- *; intros. apply Comp_r; assumption. Qed.
imports: HomFunctor_NT CatFunct Functor_dup1