proposition: Lemma Fst_map_law : forall a b : PROD A B, Map_law (Hom_l (u:=a) (t:=b)).
proof: Proof. unfold Map_law in |- *. intros a b; unfold Equal at 1 in |- *; simpl in |- *. unfold Equal_Pmor in |- *; intros f g H. elim H; intros; assumption. Qed.
imports: PROD Functor