proposition: Lemma PsiUA_1_o_PsiUA : AreIsos (PsiUA dxc) (PsiUA_1 dxc).
proof: Proof. unfold AreIsos, RIso_law in |- *; simpl in |- *; split. unfold Ext in |- *; simpl in |- *. unfold PsiUA_arrow, Id_fun, PsiUA_1_arrow in |- *. intro f. unfold FunSET2_l_ob in |- *; simpl in |- *; unfold CoadjointUA_ob in |- *. apply CoUA_unic1; apply Refl. unfold Ext in |- *; simpl in |- *. unfold PsiUA_arrow, Id_fun, PsiUA_1_arrow in |- *. intro f. unfold FunSET2_r_ob in |- *; apply (CoUA_diag (UA_of (Ob_r dxc))). Qed.
imports: Adj_UA