proposition: Lemma FunSET_map_law : Map_law FunSET_mor.
proof: Proof. unfold Map_law in |- *; simpl in |- *. unfold Ext in |- *; simpl in |- *. unfold FunSET_mor1, FunSET_ob in |- *. intros f g H h. apply Comp_l; assumption. Qed.
imports: SET Functor Dual