X-Git-Url: http://git.megacz.com/?p=coq-categories.git;a=blobdiff_plain;f=src%2FCoherence_ch7_8.v;h=20d5920387e0f17a6f855dd4c4cdb4015ad34197;hp=26652552b3c114ec7cef69f666e8a2a843bf7ffb;hb=90844bf411c7cddcd92d48c0b020e5775ace0849;hpb=1dd1bee2b13b43812ebbc078bdbf774886392886

diff --git a/src/Coherence_ch7_8.v b/src/Coherence_ch7_8.v
index 2665255..20d5920 100644
--- a/src/Coherence_ch7_8.v
+++ b/src/Coherence_ch7_8.v
@@ -1,6 +1,5 @@
 Generalizable All Variables.
-Require Import Preamble.
-Require Import General.
+Require Import Notations.
 Require Import Categories_ch1_3.
 Require Import Functors_ch1_4.
 Require Import Isomorphisms_ch1_5.
@@ -16,14 +15,14 @@ Section Coherence.
            {bobj:C->C->C}
            (first  : forall a b c:C, (a~~{C}~~>b) -> ((bobj a c)~~{C}~~>(bobj b c)))
            (second : forall a b c:C, (a~~{C}~~>b) -> ((bobj c a)~~{C}~~>(bobj c b)))
-           (assoc  : forall a b c:C, (bobj a (bobj b c)) ~~{C}~~> (bobj (bobj a b) c)).
+           (assoc  : forall a b c:C, (bobj (bobj a b) c) ~~{C}~~> (bobj a (bobj b c))).
 
   Record Pentagon :=
-  { pentagon :   forall a b c d,                 (assoc a _ _ )  >>>
-                                                 (assoc _ _ _ )  ~~
-                                   (second _ _ a (assoc b c d )) >>>
-                                                 (assoc _ _ _ )  >>>
-                                   (first  _ _ _ (assoc a b _ ))
+  { pentagon :   forall a b c d,    (first _ _ d (assoc a b c ))  >>>
+                                                 (assoc a _ d )   >>>
+                                   (second _ _ a (assoc b c d )) 
+                                              ~~ (assoc _ c d )   >>>
+                                                 (assoc a b _ )
   }.
 
   Context {I:C}
@@ -31,7 +30,7 @@ Section Coherence.
           (cancelr : forall a    :C,              (bobj a I) ~~{C}~~> a).
 
   Record Triangle :=
-  { triangle :  forall a b, (assoc a I b) >>> (first _ _ b (cancelr a)) ~~ (second _ _ a (cancell b))
+  { triangle :  forall a b, (first _ _ b (cancelr a)) ~~ (assoc a I b) >>> (second _ _ a (cancell b))
 
   (* 
    * This is taken as an axiom in Mac Lane, Categories for the Working