proposition: Lemma CoadjointUA_id_law : Fid_law CoadjointUA_map.
proof: Proof. unfold Fid_law in |- *; simpl in |- *. unfold CoadjointUA_mor, CoadjointUA_ob in |- *. intro c. apply CoUA_unic1. apply Trans with (Id (F (CoUA_ob (UA_of c))) o CoUA_mor (UA_of c)). apply Comp_r; apply FId. apply Trans with (CoUA_mor (UA_of c)). apply Idl. apply Idr. Qed.
imports: Adj_UA