helm/software/matita/library/datatypes/categories.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "logic/cprop_connectives.ma".
  16
  17 record equivalence_relation (A:Type) : Type ≝
  18  { eq_rel:2> A → A → CProp;
  19    refl: reflexive ? eq_rel;
  20    sym: symmetric ? eq_rel;
  21    trans: transitive ? eq_rel
  22  }.
  23
  24 record setoid : Type ≝
  25  { carr:> Type;
  26    eq: equivalence_relation carr
  27  }.
  28
  29 interpretation "setoid eq" 'eq x y = (eq_rel _ (eq _) x y).
  30 notation ".= r" with precedence 50 for @{trans ????? $r}.
  31 interpretation "setoid symmetry" 'invert r = (sym ____ r).
  32
  33 record binary_morphism (A,B,C: setoid) : Type ≝
  34  { fun:2> A → B → C;
  35    prop: ∀a,a',b,b'. eq ? a a' → eq ? b b' → eq ? (fun a b) (fun a' b')
  36  }.
  37
  38 notation "# r" with precedence 60 for @{prop ???????? (refl ???) $r}.
  39 notation "r #" with precedence 60 for @{prop ???????? $r (refl ???)}.
  40
  41 definition CPROP: setoid.
  42  constructor 1;
  43   [ apply CProp
  44   | constructor 1;
  45      [ apply Iff
  46      | intros 1; split; intro; assumption
  47      | intros 3; cases H; split; assumption
  48      | intros 5; cases H; cases H1; split; intro;
  49         [ apply (H4 (H2 H6)) | apply (H3 (H5 H6))]]]
  50 qed.
  51
  52 definition eq_morphism: ∀S:setoid. binary_morphism S S CPROP.
  53  intro;
  54  constructor 1;
  55   [ apply (eq_rel ? (eq S))
  56   | intros; split; intro;
  57      [ apply (.= H \sup -1);
  58        apply (.= H2);
  59        assumption
  60      | apply (.= H);
  61        apply (.= H2);
  62        apply (H1 \sup -1)]]
  63 qed.
  64
  65 record category : Type ≝
  66  { objs:> Type;
  67    arrows: objs → objs → setoid;
  68    id: ∀o:objs. arrows o o;
  69    comp: ∀o1,o2,o3. binary_morphism (arrows o1 o2) (arrows o2 o3) (arrows o1 o3);
  70    comp_assoc: ∀o1,o2,o3,o4. ∀a12,a23,a34.
  71     comp o1 o3 o4 (comp o1 o2 o3 a12 a23) a34 = comp o1 o2 o4 a12 (comp o2 o3 o4 a23 a34);
  72    id_neutral_left: ∀o1,o2. ∀a: arrows o1 o2. comp ??? (id o1) a = a;
  73    id_neutral_right: ∀o1,o2. ∀a: arrows o1 o2. comp ??? a (id o2) = a
  74  }.
  75
  76 interpretation "category composition" 'compose x y = (fun ___ (comp ____) x y).
  77 notation "'ASSOC'" with precedence 90 for @{comp_assoc ????????}.