remove reliance on General.v

[coq-categories.git] / src / Coherence_ch7_8.v

diff --git a/src/Coherence_ch7_8.v b/src/Coherence_ch7_8.v
index 2665255..2d5f689 100644 (file)
--- 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 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