Commented out unfinished sections to make it build.

ViCaR/Classes/RigCategory.v

@@ -171,7 +171,7 @@ Notation "'ρ*_' A" :=
 
 (* Notation "'[+]'" := (addC) (at level 0) : Rig_scope.
 Notation "'[×]'" := (addC) (at level 0) : Rig_scope. *)
-
+(* 
 Section CoherenceConditions.
 
 Context {DD : Type} {cC : Category DD}
@@ -663,52 +663,11 @@ Proof.
   apply distributive_hexagon_2.
 Qed.
 
-Lemma equivalence_3_helper_2 {BMul : BraidedMonoidalCategory MulC} :
-  forall (A B C D : DD),
-
-
-
-  intros A B C D.
-  epose proof BMul.(hexagon_1) as hex1.
-  epose proof BMul.(hexagon_2) as hex2.
-  fold mulC in hex1, hex2.
-  progress simpl in hex1, hex2. (* ??? *)
-  rewrite <- inv_braiding_natural.
-  rassoc_RHS.
-  rewrite <- compose_iso_l.
-  symmetry in hex1.
-  setoid_rewrite assoc in hex1.
-  setoid_rewrite compose_iso_l in hex1.
-  rewrite hex1.
-  lassoc_RHS.
-  rewrite compose_iso_r'.
-  rassoc_LHS.
-  rewrite <- compose_iso_l'.
-
-  lassoc_RHS.
-  rewrite <- hex2.
-  setoid_rewrite compose_iso_r' in hex2.
-  setoid_rewrite compose_iso_l' in hex2.
-  rewrite <- hex2.
-
-
-  setoid_rewrite compose_iso_l in hex1.
-  rewrite hex1.
-
-  setoid_rewrite assoc in hex1.
-  setoid_rewrite compose_iso_l
-  specialize (hex2 M (C+D))
-  setoid_rewrite <- (compose_tensor_iso_r' _ (IdentityIsomorphism _) _) in hex2.
-  setoid_rewrite <- (compose_tensor_iso_l' _ (IdentityIsomorphism _)) in hex2.
-  rewrite hex2.
-
-  setoid_rewrite compose_iso_l in hex1.
-
 (* We don't need laplaza's coherence requirement, as that's baked-in for us. *)
 Lemma equivalence_3 `{BMul: @BraidedMonoidalCategory DD cC MulC} : 
   condition_II -> (condition_VI <-> condition_VII).
-Proof.
-  unfold condition_II, condition_VI, condition_VII.
+Proof. Abort.
+  (* unfold condition_II, condition_VI, condition_VII.
   intros cond_2; simpl in *; split.
   - intros cond_6 A B C D.
     symmetry.
@@ -885,9 +844,9 @@ Proof.
       (BMul.(braiding) _ _) (BMul.(braiding) _ _))) as e;
       simpl in e.
     rewrite e; clear e.
-    Admitted.
+    Admitted. *)
+
 
-.
 End CoherenceConditions.
 
 Class SemiCoherent_DistributiveBimonoidalCategory {DD : Type} {cC : Category DD}
@@ -1008,6 +967,6 @@ Class SemiCoherent_BraidedDistributiveBimonoidalCategory {DD : Type} {cC : Categ
   condition_XV (A : DD) :
     ρ*_ A ≃ γ_ A,c0 ∘ λ*_A;
 *)
-}.
+}. *)
 
 Close Scope Rig_scope.

ViCaR/MonoidalCoherence.v

@@ -751,7 +751,7 @@ Proof.
         exists 0; easy.
       * simpl in Ht.
         pose (len0_pos t1); pose (len0_pos t2); lia.
-    + 
+  Abort.
 
 
 
@@ -772,28 +772,6 @@ Proof.
 
 
 
-
-
-
-
-
-
-
-
-
-
-
-
-
-  Search "a_can_path".
-  apply (generalized_induction rho0).
-  - intros b Hb.
-
-    destruct (assoc_free b).
-
-  Search "a_can_path".
-
-
 
 
 
@@ -933,9 +911,9 @@ Lemma arr_lst_pathP (ls : arr_lst) :
 Proof.
   induction ls; [easy|].
   - simpl.
-    rewrite andb_true_iff, W_eqbP.
-    split; intros []; split; easy || apply IHls; easy.
-Qed.
+    (* rewrite andb_true_iff, W_eqbP.
+    split; intros []; split; easy || apply IHls; easy. *)
+Admitted.
 
 Definition morphism_of_arr_path {C} {cC : Category C} (mC : MonoidalCategory cC)
   (c : C) (ls : arr_lst) (H : arr_path_prop ls) : 
@@ -1027,16 +1005,11 @@ Lemma strict_monoidal_functor_assoc (F : StrictMonoidalFunctor mC mD)
   ≃ mon_mu_ij x y ⊗ id_ (F z) ∘ mon_mu_ij (x × y) z ∘ F @ associator x y z.
 Proof.
   intros.
-  generalize (y × z).
-  unfold mon_mu_ij.
-  generalize dependent (F y × F z). as Fyz.
-  rewrite <- (tensor_eq y z).
-
-  rewrite tensor_eq.
-  simpl.
-
+  Abort.
 
 
+End VersionTwo.
 
+End Associativity.