X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FGeneralizedArrowFromReification.v;h=9ff0d4df8bd35789d076ed1ba5d5282109dbe1a7;hp=810e8628b7158f8227c1a216b01139bcfdd5d483;hb=a5617bbb88197a50083a64c9970511a15f7ed98a;hpb=64d416692bda1d36c33b5efa245d46dcf546ad4a

diff --git a/src/GeneralizedArrowFromReification.v b/src/GeneralizedArrowFromReification.v
index 810e862..9ff0d4d 100644
--- a/src/GeneralizedArrowFromReification.v
+++ b/src/GeneralizedArrowFromReification.v
@@ -265,13 +265,633 @@ Section GArrowFromReification.
        (garrow_functor >>>> bin_second(BinoidalCat:=enr_c_bin C) (R' a))
     <~~~>  (bin_second(BinoidalCat:=enr_v_pmon K) a >>>> garrow_functor) :=
     { ni_iso := fun a => iso_id _ }.
-    admit.
+
+    intros.
+      etransitivity.  apply iso_id_lemma1.  symmetry.
+      etransitivity.  apply iso_id_lemma2.  symmetry.
+
+    Opaque Underlying.
+    unfold garrow_functor.
+      unfold functor_comp at 1.
+      unfold functor_comp at 1.
+      Opaque functor_comp. simpl. Transparent functor_comp.
+
+    symmetry.
+      eapply transitivity.
+      apply (functor_comp_assoc (RestrictToImage reification) (R' >>>> step2_functor) (ebc_second (R' a)) f).
+      unfold functor_comp at 1.
+      unfold functor_comp at 1.
+      Opaque functor_comp. simpl. Transparent functor_comp.
+
+    symmetry.
+      eapply transitivity.
+      set (ni_commutes (mf_second(PreMonoidalFunctor:=reification_rstar reification) a) f) as qq.
+      unfold functor_comp in qq.
+      simpl in qq.
+      apply iso_shift_right' in qq.
+      apply (fmor_respects(R' >>>> step2_functor) _ _ qq).
+
+    apply (me_faithful(MonicEnrichment:=CMon)).
+      symmetry.
+      unfold fmor at 1.
+      eapply transitivity.
+      set (ni_commutes (mf_second(PreMonoidalFunctor:=CM) (R' a))) as zz.
+      unfold functor_comp in zz; unfold functor_fobj in zz; simpl in zz.
+      set (zz _ _ ((R' >>>> step2_functor) \ (reification \ f))) as zz'.
+      apply iso_shift_right' in zz'.
+      apply zz'.
+
+    unfold functor_comp; simpl.
+
+    symmetry.
+      eapply transitivity.
+      set full_roundtrip as full_roundtrip'.
+      unfold fmor in full_roundtrip'.
+      simpl in full_roundtrip'.
+      apply full_roundtrip'.
+
+    set (@iso_shift_right') as q. simpl in q. apply q. clear q.
+
+    set (@iso_shift_left) as q.   simpl in q. apply q. clear q.
+
+    symmetry.
+      eapply transitivity.
+      set full_roundtrip as full_roundtrip'.
+      unfold fmor in full_roundtrip'.
+      simpl in full_roundtrip'.
+      apply (fun a' b' f z => fmor_respects (bin_second(BinoidalCat:=enr_v_bin C) z) _ _ (full_roundtrip' a' b' f)).
+      symmetry.
+
+    intros.
+      unfold bin_obj.
+      unfold senr_v_bobj.
+
+    setoid_rewrite <- associativity.
+      setoid_rewrite <- associativity.
+      setoid_rewrite <- associativity.
+      setoid_rewrite <- associativity.
+      simpl.
+      setoid_rewrite <- associativity.
+      etransitivity.
+      eapply transitivity.
+        apply associativity.
+        eapply transitivity; [ idtac | apply right_identity ].
+        apply comp_respects; [ reflexivity | idtac ].
+        etransitivity.
+        apply comp_respects; [ idtac | reflexivity ].
+        apply (mf_consistent(PreMonoidalFunctor:=CM)).
+        apply iso_comp1.
+
+    eapply transitivity.
+      eapply comp_respects; [ idtac | reflexivity ].
+      eapply comp_respects; [ idtac | reflexivity ].
+      eapply comp_respects; [ idtac | reflexivity ].
+      eapply comp_respects; [ idtac | reflexivity ].
+      eapply transitivity.
+        eapply symmetry.
+        eapply associativity.
+      eapply transitivity; [ idtac | apply left_identity ].
+      eapply comp_respects; [ idtac | reflexivity ].
+      eapply transitivity.
+        eapply comp_respects; [ idtac | reflexivity ].
+        eapply symmetry.
+        apply (mf_consistent(PreMonoidalFunctor:=CM)).
+        apply iso_comp1.
+
+    eapply symmetry.
+      eapply transitivity.
+      setoid_rewrite <- fmor_preserves_comp.
+      setoid_rewrite <- fmor_preserves_comp.
+      eapply reflexivity.
+      eapply symmetry.
+
+    apply comp_respects; try reflexivity.
+
+    eapply transitivity.
+      apply associativity.
+      eapply transitivity.
+      apply associativity.
+      eapply transitivity.
+      apply associativity.
+      eapply transitivity.
+      apply associativity.
+      apply comp_respects; try reflexivity.
+
+    eapply transitivity.
+      eapply comp_respects; [ reflexivity | idtac ].
+      eapply transitivity.
+      eapply comp_respects; [ idtac | reflexivity ].
+      apply mf_consistent.
+      eapply transitivity.
+      eapply comp_respects; [ reflexivity | idtac ].
+        apply associativity.
+      apply iso_comp1_right.
+
+    eapply transitivity.
+      eapply comp_respects; [ reflexivity | idtac ].
+      eapply transitivity.
+        apply associativity.
+      eapply comp_respects; [ reflexivity | idtac ].
+      eapply transitivity.
+        eapply symmetry.
+        apply associativity.
+      eapply transitivity; [ idtac | apply left_identity ].
+      eapply comp_respects; [ idtac | reflexivity ].
+      eapply transitivity.
+        eapply comp_respects; [ idtac | reflexivity ].
+        eapply symmetry.
+        eapply (mf_consistent(PreMonoidalFunctor:=reification)).
+      apply iso_comp1.
+
+    eapply transitivity.
+      eapply comp_respects; [ reflexivity | idtac ].
+      eapply symmetry.
+      apply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)).
+      eapply transitivity; [ idtac | apply right_identity ].
+
+    eapply transitivity.
+      eapply symmetry.
+      apply associativity.
+    eapply transitivity.
+      eapply comp_respects; [ idtac | reflexivity ].
+      unfold functor_fobj.
+      apply (fmor_preserves_comp (bin_first(BinoidalCat:=enr_v_bin C) (reification_rstar_obj reification A))).
+
+    apply symmetry.
+      eapply transitivity.
+      apply right_identity.
+      apply symmetry.
+      eapply transitivity; [ idtac | apply left_identity ].
+      apply comp_respects; [ idtac | reflexivity ].
+
+    eapply transitivity.
+      Focus 2.
+      eapply (fmor_preserves_id (bin_first(BinoidalCat:=enr_v_bin C) (reification_rstar_obj reification A))).
+      idtac.
+      apply (fmor_respects (bin_first(BinoidalCat:=enr_v_bin C) (reification_rstar_obj reification A))).
+      apply iso_comp2.
     Defined.
 
 Implicit Arguments mf_first [[Ob] [Hom] [C1] [bin_obj'] [bc] [I1] [PM1] [Ob0] [Hom0] [C2] [bin_obj'0] [bc0] [I2] [PM2] [fobj] [F]].
 Implicit Arguments mf_second [[Ob] [Hom] [C1] [bin_obj'] [bc] [I1] [PM1] [Ob0] [Hom0] [C2] [bin_obj'0] [bc0] [I2] [PM2] [fobj] [F]].
 Implicit Arguments mf_i [[Ob] [Hom] [C1] [bin_obj'] [bc] [I1] [PM1] [Ob0] [Hom0] [C2] [bin_obj'0] [bc0] [I2] [PM2] [fobj] [F]].
 
+  Lemma assoc_lemma1 : forall a b c,
+       iso_backward ((mf_first reification c) (a ⊗ b)) >>>
+       iso_backward ((mf_second reification a) b) ⋉ reification c >>>
+      #(pmon_assoc(PreMonoidalCat:=enr_v_mon C) (reification a) (reification c) (reification_rstar_obj reification b)) >>>
+      reification a ⋊ #((mf_first reification c) b) >>>
+      #((mf_second reification a) (b ⊗ c)) ~~
+      reification \ #((pmon_assoc(PreMonoidalCat:=enr_v_mon K) a c) b).
+
+    intros.
+      eapply transitivity.
+        apply associativity.
+        eapply transitivity.
+        apply associativity.
+        eapply transitivity.
+        apply associativity.
+        apply symmetry.
+        set (@iso_shift_right') as q.
+        simpl in q.
+        apply q.
+        clear q.
+        
+      eapply symmetry.
+        eapply transitivity.
+        apply comp_respects; [ reflexivity | idtac ].
+        set (mf_assoc(PreMonoidalFunctor:=reification)) as q.
+        eapply transitivity.
+        eapply symmetry.
+        apply associativity.
+        apply q.
+
+      eapply transitivity.
+        eapply symmetry.
+        apply associativity.
+        apply comp_respects; try reflexivity.
+        eapply transitivity.
+        eapply symmetry.
+        apply associativity.
+        eapply transitivity; [ idtac | apply left_identity ].
+        apply comp_respects; try reflexivity.
+      
+      eapply transitivity.
+        apply (fmor_preserves_comp (bin_first(BinoidalCat:=enr_v_bin C) _)).
+      eapply transitivity; [ idtac |
+        apply (fmor_preserves_id (bin_first(BinoidalCat:=enr_v_bin C) _)) ].
+      apply (fmor_respects (bin_first(BinoidalCat:=enr_v_bin C) _)).
+      apply iso_comp2.
+      Qed.
+
+  Lemma assoc_lemma2 : forall a b c,
+       iso_backward ((mf_first CM (garrow_fobj c)) _) >>>
+       (bin_first(BinoidalCat:=enr_v_bin C) _ \ iso_backward ((mf_second CM (garrow_fobj a)) (garrow_fobj b))) >>> 
+       (#((pmon_assoc(PreMonoidalCat:=enr_v_mon C) _ _) _) >>>
+        (bin_second(BinoidalCat:=enr_v_bin C) _ \ 
+         #((mf_first CM (garrow_fobj c)) (garrow_fobj b)))) >>>
+       #((mf_second CM (garrow_fobj a)) _) ~~
+       HomFunctor C _ \ #((pmon_assoc(PreMonoidalCat:=enr_c_pm C) (garrow_fobj a) (garrow_fobj c)) (garrow_fobj b)).
+    intros.
+      eapply transitivity.
+        apply associativity.
+        eapply transitivity.
+        apply associativity.
+        set (@iso_shift_right') as q.
+        apply symmetry.
+        simpl in q.
+        apply q.
+        clear q.
+        
+      eapply symmetry.
+        eapply transitivity.
+        apply comp_respects; [ reflexivity | idtac ].
+        set (mf_assoc(PreMonoidalFunctor:=CM)) as q.
+        apply q.
+
+      eapply transitivity.
+        eapply symmetry.
+        apply associativity.
+        apply comp_respects; try reflexivity.
+        eapply transitivity.
+          eapply symmetry.
+          apply associativity.
+        eapply transitivity; [ idtac | apply left_identity ].
+        apply comp_respects; try reflexivity.
+
+      eapply transitivity.
+        apply (fmor_preserves_comp (bin_first(BinoidalCat:=enr_v_bin C) _)).
+      eapply transitivity; [ idtac |
+        apply (fmor_preserves_id (bin_first(BinoidalCat:=enr_v_bin C) _)) ].
+      apply (fmor_respects (bin_first(BinoidalCat:=enr_v_bin C) _)).
+      apply iso_comp2.
+      Qed.
+
+  Lemma assoc_coherent (a b c : enr_v K) :
+   (#((pmon_assoc(PreMonoidalCat:=enr_c_pm C)
+     (garrow_functor a) (garrow_functor c)) (garrow_fobj b)) >>> garrow_functor a ⋊ #((garrow_first c) b)) >>>
+   #((garrow_second a) (b ⊗ c)) ~~
+   (#((garrow_second a) b) ⋉ garrow_functor c >>>
+     #((garrow_first c) (a ⊗ b))) >>> garrow_functor \ #((pmon_assoc(PreMonoidalCat:=enr_v_mon K) a c) b).
+    Opaque Underlying.
+    eapply transitivity.
+      eapply transitivity; [ idtac | apply right_identity ].
+      eapply comp_respects; [ eapply reflexivity | idtac ].
+      reflexivity.
+
+    apply symmetry.
+      eapply transitivity.
+      eapply transitivity; [ idtac | apply left_identity ].
+      eapply comp_respects; [ idtac | eapply reflexivity ].
+      eapply transitivity; [ idtac | apply right_identity ].
+      apply comp_respects.
+      simpl.
+      apply (fmor_preserves_id (ebc_first (garrow_functor c))).
+      reflexivity.
+
+    symmetry.
+      eapply transitivity.
+      eapply transitivity; [ idtac | apply right_identity ].
+      apply comp_respects. 
+      reflexivity.
+      simpl.
+      apply (fmor_preserves_id (ebc_second (garrow_functor a))).
+      symmetry.
+
+    unfold functor_fobj.
+      unfold garrow_functor.
+      unfold step2_functor.
+      Opaque R'.
+      Opaque ff_functor_section_functor.
+      unfold functor_comp.
+      simpl.
+      Transparent R'.
+      Transparent ff_functor_section_functor.
+      idtac.
+      apply (me_faithful(MonicEnrichment:=CMon)).
+      eapply transitivity; [ eapply full_roundtrip | idtac ].
+
+    unfold fmor at 1.
+      unfold R'.
+      unfold me_homfunctor.
+      eapply transitivity.
+        eapply comp_respects; [ idtac | apply reflexivity ].
+        eapply comp_respects; [ apply reflexivity | idtac ].
+        eapply symmetry.
+        apply assoc_lemma1.
+
+      apply symmetry.
+        eapply transitivity.
+        eapply symmetry.
+        apply assoc_lemma2.
+
+      simpl.
+        eapply transitivity.
+        eapply comp_respects; [ apply reflexivity | idtac ].
+        eapply symmetry.
+        eapply (mf_consistent(PreMonoidalFunctor:=CM)).
+        apply symmetry.
+        eapply transitivity.
+        eapply symmetry.
+        apply associativity.
+        apply comp_respects; [ idtac | apply reflexivity ].
+
+      eapply transitivity.
+        apply associativity.
+        eapply transitivity.
+        apply associativity.
+        symmetry.
+        eapply transitivity.
+        apply associativity.
+        apply comp_respects; [ reflexivity | idtac ].
+
+      apply symmetry.
+        eapply transitivity.
+        apply comp_respects; [ reflexivity | idtac ].
+        eapply transitivity.
+        eapply symmetry.
+        apply associativity.
+        eapply transitivity.
+        apply comp_respects; [ idtac | reflexivity ].
+        eapply transitivity.
+        apply associativity.
+        eapply transitivity.
+        eapply transitivity.
+        apply comp_respects; [ reflexivity | idtac ].
+        apply comp_respects; [ idtac | reflexivity ].
+        eapply symmetry.
+        apply (mf_consistent(PreMonoidalFunctor:=reification)).
+        apply comp_respects; [ reflexivity | idtac ].
+        apply iso_comp1.
+        apply right_identity.
+        eapply transitivity.
+        eapply symmetry.
+        apply associativity.
+        eapply transitivity.
+        apply comp_respects; [ idtac | reflexivity ].
+        eapply transitivity.
+        apply associativity.
+        apply comp_respects; [ reflexivity | idtac ].
+        eapply symmetry.
+        eapply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)).        
+        eapply transitivity.
+        eapply transitivity.
+        apply comp_respects; [ reflexivity | idtac ].
+        eapply transitivity.
+          eapply symmetry.
+          apply (fmor_preserves_comp (bin_second(BinoidalCat:=enr_v_mon C) _)).
+        apply comp_respects; [ idtac | reflexivity ].
+        eapply symmetry.
+          apply (fmor_preserves_comp (bin_second(BinoidalCat:=enr_v_mon C) _)).
+        apply comp_respects; [ reflexivity | idtac ].
+          apply associativity.
+        eapply transitivity.
+          eapply symmetry.
+          apply associativity.
+        apply comp_respects; [ idtac | reflexivity ].
+        eapply transitivity.
+        eapply transitivity.
+        apply associativity.
+        apply comp_respects; [ reflexivity | idtac ].
+        eapply transitivity.
+        apply associativity.
+        eapply transitivity; [ idtac | apply right_identity ].
+        apply comp_respects; [ reflexivity | idtac ].
+        eapply transitivity.
+        apply (fmor_preserves_comp (bin_second(BinoidalCat:=enr_v_mon C) _)).
+        eapply transitivity; [ idtac |
+        apply (fmor_preserves_id (bin_second(BinoidalCat:=enr_v_mon C) _)) ].
+        apply (fmor_respects (bin_second(BinoidalCat:=enr_v_mon C) _)).
+        apply iso_comp1.
+        apply reflexivity.
+
+      eapply transitivity.
+        eapply symmetry.
+        apply associativity.
+        eapply transitivity.
+        eapply symmetry.
+        apply associativity.
+        eapply symmetry.
+        eapply transitivity.
+        eapply symmetry.
+        apply associativity.
+        apply comp_respects; [ idtac | reflexivity ].
+
+      apply symmetry.
+        eapply transitivity.
+        apply comp_respects; [ idtac | reflexivity ].
+        eapply transitivity.
+        apply associativity.
+        apply comp_respects; [ reflexivity | idtac ].
+        eapply transitivity.
+        eapply symmetry.
+        apply associativity.
+        apply comp_respects; [ idtac | reflexivity ].
+        eapply transitivity.
+        apply comp_respects; [ reflexivity | idtac ].
+        apply associativity.
+        apply iso_comp1_right.
+
+      eapply transitivity.
+        apply comp_respects; [ idtac | reflexivity ].
+        eapply transitivity.
+        apply comp_respects; [ reflexivity | idtac ].
+        apply associativity.
+        eapply transitivity.
+        eapply symmetry.
+        apply associativity.
+        apply comp_respects; [ idtac | reflexivity ].
+        eapply transitivity.
+        apply comp_respects; [ idtac | reflexivity ].
+        eapply transitivity.
+        apply comp_respects; [ reflexivity | idtac ].
+        eapply transitivity.
+        eapply symmetry.
+        apply (fmor_preserves_comp (bin_first(BinoidalCat:=enr_v_bin C) _)).
+        eapply transitivity.
+        apply comp_respects; [ reflexivity | idtac ].
+        eapply symmetry.
+        apply (fmor_preserves_comp (bin_first(BinoidalCat:=enr_v_bin C) _)).
+        eapply symmetry.
+        apply associativity.
+        eapply symmetry.
+        apply associativity.
+        apply reflexivity.
+        eapply transitivity.
+        apply comp_respects; [ idtac | reflexivity ].
+        apply comp_respects; [ idtac | reflexivity ].
+        eapply transitivity.
+          apply associativity.
+        eapply transitivity; [ idtac | apply right_identity ].
+        apply comp_respects; [ reflexivity | idtac ].
+        eapply transitivity.
+        apply (fmor_preserves_comp (bin_first(BinoidalCat:=enr_v_bin C) _)).
+        eapply transitivity; [ idtac | apply (fmor_preserves_id (bin_first(BinoidalCat:=enr_v_mon C) _)) ].
+        apply (fmor_respects (bin_first(BinoidalCat:=enr_v_mon C) _)).
+        eapply transitivity.
+          apply comp_respects; [ idtac | reflexivity ].
+          eapply mf_consistent.
+          apply iso_comp1.
+
+      eapply transitivity.
+        apply associativity.
+        eapply transitivity.
+        apply comp_respects; [ idtac | reflexivity ].
+        eapply transitivity.
+        eapply symmetry.
+        apply associativity.
+        apply comp_respects; [ idtac | reflexivity ].
+        eapply symmetry.
+        eapply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)).
+        eapply transitivity.
+        apply associativity.
+        eapply transitivity.
+        apply associativity.
+        set (fun a b => isos_forward_equal_then_backward_equal _ _ (mf_consistent(PreMonoidalFunctor:=CM) a b)) as q.
+        apply symmetry.
+        eapply transitivity.
+        apply comp_respects; [ idtac | reflexivity ].
+        set (q (garrow_fobj b) (garrow_fobj a)) as q'.
+        simpl in q'.
+        set (fun qq => fmor_respects (bin_first(BinoidalCat:=enr_v_bin C) qq) _ _ q') as q''.
+        eapply symmetry.
+        apply q''.
+        apply comp_respects; [ reflexivity | idtac ].
+
+      apply symmetry.
+        eapply transitivity.
+        apply comp_respects; [ reflexivity | idtac ].
+        apply comp_respects; [ reflexivity | idtac ].
+        apply comp_respects; [ idtac | reflexivity ].
+        set (ni_commutes (pmon_assoc_rr(PreMonoidalCat:=enr_v_mon C) (reification b) (reification c))
+                          #(homset_tensor_iso a)) as xx.
+        unfold functor_comp in xx.
+        simpl in xx.
+        set (pmon_coherent_r(PreMonoidalCat:=enr_v_mon C) (reification a) (reification b) (reification c)) as yy.
+          set (isos_forward_equal_then_backward_equal _ _ yy) as yy'.
+          eapply transitivity.
+          apply comp_respects; [ idtac | reflexivity ].
+          apply symmetry in yy'.
+          eapply transitivity; [ idtac | apply yy' ].
+          eapply symmetry.
+          apply iso_inv_inv.
+        clear yy' yy.
+          apply iso_shift_right' in xx.
+          apply symmetry in xx.
+          idtac.
+          assert (#((pmon_assoc_rr(PreMonoidalCat:=enr_v_mon C) (reification b) (reification c)) (reification a)) ⁻¹ >>>
+       #(homset_tensor_iso a) ⋉ (reification b ⊗ reification c)
+         ~~
+       (#(homset_tensor_iso a) ⋉ reification b) ⋉ reification c >>>
+       #((pmon_assoc_rr(PreMonoidalCat:=enr_v_mon C) (reification b) (reification c)) _)⁻¹).
+          apply iso_shift_left.
+          eapply transitivity.
+          apply associativity.
+          apply xx.
+          apply H.
+          clear q.
+        eapply transitivity.
+          apply comp_respects; [ reflexivity | idtac ].
+          eapply transitivity.
+          apply comp_respects; [ idtac | reflexivity ].
+          eapply symmetry.
+          apply (fmor_preserves_comp (bin_first(BinoidalCat:=enr_v_mon C) _)).
+          eapply transitivity.
+          apply associativity.
+          apply comp_respects; [ reflexivity | idtac ].
+          eapply transitivity.
+          eapply symmetry.
+          apply associativity.
+          apply comp_respects; [ idtac | reflexivity ].
+          eapply transitivity.
+          eapply symmetry.
+          apply associativity.
+          eapply transitivity; [ idtac | apply left_identity ].
+          apply comp_respects; [ idtac | reflexivity ].
+          eapply transitivity.
+            apply (fmor_preserves_comp (bin_first(BinoidalCat:=enr_v_bin C) _)).
+          eapply transitivity; [ idtac |
+            apply (fmor_preserves_id (bin_first(BinoidalCat:=enr_v_bin C) _)) ].
+          apply (fmor_respects (bin_first(BinoidalCat:=enr_v_bin C) _)).
+          eapply transitivity.
+            apply (fmor_preserves_comp (bin_first(BinoidalCat:=enr_v_bin C) _)).
+          eapply transitivity; [ idtac |
+            apply (fmor_preserves_id (bin_first(BinoidalCat:=enr_v_bin C) _)) ].
+          apply (fmor_respects (bin_first(BinoidalCat:=enr_v_bin C) _)).
+          apply iso_comp2.
+          
+      set (fun a' => ni_commutes (pmon_assoc(PreMonoidalCat:=enr_v_mon C) a' (reification c))
+        (iso_backward (homset_tensor_iso b))) as xx.
+        unfold fmor in xx; unfold functor_comp in xx; simpl in xx.
+        eapply transitivity.
+        apply comp_respects; [ reflexivity | idtac ].
+        eapply transitivity.
+        eapply symmetry.
+        eapply associativity.
+        apply comp_respects; [ idtac | reflexivity ].
+        eapply transitivity.
+        apply comp_respects; [ reflexivity | idtac ].
+        eapply transitivity.
+          eapply isos_forward_equal_then_backward_equal.
+          apply (pmon_coherent_r(PreMonoidalCat:=enr_v_mon C)).
+          apply iso_inv_inv.
+          eapply symmetry.
+          eapply xx.
+          clear xx.
+        eapply transitivity.
+          apply comp_respects; [ reflexivity | idtac ].
+          eapply transitivity.
+          eapply associativity.
+          apply comp_respects; [ reflexivity | idtac ].
+          eapply transitivity.
+          apply comp_respects; [ reflexivity | idtac ].
+          eapply symmetry.
+          apply (fmor_preserves_comp (bin_second(BinoidalCat:=enr_v_bin C) _)).
+          eapply transitivity.
+          eapply symmetry.
+          eapply associativity.
+          eapply transitivity; [ idtac | apply left_identity ].
+          apply comp_respects; [ idtac | reflexivity ].
+          eapply transitivity.
+            apply (fmor_preserves_comp (bin_second(BinoidalCat:=enr_v_bin C) _)).
+            eapply transitivity; [ idtac |
+            apply (fmor_preserves_id (bin_second(BinoidalCat:=enr_v_bin C) _)) ].
+            apply fmor_respects.
+          eapply transitivity.
+            apply (fmor_preserves_comp (bin_first(BinoidalCat:=enr_v_bin C) _)).
+            eapply transitivity; [ idtac |
+            apply (fmor_preserves_id (bin_first(BinoidalCat:=enr_v_bin C) _)) ].
+            apply (fmor_respects (bin_first(BinoidalCat:=enr_v_bin C) _)).
+          apply iso_comp2.
+        
+      set (fun a b => ni_commutes (pmon_assoc_ll(PreMonoidalCat:=enr_v_mon C) a b)) as xx.
+        unfold functor_comp in xx.
+        simpl in xx.
+        eapply transitivity.
+        apply comp_respects; [ reflexivity | idtac ].
+        eapply transitivity.
+          apply comp_respects; [ idtac | reflexivity ].
+          eapply symmetry.
+          apply (pmon_coherent_l(PreMonoidalCat:=enr_v_mon C)).
+          apply xx.
+        eapply transitivity.
+          eapply symmetry.
+          apply associativity.
+        apply symmetry.
+          eapply transitivity.
+          eapply symmetry.
+          apply (pmon_coherent_l(PreMonoidalCat:=enr_v_mon C)).
+        apply symmetry.
+        eapply transitivity; [ idtac | apply left_identity ].
+          apply comp_respects; [ idtac | reflexivity ].
+        eapply transitivity.
+          apply (fmor_preserves_comp (bin_second(BinoidalCat:=enr_v_bin C) _)).
+          eapply transitivity; [ idtac |
+          apply (fmor_preserves_id (bin_second(BinoidalCat:=enr_v_bin C) _)) ].
+          apply fmor_respects.
+          apply iso_comp2.
+      Qed.
+
   Lemma cancell_lemma `(F:PreMonoidalFunctor) b :
     iso_backward (mf_i F) ⋉ (F b) >>> #(pmon_cancell (F b)) ~~
     #((mf_first F b) _) >>>  F \ #(pmon_cancell b).
@@ -296,7 +916,7 @@ Implicit Arguments mf_i [[Ob] [Hom] [C1] [bin_obj'] [bc] [I1] [PM1] [Ob0] [Hom0]
     apply (fmor_respects (-⋉ F b)).
     apply iso_comp2.
     Qed.
-
+*)
   Lemma cancell_coherent (b:enr_v K) :
    #(pmon_cancell(PreMonoidalCat:=enr_c_pm C) (garrow_functor b)) ~~
    (#(iso_id (enr_c_i C)) ⋉ garrow_functor b >>>
@@ -407,20 +1027,23 @@ Implicit Arguments mf_i [[Ob] [Hom] [C1] [bin_obj'] [bc] [I1] [PM1] [Ob0] [Hom0]
     set (@comp_respects) as qq.
     unfold Proper in qq.
     unfold respectful in qq.
-    set (qq _ _ _ _ _ _ (iso_backward (mf_i F) ⋉ F b) (iso_backward (mf_i F) ⋉ F b) (reflexivity _) _ _ q) as q'.
+    set (qq _ _ _ _ _ _ (F b ⋊ iso_backward (mf_i F)) (F b ⋊ iso_backward (mf_i F)) (reflexivity _) _ _ q) as q'.
     setoid_rewrite <- associativity in q'.
     clear q qq.
-    setoid_rewrite (fmor_preserves_comp (-⋉ F b)) in q'.
+    setoid_rewrite (fmor_preserves_comp (F b ⋊ -)) in q'.
     eapply transitivity; [ apply q' | idtac ].
     clear q'.
     setoid_rewrite <- associativity.
     apply comp_respects; try reflexivity.
     symmetry.
     apply iso_shift_left.
+    eapply transitivity.
+      apply comp_respects; [ idtac | reflexivity ].
+      apply mf_consistent.
     setoid_rewrite iso_comp1.
     symmetry.
-    eapply transitivity; [ idtac | eapply (fmor_preserves_id (-⋉ F b))].
-    apply (fmor_respects (-⋉ F b)).
+    eapply transitivity; [ idtac | eapply (fmor_preserves_id (F b ⋊ - ))].
+    apply (fmor_respects (F b ⋊ -)).
     apply iso_comp2.
     Qed.
 
@@ -428,7 +1051,6 @@ Implicit Arguments mf_i [[Ob] [Hom] [C1] [bin_obj'] [bc] [I1] [PM1] [Ob0] [Hom0]
    #(pmon_cancelr(PreMonoidalCat:=enr_c_pm C) (garrow_functor b)) ~~
    (garrow_functor b ⋊ #(iso_id (enr_c_i C)) >>>
     #((garrow_second b) (enr_v_i K))) >>> garrow_functor \ #(pmon_cancelr(PreMonoidalCat:=enr_v_mon K) b).
-
     Opaque Underlying.
     Opaque fmor.
     intros; simpl.
@@ -534,21 +1156,16 @@ Implicit Arguments mf_i [[Ob] [Hom] [C1] [bin_obj'] [bc] [I1] [PM1] [Ob0] [Hom0]
   ; mf_second     := garrow_second
   ; mf_i          := iso_id _ }.
     intros; reflexivity.
-    intros.
-      unfold garrow_functor.
-      unfold fmor.
-      Opaque fmor. simpl.
-      unfold step2_functor.
-      admit.
-      Transparent fmor.
-
+    intros; apply (reification_host_lang_pure _ _ _ reification).
     apply cancell_coherent.
     apply cancelr_coherent.
-    admit.
+    apply assoc_coherent.
     Defined.
 
   Definition garrow_from_reification : GeneralizedArrow K CM :=
-    {| ga_functor_monoidal := garrow_monoidal |}.
+    {| ga_functor_monoidal := garrow_monoidal
+     ; ga_host_lang_pure   := reification_host_lang_pure _ _ _ reification
+    |}.
 
 End GArrowFromReification.