src/PreCategory.v

   1 (*********************************************************************************************************************************)
   2 (* SemiCategory:                                                                                                                 *)
   3 (*                                                                                                                               *)
   4 (*   Same as a category, but without identity maps.   See                                                                        *)
   5 (*                                                                                                                               *)
   6 (*       http://ncatlab.org/nlab/show/semicategory                                                                               *)
   7 (*                                                                                                                               *)
   8 (*********************************************************************************************************************************)
   9
  10 Generalizable All Variables.
  11 Require Import Preamble.
  12 Require Import General.
  13
  14 Class SemiCategory (Ob:Type)(Hom:Ob->Ob->Type) :=
  15 { semi_hom              := Hom
  16 ; semi_ob               := Ob
  17 ; semi_comp             :  forall  {a}{b}{c}, Hom a b -> Hom b c -> Hom a c
  18 ; semi_eqv              :  forall  a b,   (Hom a b) -> (Hom a b) -> Prop
  19 ; semi_eqv_equivalence  :  forall  a b,   Equivalence (semi_eqv a b)
  20 ; semi_comp_respects    :  forall  a b c, Proper (semi_eqv a b ==> semi_eqv b c ==> semi_eqv a c) (@semi_comp _ _ _)
  21 ; semi_associativity    :
  22        forall `(f:Hom a b)`(g:Hom b c)`(h:Hom c d), semi_eqv _ _ (semi_comp (semi_comp f g) h) (semi_comp f (semi_comp g h))
  23 }.
  24 Coercion semi_ob : SemiCategory >-> Sortclass.
  25
  26 Notation "a ~->   b" := (@semi_hom  _ _ _       a b) (at level 70).
  27 Notation "f ~-~   g" := (@semi_eqv  _ _ _ _ _   f g) (at level 54).
  28 Notation "f >>->> g" := (@semi_comp _ _ _ _ _ _ f g) (at level 45).
  29
  30 Add Parametric Relation (Ob:Type)(Hom:Ob->Ob->Type)(C:SemiCategory Ob Hom)(a b:Ob) : (semi_hom a b) (semi_eqv a b)
  31   reflexivity proved by  (@Equivalence_Reflexive  _ _ (semi_eqv_equivalence a b))
  32   symmetry proved by     (@Equivalence_Symmetric  _ _ (semi_eqv_equivalence a b))
  33   transitivity proved by (@Equivalence_Transitive _ _ (semi_eqv_equivalence a b))
  34   as parametric_relation_semi_eqv.
  35   Add Parametric Morphism `(c:SemiCategory Ob Hom)(a b c:Ob) : (@semi_comp _ _ _ a b c)
  36   with signature (semi_eqv _ _ ==> semi_eqv _ _ ==> semi_eqv _ _) as parametric_morphism_semi_comp.
  37     intros.
  38     apply semi_comp_respects; auto.
  39   Defined.
  40
  41 Class SemiFunctor
  42 `( c1                 : SemiCategory                           )
  43 `( c2                 : SemiCategory                           )
  44 ( fobj                : c1 -> c2                               ) :=
  45 { semifunctor_fobj         := fobj
  46 ; semi_fmor                : forall {a b}, (a~->b) -> (fobj a)~->(fobj b)
  47 ; semi_fmor_respects       : forall a b (f f':a~->b),   (f ~-~ f') ->        (semi_fmor f ~-~ semi_fmor f')
  48 ; semi_fmor_preserves_comp : forall `(f:a~->b)`(g:b~->c), (semi_fmor f) >>->> (semi_fmor g) ~-~ semi_fmor (f >>->> g)
  49 }.
  50 Implicit Arguments semi_fmor [[Ob][Hom][c1][Ob0][Hom0][c2][fobj][a][b]].
  51
  52   (* register "fmor" so we can rewrite through it *)
  53   Implicit Arguments semi_fmor                [ Ob Hom Ob0 Hom0 c1 c2 fobj a b ].
  54   Implicit Arguments semi_fmor_respects       [ Ob Hom Ob0 Hom0 c1 c2 fobj a b ].
  55   Implicit Arguments semi_fmor_preserves_comp [ Ob Hom Ob0 Hom0 c1 c2 fobj a b c ].
  56   Notation "F \- f" := (semi_fmor F f) (at level 20)  : category_scope.
  57   Add Parametric Morphism `(C1:SemiCategory)`(C2:SemiCategory)
  58     (Fobj:C1->C2)
  59     (F:SemiFunctor C1 C2 Fobj)
  60     (a b:C1)
  61   : (@semi_fmor _ _ C1 _ _ C2 Fobj F a b)
  62   with signature ((@semi_eqv C1 _ C1 a b) ==> (@semi_eqv C2 _ C2 (Fobj a) (Fobj b))) as parametric_morphism_semi_fmor'.
  63   intros; apply (@semi_fmor_respects _ _ C1 _ _ C2 Fobj F a b x y); auto.
  64   Defined.
  65   Coercion semifunctor_fobj : SemiFunctor >-> Funclass.
  66
  67 Definition semifunctor_comp
  68   `(C1:SemiCategory)
  69   `(C2:SemiCategory)
  70   `(C3:SemiCategory)
  71   `(F:@SemiFunctor _ _ C1 _ _ C2 Fobj)`(G:@SemiFunctor _ _ C2 _ _ C3 Gobj) : SemiFunctor C1 C3 (Gobj ○ Fobj).
  72   intros. apply (Build_SemiFunctor _ _ _ _ _ _ _ (fun a b m => semi_fmor G (semi_fmor F m))).
  73   intros.
  74   setoid_rewrite H.
  75   reflexivity.
  76   intros.
  77   setoid_rewrite semi_fmor_preserves_comp; auto.
  78   setoid_rewrite semi_fmor_preserves_comp; auto.
  79   reflexivity.
  80   Defined.
  81 Notation "f >>>–>>> g" := (@semifunctor_comp _ _ _ _ _ _ _ _ _ _ f _ g) (at level 20)  : category_scope.
  82
  83 Class IsomorphicSemiCategories `(C:SemiCategory)`(D:SemiCategory) :=
  84 { isc_f_obj    : C -> D
  85 ; isc_g_obj    : D -> C
  86 ; isc_f        : SemiFunctor C D isc_f_obj
  87 ; isc_g        : SemiFunctor D C isc_g_obj
  88 ; isc_forward  : forall a b (f:a~->b), semi_fmor isc_f  (semi_fmor isc_g  f) ~-~ f
  89 }.
  90 ; isc_backward : isc_g >>>> isc_f ~~~~ functor_id D
  91 }.
  92
  93