∀P,Q. arrows2 OCSPA P Q → Oconvergent_relation_space_setoid P Q ≝ λP,Q,x.x.
coercion Oconvergent_relation_space_setoid_of_arrows2_OCSPA.
∀P,Q. arrows2 OCSPA P Q → Oconvergent_relation_space_setoid P Q ≝ λP,Q,x.x.
coercion Oconvergent_relation_space_setoid_of_arrows2_OCSPA.