proposition: Lemma AdjointUA_id_law : Fid_law AdjointUA_map.
proof: Proof. unfold Fid_law in |- *; simpl in |- *. unfold AdjointUA_mor, AdjointUA_ob in |- *. intro d. apply UA_unic1. apply Trans with (UA_mor (UA_of d) o Id (G (UA_ob (UA_of d)))). apply Comp_l; apply FId. apply Trans with (UA_mor (UA_of d)). apply Idr1. apply Idl1. Qed.
imports: Adj_UA