-
-definition BP: category2.
- constructor 1;
- [ apply basic_pair
- | apply relation_pair_setoid
- | apply id_relation_pair
- | apply relation_pair_composition
- | intros;
+
+definition Orelation_pair_composition_morphism:
+ ∀o1,o2,o3. binary_morphism2 (Orelation_pair_setoid o1 o2) (Orelation_pair_setoid o2 o3) (Orelation_pair_setoid o1 o3).
+intros; constructor 1;
+[ apply Orelation_pair_composition;
+| apply Orelation_pair_composition_is_morphism;]
+qed.
+
+lemma Orelation_pair_composition_morphism_assoc:
+∀o1,o2,o3,o4:Obasic_pair
+ .Πa12:Orelation_pair_setoid o1 o2
+ .Πa23:Orelation_pair_setoid o2 o3
+ .Πa34:Orelation_pair_setoid o3 o4
+ .Orelation_pair_composition_morphism o1 o3 o4
+ (Orelation_pair_composition_morphism o1 o2 o3 a12 a23) a34
+ =Orelation_pair_composition_morphism o1 o2 o4 a12
+ (Orelation_pair_composition_morphism o2 o3 o4 a23 a34).
+ intros;