- apply (equal_morphism ???? (r\sub\c ∘ (r1\sub\c ∘ ⊩)) ? ((⊩ ∘ r\sub\f) ∘ r1\sub\f));
- [1,2: apply associative_composition]
- apply (equal_morphism ???? (r\sub\c ∘ (⊩ ∘ r1\sub\f)) ? ((r\sub\c ∘ ⊩) ∘ r1\sub\f));
- [1,2: apply composition_morphism; first [assumption | apply refl_equal_relations]
- | apply sym_equal_relations;
- apply associative_composition
- ]]
- | intros;
- alias symbol "eq" = "equal relation".
- change with (a\sub\c ∘ b\sub\c ∘ ⊩ = a'\sub\c ∘ b'\sub\c ∘ ⊩);
- apply (equal_morphism ???? (a\sub\c ∘ (b\sub\c ∘ ⊩)) ? (a'\sub\c ∘ (b'\sub\c ∘ ⊩)));
- [ apply associative_composition
- | apply sym_equal_relations; apply associative_composition]
- apply (equal_morphism ???? (a\sub\c ∘ (b'\sub\c ∘ ⊩)) ? (a' \sub \c∘(b' \sub \c∘⊩)));
- [2: apply refl_equal_relations;
- |1: apply composition_morphism;
- [ apply refl_equal_relations
- | assumption]]
- apply (equal_morphism ???? (a\sub\c ∘ (⊩ ∘ b'\sub\f)) ? (a'\sub\c ∘ (⊩ ∘ b'\sub\f)));
- [1,2: apply composition_morphism;
- [1,3: apply refl_equal_relations
- | apply (commute ?? b');
- | apply sym_equal_relations; apply (commute ?? b');]]
- apply (equal_morphism ???? ((a\sub\c ∘ ⊩) ∘ b'\sub\f) ? ((a'\sub\c ∘ ⊩) ∘ b'\sub\f));
- [2: apply associative_composition
- |1: apply sym_equal_relations; apply associative_composition]
- apply composition_morphism;
- [ assumption
- | apply refl_equal_relations]]
+ alias symbol "trans" = "trans1".
+ alias symbol "assoc" = "category1 assoc".
+ apply (.= ASSOC);
+ apply (.= #‡H1);
+ alias symbol "invert" = "setoid1 symmetry".
+ apply (.= ASSOC ^ -1);
+ apply (.= H‡#);
+ apply ASSOC]
+qed.
+
+lemma relation_pair_composition_is_morphism:
+ ∀o1,o2,o3: basic_pair.
+ ∀a,a':relation_pair_setoid o1 o2.
+ ∀b,b':relation_pair_setoid o2 o3.
+ a=a' → b=b' →
+ relation_pair_composition o1 o2 o3 a b
+ = relation_pair_composition o1 o2 o3 a' b'.
+intros 3 (o1 o2 o3);
+ intros;
+ change with (⊩ ∘ (b\sub\c ∘ a\sub\c) = ⊩ ∘ (b'\sub\c ∘ a'\sub\c));
+ change in e with (⊩ ∘ a \sub\c = ⊩ ∘ a' \sub\c);
+ change in e1 with (⊩ ∘ b \sub\c = ⊩ ∘ b' \sub\c);
+ apply (.= ASSOC);
+ apply (.= #‡e1);
+ apply (.= #‡(commute ?? b'));
+ apply (.= ASSOC ^ -1);
+ apply (.= e‡#);
+ apply (.= ASSOC);
+ apply (.= #‡(commute ?? b')^-1);
+ apply (ASSOC ^ -1);
+qed.
+
+definition relation_pair_composition_morphism:
+ ∀o1,o2,o3. binary_morphism1 (relation_pair_setoid o1 o2) (relation_pair_setoid o2 o3) (relation_pair_setoid o1 o3).
+ intros;
+ constructor 1;
+ [ apply relation_pair_composition;
+ | apply relation_pair_composition_is_morphism;]
+qed.
+
+lemma relation_pair_composition_morphism_assoc:
+Πo1:basic_pair
+.Πo2:basic_pair
+ .Πo3:basic_pair
+ .Πo4:basic_pair
+ .Πa12:relation_pair_setoid o1 o2
+ .Πa23:relation_pair_setoid o2 o3
+ .Πa34:relation_pair_setoid o3 o4
+ .relation_pair_composition_morphism o1 o3 o4
+ (relation_pair_composition_morphism o1 o2 o3 a12 a23) a34
+ =relation_pair_composition_morphism o1 o2 o4 a12
+ (relation_pair_composition_morphism o2 o3 o4 a23 a34).
+ intros;
+ change with (⊩ ∘ (a34\sub\c ∘ (a23\sub\c ∘ a12\sub\c)) =
+ ⊩ ∘ ((a34\sub\c ∘ a23\sub\c) ∘ a12\sub\c));
+ alias symbol "refl" = "refl1".
+ alias symbol "prop2" = "prop21".
+ apply (ASSOC‡#);
+qed.
+
+lemma relation_pair_composition_morphism_respects_id:
+ ∀o1,o2:basic_pair.∀a:relation_pair_setoid o1 o2.
+ relation_pair_composition_morphism o1 o1 o2 (id_relation_pair o1) a=a.
+ intros;
+ change with (⊩ ∘ (a\sub\c ∘ (id_relation_pair o1)\sub\c) = ⊩ ∘ a\sub\c);
+ apply ((id_neutral_right1 ????)‡#);
+qed.
+
+lemma relation_pair_composition_morphism_respects_id_r:
+ ∀o1,o2:basic_pair.∀a:relation_pair_setoid o1 o2.
+ relation_pair_composition_morphism o1 o2 o2 a (id_relation_pair o2)=a.
+ intros;
+ change with (⊩ ∘ ((id_relation_pair o2)\sub\c ∘ a\sub\c) = ⊩ ∘ a\sub\c);
+ apply ((id_neutral_left1 ????)‡#);