include "relations.ma".
include "notation.ma".
-record basic_pair: Type1 ≝
- { concr: REL;
- form: REL;
- rel: arrows1 ? concr form
- }.
+record basic_pair: Type1 ≝ {
+ concr: REL; form: REL; rel: concr ⇒_\r1 form
+}.
interpretation "basic pair relation" 'Vdash2 x y c = (fun21 ??? (rel c) x y).
interpretation "basic pair relation (non applied)" 'Vdash c = (rel c).
-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 ∘ ⊩
}.
-
interpretation "concrete relation" 'concr_rel r = (concr_rel ?? r).
interpretation "formal relation" 'form_rel r = (form_rel ?? r).
-definition relation_pair_equality:
- ∀o1,o2. equivalence_relation1 (relation_pair o1 o2).
- intros;
- constructor 1;
- [ apply (λr,r'. ⊩ ∘ r \sub\c = ⊩ ∘ r' \sub\c);
- | simplify;
- intros;
- apply refl1;
- | simplify;
- intros 2;
- apply sym1;
- | simplify;
- intros 3;
- apply trans1;
- ]
+definition relation_pair_equality: ∀o1,o2. equivalence_relation1 (relation_pair o1 o2).
+ intros; constructor 1; [ apply (λr,r'. ⊩ ∘ r \sub\c = ⊩ ∘ r' \sub\c);
+ | simplify; intros; apply refl1;
+ | simplify; intros 2; apply sym1;
+ | simplify; intros 3; apply trans1; ]
qed.
definition relation_pair_setoid: basic_pair → basic_pair → setoid1.
coercion relation_pair_of_relation_pair_setoid.
lemma eq_to_eq':
- ∀o1,o2.∀r,r':relation_pair_setoid o1 o2. r=r' → r \sub\f ∘ ⊩ = r'\sub\f ∘ ⊩.
+ ∀o1,o2.∀r,r':relation_pair_setoid o1 o2. r =_1 r' → r \sub\f ∘ ⊩ = r'\sub\f ∘ ⊩.
intros 7 (o1 o2 r r' H c1 f2);
split; intro H1;
[ lapply (fi ?? (commute ?? r c1 f2) H1) as H2;