proposition: Lemma Codiese_map : forall a' : A, Map_law (CoUA_diese t (a':=a')).
proof: Proof. intros a'. unfold Map_law in |- *; intros f g H. apply (Prf_isCoUA_law2 t (f:=g) (g:=CoUA_diese t f)). unfold CoUA_eq in |- *. apply Trans with f. apply (Prf_isCoUA_law1 t f). assumption. Qed.
imports: UniversalArrow Dual_Functor