+lemma Orelation_pair_composition_morphism_respects_id_r:
+Πo1:Obasic_pair
+.Πo2:Obasic_pair
+ .Πa:Orelation_pair_setoid o1 o2
+ .Orelation_pair_composition_morphism o1 o2 o2 a (Oid_relation_pair o2)=a.
+intros;
+ change with (⊩ ∘ ((Oid_relation_pair o2)\sub\c ∘ a\sub\c) = ⊩ ∘ a\sub\c);
+ apply ((id_neutral_left2 ????)‡#);
+qed.
+
+definition OBP: category2.
+ constructor 1;
+ [ apply Obasic_pair
+ | apply Orelation_pair_setoid
+ | apply Oid_relation_pair
+ | apply Orelation_pair_composition_morphism
+ | apply Orelation_pair_composition_morphism_assoc;
+ | apply Orelation_pair_composition_morphism_respects_id;
+ | apply Orelation_pair_composition_morphism_respects_id_r;]
+qed.
+
+definition Obasic_pair_of_objs2_OBP: objs2 OBP → Obasic_pair ≝ λx.x.
+coercion Obasic_pair_of_objs2_OBP.
+
+definition Orelation_pair_setoid_of_arrows2_OBP:
+ ∀P,Q.arrows2 OBP P Q → Orelation_pair_setoid P Q ≝ λP,Q,c.c.
+coercion Orelation_pair_setoid_of_arrows2_OBP.