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.
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 *)
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))).
21 { pentagon : forall a b c d, (first _ _ d (assoc a b c )) >>>
23 (second _ _ a (assoc b c d ))
29 (cancell : forall a :C, (bobj I a) ~~{C}~~> a)
30 (cancelr : forall a :C, (bobj a I) ~~{C}~~> a).
33 { triangle : forall a b, (first _ _ b (cancelr a)) ~~ (assoc a I b) >>> (second _ _ a (cancell b))
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
44 ; coincide : (cancell I) ~~ (cancelr I)
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 ].