+
+definition concrete_space_of_CSPA : objs2 CSPA → concrete_space ≝ λx.x.
+coercion concrete_space_of_CSPA.
+
+definition convergent_relation_space_setoid_of_arrows2_CSPA :
+ ∀P,Q. arrows2 CSPA P Q → convergent_relation_space_setoid P Q ≝ λP,Q,x.x.
+coercion convergent_relation_space_setoid_of_arrows2_CSPA.
+