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 ∘ ⊩
+ commute: comp1 REL ??? concr_rel (rel ?) =_1 form_rel ∘ ⊩
}.
interpretation "concrete relation" 'concr_rel r = (concr_rel ?? r).
∀P,Q. relation_pair_setoid P Q → relation_pair P Q ≝ λP,Q,x.x.
coercion relation_pair_of_relation_pair_setoid.
+alias symbol "compose" (instance 1) = "category1 composition".
lemma eq_to_eq':
- ∀o1,o2.∀r,r':relation_pair_setoid o1 o2. r =_1 r' → r \sub\f ∘ ⊩ = r'\sub\f ∘ ⊩.
+ ∀o1,o2.∀r,r':relation_pair_setoid o1 o2. r =_1 r' → r \sub\f ∘ ⊩ =_1 r'\sub\f ∘ ⊩.
intros 5 (o1 o2 r r' H);
apply (.= (commute ?? r)^-1);
change in H with (⊩ ∘ r \sub\c = ⊩ ∘ r' \sub\c);
| lapply (id_neutral_right1 ? (concr o) ? (⊩)) as H;
lapply (id_neutral_left1 ?? (form o) (⊩)) as H1;
apply (.= H);
- apply (H1 \sup -1);]
+ apply (H1^-1);]
qed.
lemma relation_pair_composition:
apply (.= ASSOC ^ -1);
apply (.= e‡#);
apply (.= ASSOC);
- apply (.= #‡(commute ?? b')\sup -1);
+ apply (.= #‡(commute ?? b')^-1);
apply (ASSOC ^ -1);
qed.