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.
10 (* these are the coherence diagrams found in Definition 7.23 of Awodey's book *)
12 (* DO NOT try to inline this into [Pre]MonoidalCat; it triggers a Coq resource consumption bug *)
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))).
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   }.
29   Context {I:C}
30           (cancell : forall a    :C,              (bobj I a) ~~{C}~~> a)
31           (cancelr : forall a    :C,              (bobj a I) ~~{C}~~> a).
33   Record Triangle :=
34   { triangle :  forall a b, (first _ _ b (cancelr a)) ~~ (assoc a I b) >>> (second _ _ a (cancell b))
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   }.
48 End Coherence.
50 Coercion pentagon : Pentagon >-> Funclass.
51 Coercion triangle : Triangle >-> Funclass.
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 ].