X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=src%2FPreMonoidalCategories.v;h=e56c72750ef96123175d40ce6fdfe84fe5f81965;hb=45449bae8b3348278301e268aabb2a1c3dd8d0cb;hp=4ab56d2dde51792e57c1453886d7a7c2d911efa7;hpb=e928451c4c45cdbdd975bbfb229e8cc2616b8194;p=coq-categories.git

diff --git a/src/PreMonoidalCategories.v b/src/PreMonoidalCategories.v
index 4ab56d2..e56c727 100644
--- a/src/PreMonoidalCategories.v
+++ b/src/PreMonoidalCategories.v
@@ -3,6 +3,7 @@ Require Import Preamble.
 Require Import Categories_ch1_3.
 Require Import Functors_ch1_4.
 Require Import Isomorphisms_ch1_5.
+Require Import EpicMonic_ch2_1.
 Require Import InitialTerminal_ch2_2.
 Require Import Subcategories_ch7_1.
 Require Import NaturalTransformations_ch7_4.
@@ -53,16 +54,95 @@ Implicit Arguments pmon_assoc   [ Ob Hom C bin_obj' bc I PreMonoidalCat ].
 Coercion pmon_bin : PreMonoidalCat >-> BinoidalCat.
 
 (* this turns out to be Exercise VII.1.1 from Mac Lane's CWM *)
-Lemma MacLane_ex_VII_1_1 `{mn:PreMonoidalCat(I:=EI)} a b
-  : #(pmon_cancelr (a ⊗ b)) ~~ #((pmon_assoc a EI) b) >>> (a ⋊-) \ #(pmon_cancelr b).
-  set (pmon_pentagon EI EI a b) as penta. unfold pmon_pentagon in penta.
-  set (pmon_triangle a b) as tria. unfold pmon_triangle in tria.
-  apply (fmor_respects(bin_second EI)) in tria.
-  set (@fmor_preserves_comp) as fpc.
-  setoid_rewrite <- fpc in tria.
-  set (ni_commutes (pmon_assoc a b)) as xx.
-  (* FIXME *)
-  Admitted.
+Lemma MacLane_ex_VII_1_1 `{mn:PreMonoidalCat(I:=EI)} b a
+  : 
+  let    α := fun a b c => #((pmon_assoc a c) b)
+  in     α a b EI >>> _ ⋊ #(pmon_cancelr _) ~~ #(pmon_cancelr _).
+
+  intros.  simpl in α.
+
+  (* following Mac Lane's hint, we aim for (λ >>> α >>> λ×1)~~(λ >>> λ) *)
+  set (epic _ (iso_epic (pmon_cancelr ((a⊗b)⊗EI)))) as q.
+    apply q.
+    clear q.
+
+  (* next, we show that the hint goal above is implied by the bottom-left 1/5th of the big whiteboard diagram *)
+  set (ni_commutes pmon_cancelr (α a b EI)) as q.
+    setoid_rewrite <- associativity.
+    setoid_rewrite q.
+    clear q.
+    setoid_rewrite associativity.
+
+    set (ni_commutes pmon_cancelr (a ⋊ #(pmon_cancelr b))) as q.
+    simpl in q.
+    setoid_rewrite q.
+    clear q.
+
+    set (ni_commutes pmon_cancelr (#(pmon_cancelr (a⊗b)))) as q.
+    simpl in q.
+    setoid_rewrite q.
+    clear q.
+
+    setoid_rewrite <- associativity.
+    apply comp_respects; try reflexivity.
+
+  (* now we carry out the proof in the whiteboard diagram, starting from the pentagon diagram *)
+
+  (* top 2/5ths *)
+  assert (α (a⊗b) EI EI >>> α _ _ _ >>> (_ ⋊ (_ ⋊ #(pmon_cancell _))) ~~ #(pmon_cancelr _) ⋉ _ >>> α _ _ _).
+    set (pmon_triangle (a⊗b) EI) as tria.
+    simpl in tria.
+    unfold α; simpl.
+    setoid_rewrite tria.
+    clear tria.
+    setoid_rewrite associativity.
+    apply comp_respects; try reflexivity.
+    set (ni_commutes (pmon_assoc_ll a b) #(pmon_cancell EI)) as x.
+    simpl in x.
+    setoid_rewrite pmon_coherent_l in x.
+    apply x.
+
+  (* bottom 3/5ths *)
+  assert (((#((pmon_assoc a EI) b) ⋉ EI >>> #((pmon_assoc a EI) (b ⊗ EI))) >>>
+    a ⋊ #((pmon_assoc b EI) EI)) >>> a ⋊ (b ⋊ #(pmon_cancell EI))
+    ~~ α _ _ _ ⋉ _ >>> (_ ⋊ #(pmon_cancelr _)) ⋉ _ >>> α _ _ _).
+
+    unfold α; simpl.
+    repeat setoid_rewrite associativity.
+    apply comp_respects; try reflexivity.
+
+    set (ni_commutes (pmon_assoc a EI) (#(pmon_cancelr b) )) as x.
+    simpl in x.
+    setoid_rewrite <- associativity.
+    simpl in x.
+    setoid_rewrite <- x.
+    clear x.
+
+    setoid_rewrite associativity.
+    apply comp_respects; try reflexivity.
+    setoid_rewrite (fmor_preserves_comp (a⋊-)).
+    apply (fmor_respects (a⋊-)).
+
+    set (pmon_triangle b EI) as tria.
+    simpl in tria.
+    symmetry.
+    apply tria.
+
+  set (pmon_pentagon a b EI EI) as penta. unfold pmon_pentagon in penta. simpl in penta.
+
+  set (@comp_respects _ _ _ _ _ _ _ _ penta (a ⋊ (b ⋊ #(pmon_cancell EI))) (a ⋊ (b ⋊ #(pmon_cancell EI)))) as qq.
+    unfold α in H.
+    setoid_rewrite H in qq.
+    unfold α in H0.
+    setoid_rewrite H0 in qq.
+    clear H0 H.
+
+  unfold α.
+    apply (monic _ (iso_monic ((pmon_assoc a EI) b))).
+    apply qq.
+    clear qq penta.
+    reflexivity.
+    Qed.
 
 Class PreMonoidalFunctor
 `(PM1:PreMonoidalCat(C:=C1)(I:=I1))