proposition: Lemma AdjointUA_map_law : Map_law AdjointUA_mor.
proof: Proof. unfold Map_law, AdjointUA_mor in |- *; intros f g H. apply (Diese_map (UA_of d) (x:=f o UA_mor (UA_of d')) (y:=g o UA_mor (UA_of d'))). apply Comp_r; assumption. Qed.
imports: Adj_UA