1 Generalizable All Variables.
2 Require Import Preamble.
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.
9 (* these are the coherence diagrams found in Definition 7.23 of Awodey's book *)
11 (* DO NOT try to inline this into [Pre]MonoidalCat; it triggers a Coq resource consumption bug *)
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))).
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   }.
28   Context {I:C}
29           (cancell : forall a    :C,              (bobj I a) ~~{C}~~> a)
30           (cancelr : forall a    :C,              (bobj a I) ~~{C}~~> a).
32   Record Triangle :=
33   { triangle :  forall a b, (first _ _ b (cancelr a)) ~~ (assoc a I b) >>> (second _ _ a (cancell b))
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   }.
47 End Coherence.
49 Coercion pentagon : Pentagon >-> Funclass.
50 Coercion triangle : Triangle >-> Funclass.
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 ].