proposition: Lemma PhiUA_1_o_PhiUA : AreIsos (PhiUA dxc) (PhiUA_1 dxc).
proof: Proof. unfold AreIsos in |- *; unfold RIso_law in |- *; simpl in |- *; split. unfold Ext in |- *; simpl in |- *. unfold PhiUA_arrow, Id_fun, PhiUA_1_arrow in |- *. intro f. unfold FunSET2_l_ob in |- *; apply UA_diag. unfold Ext in |- *; simpl in |- *. unfold PhiUA_arrow, Id_fun, PhiUA_1_arrow in |- *. intro f. unfold FunSET2_r_ob in |- *; simpl in |- *; unfold AdjointUA_ob in |- *. apply UA_unic1. apply Refl. Qed.
imports: Adj_UA