src/Coherence_ch7_8.v

   1 Generalizable All Variables.
   2 Require Import Notations.
   3 Require Import Categories_ch1_3.
   4 Require Import Functors_ch1_4.
   5 Require Import Isomorphisms_ch1_5.
   6 Require Import ProductCategories_ch1_6_1.
   7 Require Import NaturalTransformations_ch7_4.
   8
   9 (* these are the coherence diagrams found in Definition 7.23 of Awodey's book *)
  10
  11 (* DO NOT try to inline this into [Pre]MonoidalCat; it triggers a Coq resource consumption bug *)
  12
  13 Section Coherence.
  14   Context `{C:Category}
  15            {bobj:C->C->C}
  16            (first  : forall a b c:C, (a~~{C}~~>b) -> ((bobj a c)~~{C}~~>(bobj b c)))
  17            (second : forall a b c:C, (a~~{C}~~>b) -> ((bobj c a)~~{C}~~>(bobj c b)))
  18            (assoc  : forall a b c:C, (bobj (bobj a b) c) ~~{C}~~> (bobj a (bobj b c))).
  19
  20   Record Pentagon :=
  21   { pentagon :   forall a b c d,    (first _ _ d (assoc a b c ))  >>>
  22                                                  (assoc a _ d )   >>>
  23                                    (second _ _ a (assoc b c d ))
  24                                               ~~ (assoc _ c d )   >>>
  25                                                  (assoc a b _ )
  26   }.
  27
  28   Context {I:C}
  29           (cancell : forall a    :C,              (bobj I a) ~~{C}~~> a)
  30           (cancelr : forall a    :C,              (bobj a I) ~~{C}~~> a).
  31
  32   Record Triangle :=
  33   { triangle :  forall a b, (first _ _ b (cancelr a)) ~~ (assoc a I b) >>> (second _ _ a (cancell b))
  34
  35   (*
  36    * This is taken as an axiom in Mac Lane, Categories for the Working
  37    * Mathematician, p163, display (8), as well as in Awodey (second
  38    * triangle diagram).  However, it was shown to be eliminable by
  39    * Kelly in Theorem 6 of
  40    * http://dx.doi.org/10.1016/0021-8693(64)90018-3 but that was under
  41    * different assumptions.  To be safe we include it here as an
  42    * axiom.
  43    *)
  44   ; coincide :  (cancell I) ~~ (cancelr I)
  45   }.
  46
  47 End Coherence.
  48
  49 Coercion pentagon : Pentagon >-> Funclass.
  50 Coercion triangle : Triangle >-> Funclass.
  51
  52 Implicit Arguments pentagon [ Ob Hom C bobj first second assoc ].
  53 Implicit Arguments triangle [ Ob Hom C bobj first second assoc I cancell cancelr ].
  54 Implicit Arguments coincide [ Ob Hom C bobj first second assoc I cancell cancelr ].