-record relation_pair (BP1,BP2: basic_pair): Type ≝
- { concr_rel: arrows1 ? (concr BP1) (concr BP2);
- form_rel: arrows1 ? (form BP1) (form BP2);
+record relation_pair (BP1,BP2: basic_pair): Type2 ≝
+ { concr_rel: arrows2 ? (concr BP1) (concr BP2);
+ form_rel: arrows2 ? (form BP1) (form BP2);