From 11a22c74b3b2307eedf89c0439ba02d199dcdc9e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 30 Jun 2010 14:10:39 +0000 Subject: [PATCH] ... --- .../formal_topology/overlap/o-basic_pairs.ma | 29 ++++++++----------- 1 file changed, 12 insertions(+), 17 deletions(-) diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma index 3cbb70058..6f16b0d3f 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma @@ -15,27 +15,22 @@ include "o-algebra.ma". include "notation.ma". -record Obasic_pair: Type2 ≝ - { Oconcr: OA; - Oform: OA; - Orel: arrows2 ? Oconcr Oform - }. +record Obasic_pair: Type2 ≝ { + Oconcr: OA; Oform: OA; Orel: arrows2 ? Oconcr Oform +}. (* FIX *) interpretation "o-basic pair relation indexed" 'Vdash2 x y c = (Orel c x y). interpretation "o-basic pair relation (non applied)" 'Vdash c = (Orel c). -alias symbol "eq" = "setoid1 eq". -alias symbol "compose" = "category1 composition". -(*DIFFER*) - -alias symbol "eq" = "setoid2 eq". -alias symbol "compose" = "category2 composition". -record Orelation_pair (BP1,BP2: Obasic_pair): Type2 ≝ - { Oconcr_rel: arrows2 ? (Oconcr BP1) (Oconcr BP2); - Oform_rel: arrows2 ? (Oform BP1) (Oform BP2); - Ocommute: ⊩ ∘ Oconcr_rel = Oform_rel ∘ ⊩ - }. +notation > "B ⇒_\o2 C" right associative with precedence 72 for @{'arrows2_OA $B $C}. +notation "B ⇒\sub (\o 2) C" right associative with precedence 72 for @{'arrows2_OA $B $C}. +interpretation "'arrows2_OA" 'arrows2_OA A B = (arrows2 OA A B). + +record Orelation_pair (BP1,BP2: Obasic_pair): Type2 ≝ { + Oconcr_rel: (Oconcr BP1) ⇒_\o2 (Oconcr BP2); Oform_rel: (Oform BP1) ⇒_\o2 (Oform BP2); + Ocommute: ⊩ ∘ Oconcr_rel =_2 Oform_rel ∘ ⊩ +}. (* FIX *) interpretation "o-concrete relation" 'concr_rel r = (Oconcr_rel ?? r). @@ -71,7 +66,7 @@ definition Orelation_pair_of_Orelation_pair_setoid: ∀P,Q. Orelation_pair_setoid P Q → Orelation_pair P Q ≝ λP,Q,x.x. coercion Orelation_pair_of_Orelation_pair_setoid. -lemma eq_to_eq': ∀o1,o2.∀r,r': Orelation_pair_setoid o1 o2. r=r' → r \sub\f ∘ ⊩ = r'\sub\f ∘ ⊩. +lemma eq_to_eq': ∀o1,o2.∀r,r': Orelation_pair_setoid o1 o2. r =_2 r' → r \sub\f ∘ ⊩ =_2 r'\sub\f ∘ ⊩. intros 5 (o1 o2 r r' H); change in H with (⊩ ∘ r\sub\c = ⊩ ∘ r'\sub\c); apply (.= ((Ocommute ?? r) ^ -1)); apply (.= H); -- 2.39.2