helm/software/matita/library/formal_topology/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
  31 record binary_morphism (A,B,C: setoid) : Type ≝
  32  { fun:2> A → B → C;
  33    prop: ∀a,a',b,b'. eq ? a a' → eq ? b b' → eq ? (fun a b) (fun a' b')
  34  }.
  35
  36 record category : Type ≝
  37  { objs: Type;
  38    arrows: objs → objs → setoid;
  39    id: ∀o:objs. arrows o o;
  40    comp: ∀o1,o2,o3. binary_morphism (arrows o1 o2) (arrows o2 o3) (arrows o1 o3);
  41    comp_assoc: ∀o1,o2,o3,o4. ∀a12,a23,a34.
  42     comp o1 o3 o4 (comp o1 o2 o3 a12 a23) a34 = comp o1 o2 o4 a12 (comp o2 o3 o4 a23 a34);
  43    id_neutral_left: ∀o1,o2. ∀a: arrows o1 o2. comp ??? (id o1) a = a;
  44    id_neutral_right: ∀o1,o2. ∀a: arrows o1 o2. comp ??? a (id o2) = a
  45  }.
  46
  47 interpretation "category composition" 'compose x y = (comp ____ x y).