-alias symbol "eq" = "setoid1 eq".
-alias symbol "compose" = "category1 composition".
-record relation_pair (BP1,BP2: basic_pair): Type1 ≝
- { concr_rel: arrows1 ? (concr BP1) (concr BP2);
- form_rel: arrows1 ? (form BP1) (form BP2);
- commute: ⊩ ∘ concr_rel = form_rel ∘ ⊩
+record relation_pair (BP1,BP2: basic_pair): Type1 ≝ {
+ concr_rel: (concr BP1) ⇒_\r1 (concr BP2); form_rel: (form BP1) ⇒_\r1 (form BP2);
+ commute: ⊩ ∘ concr_rel =_1 form_rel ∘ ⊩