src/Coherence_ch7_8.v

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