From: Claudio Sacerdoti Coen Date: Sat, 23 Aug 2008 19:14:54 +0000 (+0000) Subject: Definition of categories. X-Git-Tag: make_still_working~4850 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=be9826d87207e8dcf6eb152bd54417b5a9e80ab9;p=helm.git Definition of categories. Proof that basic pairs form a category. --- diff --git a/helm/software/matita/library/formal_topology/basic_pairs.ma b/helm/software/matita/library/formal_topology/basic_pairs.ma new file mode 100644 index 000000000..5cc67a250 --- /dev/null +++ b/helm/software/matita/library/formal_topology/basic_pairs.ma @@ -0,0 +1,183 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "datatypes/subsets.ma". +include "logic/cprop_connectives.ma". +include "formal_topology/categories.ma". + +record basic_pair: Type ≝ + { carr1: Type; + carr2: Type; + concr: Ω \sup carr1; + form: Ω \sup carr2; + rel: binary_relation ?? concr form + }. + +notation "x ⊩ y" with precedence 45 for @{'Vdash2 $x $y}. +notation "⊩" with precedence 60 for @{'Vdash}. + +interpretation "basic pair relation" 'Vdash2 x y = (rel _ x y). +interpretation "basic pair relation (non applied)" 'Vdash = (rel _). + +alias symbol "eq" = "equal relation". +alias symbol "compose" = "binary relation composition". +record relation_pair (BP1,BP2: basic_pair): Type ≝ + { concr_rel: binary_relation ?? (concr BP1) (concr BP2); + form_rel: binary_relation ?? (form BP1) (form BP2); + commute: concr_rel ∘ ⊩ = ⊩ ∘ form_rel + }. + +notation "hvbox (r \sub \c)" with precedence 90 for @{'concr_rel $r}. +notation "hvbox (r \sub \f)" with precedence 90 for @{'form_rel $r}. + +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_relation (relation_pair o1 o2). + intros; + constructor 1; + [ apply (λr,r'. r \sub\c ∘ ⊩ = r' \sub\c ∘ ⊩); + | simplify; + intros; + apply refl_equal_relations; + | simplify; + intros; + apply sym_equal_relations; + assumption + | simplify; + intros; + apply (trans_equal_relations ??????? H); + assumption + ] +qed. + +definition relation_pair_setoid: basic_pair → basic_pair → setoid. + intros; + constructor 1; + [ apply (relation_pair b b1) + | apply relation_pair_equality + ] +qed. + +definition eq' ≝ + λo1,o2.λr,r':relation_pair o1 o2.⊩ ∘ r \sub\f = ⊩ ∘ r' \sub\f. + +alias symbol "eq" = "setoid eq". +lemma eq_to_eq': ∀o1,o2.∀r,r': relation_pair_setoid o1 o2. r=r' → eq' ?? r r'. + intros 7 (o1 o2 r r' H c1 f2); + split; intro; + [ lapply (fi ?? (commute ?? r c1 f2) H1) as H2; + lapply (if ?? (H c1 f2) H2) as H3; + apply (if ?? (commute ?? r' c1 f2) H3); + | lapply (fi ?? (commute ?? r' c1 f2) H1) as H2; + lapply (fi ?? (H c1 f2) H2) as H3; + apply (if ?? (commute ?? r c1 f2) H3); + ] +qed. + + +definition id: ∀o:basic_pair. relation_pair o o. + intro; + constructor 1; + [1,2: constructor 1; + intros; + apply (s=s1) + | simplify; intros; + split; + intro; + cases H; + cases H1; clear H H1; + [ exists [ apply y ] + split + [ rewrite > H2; assumption + | reflexivity ] + | exists [ apply x ] + split + [2: rewrite < H3; assumption + | reflexivity ]]] +qed. + +definition relation_pair_composition: + ∀o1,o2,o3. binary_morphism (relation_pair_setoid o1 o2) (relation_pair_setoid o2 o3) (relation_pair_setoid o1 o3). + intros; + constructor 1; + [ intros (r r1); + constructor 1; + [ apply (r \sub\c ∘ r1 \sub\c) + | apply (r \sub\f ∘ r1 \sub\f) + | lapply (commute ?? r) as H; + lapply (commute ?? r1) as H1; + 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]] +qed. + +definition BP: category. + constructor 1; + [ apply basic_pair + | apply relation_pair_setoid + | apply id + | apply relation_pair_composition + | intros; + change with (a12\sub\c ∘ a23\sub\c ∘ a34\sub\c ∘ ⊩ = + (a12\sub\c ∘ (a23\sub\c ∘ a34\sub\c) ∘ ⊩)); + apply composition_morphism; + [2: apply refl_equal_relations] + apply associative_composition + | intros; + change with ((id o1)\sub\c ∘ a\sub\c ∘ ⊩ = a\sub\c ∘ ⊩); + apply composition_morphism; + [2: apply refl_equal_relations] + intros 2; unfold id; simplify; + split; intro; + [ cases H; cases H1; rewrite > H2; assumption + | exists; [assumption] split; [reflexivity| assumption]] + | intros; + change with (a\sub\c ∘ (id o2)\sub\c ∘ ⊩ = a\sub\c ∘ ⊩); + apply composition_morphism; + [2: apply refl_equal_relations] + intros 2; unfold id; simplify; + split; intro; + [ cases H; cases H1; rewrite < H3; assumption + | exists; [assumption] split; [assumption|reflexivity]] + ] +qed. diff --git a/helm/software/matita/library/formal_topology/categories.ma b/helm/software/matita/library/formal_topology/categories.ma new file mode 100644 index 000000000..7adcb279f --- /dev/null +++ b/helm/software/matita/library/formal_topology/categories.ma @@ -0,0 +1,47 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "logic/cprop_connectives.ma". + +record equivalence_relation (A:Type) : Type ≝ + { eq_rel:2> A → A → CProp; + refl: reflexive ? eq_rel; + sym: symmetric ? eq_rel; + trans: transitive ? eq_rel + }. + +record setoid : Type ≝ + { carr:> Type; + eq: equivalence_relation carr + }. + +interpretation "setoid eq" 'eq x y = (eq_rel _ (eq _) x y). + +record binary_morphism (A,B,C: setoid) : Type ≝ + { fun:2> A → B → C; + prop: ∀a,a',b,b'. eq ? a a' → eq ? b b' → eq ? (fun a b) (fun a' b') + }. + +record category : Type ≝ + { objs: Type; + arrows: objs → objs → setoid; + id: ∀o:objs. arrows o o; + comp: ∀o1,o2,o3. binary_morphism (arrows o1 o2) (arrows o2 o3) (arrows o1 o3); + comp_assoc: ∀o1,o2,o3,o4. ∀a12,a23,a34. + comp o1 o3 o4 (comp o1 o2 o3 a12 a23) a34 = comp o1 o2 o4 a12 (comp o2 o3 o4 a23 a34); + id_neutral_left: ∀o1,o2. ∀a: arrows o1 o2. comp ??? (id o1) a = a; + id_neutral_right: ∀o1,o2. ∀a: arrows o1 o2. comp ??? a (id o2) = a + }. + +interpretation "category composition" 'compose x y = (comp ____ x y). \ No newline at end of file