From 16bde81cc5adcb33ebfb12153c047d1715f692ca Mon Sep 17 00:00:00 2001
From: William Spencer <wjbs@uchicago.edu>
Date: Mon, 11 Mar 2024 19:13:06 -0500
Subject: [PATCH] Significantly improved category automation. Fenceposting has
 been implemented in Ltac, and appears to be correct in some limited tests.
 More testing should be done. Performance is also poor at the moment: there
 are some fixes that should be possible immediately, but other issues
 (particularly with to_Cat) may require a tradeoff of speed and efficacy
 (which can be shifted onto the user with multiple tactics). Also, Universe
 Polymorphism has been enabled in all category files, so that Categories whose
 morphisms have specific universes (really, 'whose morphisms are in Set') play
 nicely. We now have 'ZXCategory.(morphism) = ZX', which previously failed due
 to universe constraints, and in doing so significantly hampered automation
 (which requires conversion of the local context to category names so it can
 match on them).

---
 ViCaR/CategoryAutomation.v                    | 1549 +++++++++++++++++
 ViCaR/Classes/BraidedMonoidal.v               |    2 +
 ViCaR/Classes/CastCategory.v                  |   24 +-
 ViCaR/Classes/Category.v                      |    4 +-
 ViCaR/Classes/CategoryAutomation.v            |  305 ----
 ViCaR/Classes/CompactClosed.v                 |    2 +
 ViCaR/Classes/Dagger.v                        |    2 +
 ViCaR/Classes/DaggerBraidedMonoidal.v         |    2 +
 ViCaR/Classes/DaggerMonoidal.v                |    2 +
 ViCaR/Classes/DaggerSymmetricMonoidal.v       |    2 +
 ViCaR/Classes/Monoidal.v                      |    2 +
 ViCaR/Classes/RigCategory.v                   |    4 +-
 ViCaR/Classes/SymmetricMonoidal.v             |    2 +
 ViCaR/GeneralLemmas.v                         |  144 +-
 examples/DirectSumMatrixExample.v             |    2 +-
 .../Classes => examples}/ExamplesAutomation.v |    0
 examples/KronComm.v                           |    2 +-
 examples/KronComm_orig.v                      |   12 +-
 examples/KronMatrixExample.v                  |    2 +-
 examples/MatrixExampleBase.v                  |    2 +-
 examples/MatrixPermBase.v                     |    2 +-
 examples/NatRelationsExample.v                |    2 +-
 examples/ZXExample.v                          |   33 +-
 23 files changed, 1636 insertions(+), 467 deletions(-)
 create mode 100644 ViCaR/CategoryAutomation.v
 delete mode 100644 ViCaR/Classes/CategoryAutomation.v
 rename {ViCaR/Classes => examples}/ExamplesAutomation.v (100%)

diff --git a/ViCaR/CategoryAutomation.v b/ViCaR/CategoryAutomation.v
new file mode 100644
index 0000000..03e9ca8
--- /dev/null
+++ b/ViCaR/CategoryAutomation.v
@@ -0,0 +1,1549 @@
+Require Export CategoryTypeclass.
+
+#[local] Set Universe Polymorphism.
+
+Local Close Scope Cat_scope. (* We do _not_ want to be relying on the scope for 
+  this automation to work! This will easily break things, as Ltac is not
+  type-checked (so is functionally a macro and thus notation is 
+  context-dependent). *)
+
+Ltac print_state :=
+  try (match goal with | H : ?p |- _ => idtac H ":" p; fail end);
+  idtac "---------------------------------------------------------";
+  match goal with |- ?P => idtac P 
+end.
+
+Ltac assert_not_dup x := 
+  (* try match goal with *)
+  try match goal with
+  | f := ?T : ?T', g := ?T : ?T' |- _ => tryif unify x f then fail 2 else fail 1
+  end.
+
+Ltac saturate_instances class :=
+  (progress repeat ( (* TODO: test to make sure, but || is supposed to progress, so this shouldn't need progress explicitly?*)
+    let x:= fresh in let o := open_constr:(class _) in
+    unshelve evar (x:o); [typeclasses eauto|]; 
+    (* let t:= type of x in idtac x ":" t; *) assert_not_dup x))
+  || (progress repeat (
+    let x:= fresh in let o := open_constr:(class _ _) in
+    unshelve evar (x:o); [typeclasses eauto|]; assert_not_dup x))
+  || (progress repeat (
+    let x:= fresh in let o := open_constr:(class _ _ _) in
+    unshelve evar (x:o); [typeclasses eauto|]; assert_not_dup x))
+  || (progress repeat (
+    let x:= fresh in let o := open_constr:(class _ _ _ _) in
+    unshelve evar (x:o); [typeclasses eauto|]; assert_not_dup x))
+  || (progress repeat (
+    let x:= fresh in let o := open_constr:(class _ _ _ _ _) in
+    unshelve evar (x:o); [typeclasses eauto|]; assert_not_dup x))
+  || (progress repeat (
+    let x:= fresh in let o := open_constr:(class _ _ _ _ _ _) in
+    unshelve evar (x:o); [typeclasses eauto|]; assert_not_dup x))
+  || idtac.
+
+Ltac fold_Category cC :=
+  match type of cC with Category ?C =>
+  let catify f := constr:(@f C cC) in
+  let base_fn f := (let raw := catify f in
+    let t := eval cbn in raw in constr:(t)) in
+  let cat_fold f :=
+    (let base := base_fn @f in 
+    let catted := catify @f in
+    change base with catted in *) in
+  try cat_fold @morphism; (* has issues, e.g., with ZX - 
+    might be fixable, but likely not necessary*)
+  cat_fold @compose;
+  cat_fold @c_identity;
+  let cid := base_fn @c_identity in
+    (repeat progress (
+      let H := fresh in let x := fresh in evar (x : C); 
+        let x' := eval unfold x in x in 
+        let cidx := eval cbn in (cid x') in 
+        pose (eq_refl : cidx = cC.(c_identity) x') as H;
+        erewrite H; clear x H));
+  let eqbase := base_fn @equiv in
+  let eqcat := catify @equiv in
+  change eqbase with eqcat; (* I think this is a no-op *)
+  repeat (progress match goal with
+  |- eqbase ?A ?B ?f ?g 
+    => change (eqbase A B f g) with (eqcat A B f g)
+  end);
+  try let H' := fresh in 
+    enough (H':(@equiv _ _ _ _ _ _)) by (eapply H')
+  end.
+
+Ltac fold_all_categories :=
+  saturate_instances Category;
+  repeat match goal with
+  | x := ?cC : Category ?C |- _ => (* idtac x ":=" cC ": Category" C ; *) 
+      fold_Category cC; subst x
+  (* | x : Category ?C |- _ => idtac x; fold_Category x; subst x *)
+  end.
+
+Ltac fold_MonoidalCategory mC :=
+  match type of mC with @MonoidalCategory ?C ?cC =>
+  let catify f := constr:(@f C cC) in
+  let mcatify f := constr:(@f C cC mC) in
+  let base_fn f := 
+    (let t := eval cbn in f in constr:(t)) in
+  let cbase_fn f := (let raw := catify f in
+    let t := eval cbn in raw in constr:(t)) in
+  let mbase_fn f := (let raw := mcatify f in
+    let t := eval cbn in raw in constr:(t)) in
+  let f_fold f :=
+    (let base := base_fn @f in 
+     change base with f) in
+  let cat_fold f :=
+    (let base := cbase_fn @f in 
+    let catted := catify @f in
+    change base with catted in *) in
+  let mcat_fold f :=
+    (let base := mbase_fn @f in 
+    let catted := mcatify @f in
+    change base with catted in *) in
+  let tens := mbase_fn @tensor in
+    let ob_base := base_fn (@obj2_map C C C cC cC cC tens) in
+      change ob_base with mC.(tensor).(obj2_map);
+    let mor_base := base_fn (@morphism2_map C C C cC cC cC tens) in
+      change mor_base with (@morphism2_map C C C cC cC cC mC.(tensor))
+      (* (@tensor C cC mC).(@morphism2_map C C C cC cC cC) *);
+  mcat_fold @I;
+  let lunit := mbase_fn @left_unitor in
+    repeat progress (
+      let H := fresh in let x := fresh in 
+      evar (x : C);  (* TODO: Test this - last I tried it was uncooperative *)
+      let x' := eval unfold x in x in 
+      let lunitx := eval cbn in ((lunit x').(forward)) in
+      pose (eq_refl : lunitx = (mC.(left_unitor) (A:=x')).(forward)) as H;
+      erewrite H; clear x H);
+  let runit := mbase_fn @right_unitor in 
+    repeat progress (
+      let H := fresh in let x := fresh in 
+      evar (x : C);  (* TODO: Test this - last I tried it was uncooperative *)
+      let x' := eval unfold x in x in 
+      let runitx := eval cbn in ((runit x').(forward)) in
+      pose (eq_refl : runitx = (mC.(right_unitor) (A:=x')).(forward)) as H;
+      erewrite H; clear x H)
+  end.
+
+Ltac fold_all_monoidal_categories :=
+  saturate_instances MonoidalCategory;
+  repeat match goal with
+  | x := ?mC : MonoidalCategory ?C |- _ => (* idtac x ":=" cC ": Category" C ; *) 
+      fold_MonoidalCategory mC; subst x
+  (* | x : Category ?C |- _ => idtac x; fold_Category x; subst x *)
+  end.
+
+Ltac fold_BraidedMonoidalCategory bC :=
+  match type of bC with @BraidedMonoidalCategory ?C ?cC ?mC =>
+  let catify f := constr:(@f C cC) in
+  let mcatify f := constr:(@f C cC mC) in
+  let bcatify f := constr:(@f C cC mC bC) in
+  let base_fn f := 
+    (let t := eval cbn in f in constr:(t)) in
+  let cbase_fn f := (let raw := catify f in
+    let t := eval cbn in raw in constr:(t)) in
+  let mbase_fn f := (let raw := mcatify f in
+    let t := eval cbn in raw in constr:(t)) in
+  let bbase_fn f := (let raw := bcatify f in
+    let t := eval cbn in raw in constr:(t)) in
+  let f_fold f :=
+    (let base := base_fn @f in 
+     change base with f) in
+  let cat_fold f :=
+    (let base := cbase_fn @f in 
+    let catted := catify @f in
+    change base with catted in *) in
+  let mcat_fold f :=
+    (let base := mbase_fn @f in 
+    let catted := mcatify @f in
+    change base with catted in *) in
+  let bcat_fold f :=
+    (let base := bbase_fn @f in 
+    let catted := bcatify @f in
+    change base with catted in *) in
+  let braid := bbase_fn @braiding in
+    let braidbase := constr:(ltac:(first [exact (ltac:(eval unfold braid in braid)) | exact braid])) in
+    let braidforw := eval cbn in 
+      (fun A B => (braidbase.(component2_iso) A B).(forward)) in
+    repeat progress (let H := fresh in let y := fresh in let x := fresh in
+      evar (y : C); evar (x : C); 
+      let x' := eval unfold x in x in let y' := eval unfold y in y in
+      let braidforwxy := eval cbn in (braidforw x' y') in
+      pose (eq_refl : braidforwxy = 
+        (bC.(braiding).(component2_iso) x' y').(forward)) as H;
+      erewrite H; clear x y H);
+    
+    let braidrev := eval cbn in
+      (fun A B => (braidbase.(component2_iso) A B).(reverse)) in
+    repeat progress (let H := fresh in let y := fresh in let x := fresh in
+      evar (y : C); evar (x : C); 
+      let x' := eval unfold x in x in let y' := eval unfold y in y in
+      let braidrevxy := eval cbn in (braidrev x' y') in
+      pose (eq_refl : braidrevxy = 
+        (bC.(braiding).(component2_iso) x' y').(reverse)) as H;
+      erewrite H; clear x y H)
+  end.
+
+Ltac fold_all_braided_monoidal_categories :=
+  saturate_instances BraidedMonoidalCategory;
+  repeat match goal with
+  | x := ?bC : BraidedMonoidalCategory ?C |- _ => 
+      fold_BraidedMonoidalCategory bC; subst x
+  end.
+
+Ltac fold_CompactClosedCategory ccC :=
+  match type of ccC with @CompactClosedCategory ?C ?cC ?mC ?bC ?sC =>
+  let catify f := constr:(@f C cC) in
+  let mcatify f := constr:(@f C cC mC) in
+  let bcatify f := constr:(@f C cC mC bC) in
+  let cccatify f := constr:(@f C cC mC bC sC ccC) in
+  let base_fn f := 
+    (let t := eval cbn in f in constr:(t)) in
+  let cbase_fn f := (let raw := catify f in
+    let t := eval cbn in raw in constr:(t)) in
+  let mbase_fn f := (let raw := mcatify f in
+    let t := eval cbn in raw in constr:(t)) in
+  let bbase_fn f := (let raw := bcatify f in
+    let t := eval cbn in raw in constr:(t)) in
+  let ccbase_fn f := (let raw := cccatify f in
+    let t := eval cbn in raw in constr:(t)) in
+  let f_fold f :=
+    (let base := base_fn @f in 
+     change base with f) in
+  let cat_fold f :=
+    (let base := cbase_fn @f in 
+    let catted := catify @f in
+    change base with catted in *) in
+  let mcat_fold f :=
+    (let base := mbase_fn @f in 
+    let catted := mcatify @f in
+    change base with catted in *) in
+  let bcat_fold f :=
+    (let base := bbase_fn @f in 
+    let catted := bcatify @f in
+    change base with catted in *) in
+  let cccat_fold f :=
+    (let base := ccbase_fn @f in 
+    let catted := cccatify @f in
+    change base with catted in *) in
+  
+  let dua := ccbase_fn @dual in
+    first [
+      (unify dua (@id C) (*; idtac "would loop" *) )
+      | (
+    repeat progress (
+      let H := fresh in let x := fresh in 
+        evar (x : C);  (* TODO: Test this - last I tried it was uncooperative *)
+        let x' := eval unfold x in x in 
+        let duax := eval cbn in (dua x') in
+        pose (eq_refl : duax = ccC.(dual) x') as H;
+        erewrite H; clear x H))];
+  
+  cccat_fold @unit;
+  cccat_fold @counit;
+
+  let uni := ccbase_fn @unit in
+    repeat progress (let H := fresh in let x := fresh in
+      evar (x : C); 
+      let x' := eval unfold x in x in 
+      let unix := eval cbn in (uni x') in
+      pose (eq_refl : unix = 
+        ccC.(unit) (A:=x')) as H;
+      erewrite H; clear x H);
+  
+  let couni := ccbase_fn @counit in
+    repeat progress (let H := fresh in let x := fresh in
+      evar (x : C); 
+      let x' := eval unfold x in x in 
+      let counix := eval cbn in (couni x') in
+      pose (eq_refl : counix = 
+        ccC.(counit) (A:=x')) as H;
+      erewrite H; clear x H)
+  end.
+
+Ltac fold_all_compact_closed_categories :=
+  saturate_instances CompactClosedCategory;
+  repeat match goal with
+  | x := ?ccC : CompactClosedCategory ?C |- _ => 
+      fold_CompactClosedCategory ccC; subst x
+  end.
+
+
+Ltac fold_DaggerCategory dC :=
+  match type of dC with @DaggerCategory ?C ?cC =>
+  let catify f := constr:(@f C cC) in
+  let dcatify f := constr:(@f C cC dC) in
+  let base_fn f := 
+    (let t := eval cbn in f in constr:(t)) in
+  let cbase_fn f := (let raw := catify f in
+    let t := eval cbn in raw in constr:(t)) in
+  let dbase_fn f := (let raw := dcatify f in
+    let t := eval cbn in raw in constr:(t)) in
+  let f_fold f :=
+    (let base := base_fn @f in 
+     change base with f) in
+  let cat_fold f :=
+    (let base := cbase_fn @f in 
+    let catted := catify @f in
+    change base with catted in *) in
+  let dcat_fold f :=
+    (let base := dbase_fn @f in 
+    let catted := dcatify @f in
+    change base with catted in *) in
+  
+  dcat_fold @adjoint;
+
+  let adj := dbase_fn @adjoint in
+    repeat progress (let H := fresh in 
+    let x := fresh in let y := fresh in
+      evar (x : C); evar (y : C);
+      let x' := eval unfold x in x in 
+      let y' := eval unfold y in y in 
+      let adjxy := eval cbn in (adj x' y') in
+      pose (eq_refl : adjxy = 
+        dC.(adjoint) (A:=x') (B:=y')) as H;
+      erewrite H; clear x y H)
+  end.
+
+Ltac fold_all_dagger_categories :=
+  saturate_instances DaggerCategory;
+  repeat match goal with
+  | x := ?dC : DaggerCategory ?C |- _ => 
+      fold_DaggerCategory dC; subst x
+  end.
+
+Ltac to_Cat :=
+  fold_all_categories; fold_all_monoidal_categories;
+  fold_all_braided_monoidal_categories; 
+  fold_all_compact_closed_categories;
+  fold_all_dagger_categories.
+
+
+
+(* Section on Fenceposting *)
+
+Ltac tensor_free f :=
+  try match f with
+  | context[@morphism2_map _ _ _ _ _ _ (@tensor _ _ _)] => fail 2
+  end.
+
+Ltac compose_free f :=
+  try match f with
+  | context[@compose _ _ _ _] => fail 2
+  end.
+
+Ltac pseudo_const f :=
+  tensor_free f; compose_free f.
+
+(* 
+TODO: I used to have explicit patterns, like this, for compose and tensor.
+  In testing, I found no difference, but this warrants consideration.
+Ltac tensor_only f :=
+  first [
+    pseudo_const f
+  | lazymatch f with 
+    | @morphism2_map _ _ _ _ _ _ (@tensor _ _ _) _ _ _ _ ?f ?g =>
+        tensor_only f; tensor_only g
+    end]. *)
+
+Ltac tensor_only f :=
+  first [
+    pseudo_const f
+  | lazymatch f with (* TODO: Does lazy matter here? Pretty sure it doesn't hurt, but idk if it'd ever match more than once anyways*)
+    | (?g ⊗ ?h)%Cat => tensor_only g; tensor_only h
+    end].
+
+Ltac compose_only f :=
+  first [pseudo_const f
+  | lazymatch f with (* TODO: Does lazy matter here? Pretty sure it doesn't hurt, but idk if it'd ever match more than once anyways*)
+    | (?g ∘ ?h)%Cat =>  (* old: @compose _ _ _ _ _ ?g ?h *)
+        compose_only g; compose_only h
+    end].
+
+(* Old:
+| @compose _ _ _ _ _ ?g ?h => tensor_only g; is_weak_fenced h
+| @morphism2_map _ _ _ _ _ _ (@tensor _ _ _) _ _ _ _ ?g ?h =>
+    tensor_only g; tensor_only h
+| _ => pseudo_const f
+  *)
+Ltac is_weak_fenced f :=
+  lazymatch f with
+  | (?g ∘ ?h)%Cat => tensor_only g; is_weak_fenced h
+  | (?g ⊗ ?h)%Cat =>
+      tensor_only g; tensor_only h
+  | _ => pseudo_const f
+  end.
+
+(* (Semi-Informal) Specification: 
+  Inductive is_weak_fence f :=
+  | const : tensor_only f 
+      -> is_weak_fence f
+  | comp g h : tensor_only g -> is_weak_fence h
+     -> is_weak_fence (g ∘ h).
+*)
+(* NOTE: This old partial implementation took a very step-like approach. I'd
+   rather progress in big stes (i.e. strongly recurse) *)
+Ltac weak_fencepost_form_debug_old f :=
+  let rec weak_fencepost_form f :=
+  match f with
+  | (?g ∘ ?h)%Cat => 
+      let _ := match goal with _ => tensor_only g end in (* test for tensor-only while returning constr *)
+      let _ := match goal with _ => idtac "left composite" g "is tensor-only" end in
+      let Nh := weak_fencepost_form h in 
+      (* let _ := match goal with _ => idtac h "normalizes to" Nh end in *)
+      constr:((g ∘ Nh)%Cat)
+  | (?g ∘ ?h)%Cat => 
+    match g with 
+    | (?g' ∘ ?h')%Cat => 
+      (* We _can_ do this, but we can also just recurse:
+      let _ := tensor_only g' in 
+      let _ := match goal with _ => idtac "associating as" g' "is tensor-only" end in
+      let Ng'h := weak_fencepost_form (g' ∘ h) in *)
+      (* Ditto for this... 
+      let _ := match goal with _ => idtac "associating to " g' "∘ (" h' "∘" h ")" end in
+      let Ng' := weak_fencepost_form g' in
+      let Nh'h := weak_fencepost_form (h' ∘ h) in
+      let Nf := weak_fencepost_form (Ng' ∘ Nh'h) in
+      constr:(Nf)*)
+      let _ := match goal with _ => idtac "associating to " g' "∘ (" h' "∘" h ")" end in
+      let Nf := weak_fencepost_form (g' ∘ (h' ∘ h))%Cat in
+      constr:(Nf)
+    | _ => 
+      let _ := match goal with _ => 
+        idtac "WARNING:" g "is not tensor-only or a composition" end in
+        let Nh := weak_fencepost_form h in
+        constr:((g ∘ h)%Cat)
+    end
+  | _ => let _ := match goal with _ => tensor_only f end in 
+    let _ := match goal with _ => 
+      idtac f "is tensor-only" end in
+    constr:(f)
+  | _ => 
+      let _ := match goal with _ => 
+        idtac "INFO:" f "is const or unsupported" end in
+      constr:(f)
+  end
+  in weak_fencepost_form f.
+
+
+
+Ltac right_associate f := 
+  match f with 
+  | ((?g ∘ ?h) ∘ ?i)%Cat => right_associate (g ∘ (h ∘ i))%Cat
+  | (?g ∘ ?h)%Cat => (* g shouldn't be a composition *)
+      let RAh := right_associate h in
+        constr:((g ∘ RAh)%Cat)
+  | _ => constr:(f)
+  end.
+
+(* TODO: Test this! *)
+Ltac left_associate f := 
+  match f with 
+  | (?g ∘ (?h ∘ ?i))%Cat => left_associate ((g ∘ h) ∘ i)%Cat
+  | (?g ∘ ?h)%Cat => (* h shouldn't be a composition *)
+      let LAg := left_associate g in
+        constr:((LAg ∘ h)%Cat)
+  | _ => constr:(f)
+  end.
+
+Ltac merge_stacked_composition_old g h := 
+  (* g ⊗ h = (g0 ∘ (g1 ∘ ...)) ⊗ (h0 ∘ (h1 ∘ ...)) 
+     ===> (g0 ⊗ h0) ∘ (g1 ⊗ h1) ∘ ...
+     with id_ inserted as needed. *)
+  (* In gallina: 
+  match g, h with
+  | ?g0 ∘ ?g1, ?h0 ∘ ?h1 => 
+      let rest := merge_stacked_composition g1 h1 in
+      constr:(g0 ⊗ h0 ∘ rest)
+  | ?g0 ∘ ?g1, ?h0 => 
+      match type of h0 with ?A ~> ?B =>
+        let rest := merge_stacked_composition g1 (id_ B) in
+        constr:(g0 ⊗ h0 ∘ rest)
+      end
+  | ?g0, ?h0 ∘ ?h1 => 
+    match type of g0 with ?A ~> ?B =>
+      let rest := merge_stacked_composition (id_ B) h1 in
+      constr:(g0 ⊗ h0 ∘ rest)
+    end
+  | _, _ => constr:(g ⊗ h)
+  end.*)
+  (* With ltac restrictions, *)
+  let rec merge_stacked_composition g h :=
+  match g with
+  | (?g0 ∘ ?g1)%Cat => 
+    match h with 
+    | (?h0 ∘ ?h1)%Cat =>
+        let rest := merge_stacked_composition g1 h1 in
+        constr:((g0 ⊗ h0 ∘ rest)%Cat)
+    | _ => 
+        match type of h with (?A ~> ?B)%Cat =>
+          let rest := merge_stacked_composition g1 (id_ B) in
+          constr:((g0 ⊗ h ∘ rest)%Cat)
+        end
+    end
+  | _ => 
+    match h with 
+    | (?h0 ∘ ?h1)%Cat =>
+        match type of g with (?A ~> ?B)%Cat =>
+          let rest := merge_stacked_composition (id_ B) h1 in
+          constr:((g ⊗ h0 ∘ rest)%Cat)
+        end
+    | _ => 
+        constr:((g ⊗ h)%Cat)
+    end
+  end
+  in merge_stacked_composition g h. 
+
+
+
+Ltac merge_stacked_composition_debug gh := 
+  let rec merge_stacked_composition gh :=
+  match type of gh with @morphism ?C ?cC _ _ =>
+  match gh with
+    @morphism2_map C _ _ cC _ _ (@tensor C cC ?mC) ?gA ?gB ?hA ?hB ?g ?h =>
+  lazymatch g with
+  | (?g0 ∘ ?g1)%Cat => 
+    let _ := match goal with _ => 
+      idtac "found decomp of first as" g0 "∘" g1 end in
+    lazymatch h with 
+    | (?h0 ∘ ?h1)%Cat =>
+        let _ := match goal with _ => 
+          idtac "found decomp of second as" h0 "∘" h1 end in
+        let rest := merge_stacked_composition (mC.(tensor) @@ g1, h1) in
+        let _ := match goal with _ => 
+          idtac "remaining terms became" rest end in
+        let res := constr:(cC.(compose) (mC.(tensor) @@ g0, h0) rest) in
+        let _ := match goal with _ => 
+          idtac "    which combined to" res end in
+        constr:(res)
+    | _ => 
+        let _ := match goal with _ => 
+          idtac "found second to be atomic:" h end in
+        match type of h with @morphism _ _ ?A ?B =>
+          let _ := match goal with _ => 
+            idtac "resolved second as type" hA "~>" hB end in
+          let rest := merge_stacked_composition (mC.(tensor) @@ g1, (cC.(c_identity) hB)) in
+          let _ := match goal with _ => 
+            idtac "remaining terms became" rest end in
+          let res := constr:(cC.(compose) (mC.(tensor) @@ g0, h) rest) in
+          let _ := match goal with _ => 
+            idtac "    which combined to" res end in
+          constr:(res)
+        end
+    end
+  | _ => 
+    let _ := match goal with _ => 
+      idtac "found first to be atomic:" g end in
+    lazymatch h with 
+    | (?h0 ∘ ?h1)%Cat =>
+        let _ := match goal with _ => 
+          idtac "found decomp of second as" h0 "∘" h1 end in
+        match type of g with @morphism _ _ ?A ?B =>
+          let _ := match goal with _ => 
+            idtac "resolved second as type" gA "~>" gB end in
+          let rest := merge_stacked_composition (mC.(tensor) @@ (cC.(c_identity) gB), h1) in
+          let _ := match goal with _ => 
+            idtac "remaining terms became" rest end in
+          let res := constr:(cC.(compose) (mC.(tensor) @@ g, h0) rest) in
+          let _ := match goal with _ => 
+            idtac "    which combined to" res end in
+          constr:(res)
+        end
+    | _ => 
+        let _ := match goal with _ => 
+          idtac "found second to be atomic as well:" h end in
+        constr:(mC.(tensor) @@ g, h)
+    end
+  end
+  end end
+  in merge_stacked_composition gh. 
+
+Ltac merge_stacked_composition gh := 
+  let rec merge_stacked_composition gh :=
+  match type of gh with @morphism ?C ?cC _ _ =>
+  match gh with
+    @morphism2_map C _ _ cC _ _ (@tensor C cC ?mC) ?gA ?gB ?hA ?hB ?g ?h =>
+  lazymatch g with
+  | (?g0 ∘ ?g1)%Cat => 
+    lazymatch h with 
+    | (?h0 ∘ ?h1)%Cat =>
+        let rest := merge_stacked_composition (mC.(tensor) @@ g1, h1) in
+        constr:(cC.(compose) (mC.(tensor) @@ g0, h0) rest)
+    | _ => 
+        let rest :=
+          merge_stacked_composition 
+            (mC.(tensor) @@ g1, (cC.(c_identity) hB)) in
+        constr:(cC.(compose) (mC.(tensor) @@ g0, h) rest)
+    end
+  | _ => 
+    lazymatch h with 
+    | (?h0 ∘ ?h1)%Cat =>
+        let rest := 
+          merge_stacked_composition
+            (mC.(tensor) @@ (cC.(c_identity) gB), h1) in
+        constr:(cC.(compose) (mC.(tensor) @@ g, h0) rest)
+    | _ => 
+        constr:(mC.(tensor) @@ g, h)
+    end
+  end
+  end end
+  in merge_stacked_composition gh. 
+
+Ltac weak_fencepost_form_debug f :=
+  let rec weak_fencepost f :=
+  match f with
+  | @compose ?C ?cC _ _ _ ?g ?h => 
+      let _ := match goal with _ => 
+        idtac "splitting on ∘ into" g "and" h "..." end in
+      let Ng := weak_fencepost g in
+      let Nh := weak_fencepost h in 
+      let _ := match goal with _ => 
+        idtac "... getting" g "∘" h "into" end in
+      let res := right_associate (cC.(compose) Ng Nh) in
+      let _ := match goal with _ => 
+        idtac "    " res end in
+      constr:(res)
+  | @morphism2_map ?C _ _ ?cC _ _ (@tensor ?C ?cC ?mC) _ _ _ _ ?g ?h =>
+      let _ := match goal with _ => 
+        idtac "splitting on ⊗ into" g "and" h "..." end in
+      let Ng := weak_fencepost g in
+      let Nh := weak_fencepost h in 
+      let _ := match goal with _ => 
+        idtac "... getting" g "⊗" h "into" end in
+      let res := merge_stacked_composition (mC.(tensor) @@ Ng, Nh) in
+      let _ := match goal with _ => 
+        idtac "    " res end in
+      constr:(res)
+  | _ => 
+      let _ := match goal with _ => 
+        idtac "INFO:" f "is const or unsupported" end in
+      constr:(f)
+  end
+  in weak_fencepost f.
+
+Ltac weak_fencepost_form f :=
+  let rec weak_fencepost f :=
+  match f with
+  | @compose ?C ?cC _ _ _ ?g ?h => 
+      let Ng := weak_fencepost g in
+      let Nh := weak_fencepost h in 
+      right_associate (cC.(compose) Ng Nh)
+  | @morphism2_map ?C _ _ ?cC _ _ (@tensor ?C ?cC ?mC) _ _ _ _ ?g ?h =>
+      let Ng := weak_fencepost g in
+      let Nh := weak_fencepost h in 
+      merge_stacked_composition (mC.(tensor) @@ Ng, Nh)
+  | _ => (* f "is const or unsupported" *)
+      constr:(f)
+  end
+  in weak_fencepost f.
+
+Local Open Scope Cat_scope.
+Lemma assoc_compat_helper {C} `{Category C} {A B M N : C} :
+  forall (f : A ~> B) (g : B ~> M) (h : M ~> N) (fgh : A ~> N),
+  f ∘ (g ∘ h) ≃ fgh -> (f ∘ g) ∘ h ≃ fgh.
+Proof.
+  intros; rewrite assoc; easy.
+Qed.
+
+Lemma compose_compat_right {C} `{Category C} {A B M : C} :
+  forall (f : A ~> B) (g g' : B ~> M),
+  g ≃ g' -> f ∘ g ≃ f ∘ g'.
+Proof.
+  intros.
+  apply compose_compat; easy.
+Qed.
+
+Lemma stack_compose_distr_compat {C} `{MonoidalCategory C}
+{A B M A' B' M': C} :
+  forall (f : A ~> B) (g : B ~> M) (h : A' ~> B') (i : B' ~> M')
+  (gi : B × B' ~> M × M'),
+  g ⊗ i ≃ gi -> (f ∘ g) ⊗ (h ∘ i) ≃ f ⊗ h ∘ gi.
+Proof.
+  intros.
+  rewrite compose2_map.
+  apply compose_compat; easy.
+Qed.
+
+Lemma stack_distr_pushout_r_top_compat {C} `{MonoidalCategory C}
+  {a b m n o} : forall (f : a ~> b) (g : m ~> n) (h : n ~> o)
+  (ih : b × n ~> b × o),
+  id_ b ⊗ h ≃ ih -> f ⊗ (g ∘ h) ≃ f ⊗ g ∘ ih.
+Proof.
+  intros.
+  (* `rewrite stack_distr_pushout_r_top.` is replaced here manually 
+  to simplify dependencies *)
+  rewrite <- (right_unit (f:=f)) at 1.
+  rewrite compose2_map.
+  apply compose_compat; easy.
+Qed.
+
+Lemma stack_distr_pushout_r_bot_compat {C} `{MonoidalCategory C}
+  {a b c n o : C} : forall (f : a ~> b) (g : b ~> c) (h : n ~> o)
+  (gi : b × o ~> c × o),
+  g ⊗ id_ o ≃ gi -> (f ∘ g) ⊗ h ≃ f ⊗ h ∘ gi.
+Proof.
+  intros.
+  (* `rewrite stack_distr_pushout_r_bot.` is replaced here manually 
+  to simplify dependencies *)
+  rewrite <- (right_unit (f:=h)) at 1.
+  rewrite compose2_map.
+  apply compose_compat; easy.
+Qed.
+
+Lemma compose_compat_trans_helper {C} `{cC:Category C} {A B M : C} : forall
+  (f f' : A ~> B) (g g' : B ~> M) (fg : A ~> M),
+  f ≃ f' -> g ≃ g' -> f' ∘ g' ≃ fg -> f ∘ g ≃ fg.
+Proof.
+  intros.
+  transitivity (f' ∘ g'); [|easy].
+  apply compose_compat; easy.
+Qed.
+
+Lemma stack_compat_trans_helper {C} `{mC : MonoidalCategory C} {A A' B B' : C} : 
+  forall (f f' : A ~> A') (g g' : B ~> B') (fg : A × B ~> A' × B'),
+  f ≃ f' -> g ≃ g' -> f' ⊗ g' ≃ fg -> f ⊗ g ≃ fg.
+Proof.
+  intros.
+  transitivity (f' ⊗ g'); [|easy].
+  apply morphism2_compat; easy.
+Qed.
+
+Lemma show_equiv_stack_comp_id_bot_helper {C} `{MonoidalCategory C} 
+  {A M A' B : C} : forall (g : A ~> M) (gs : M ~> A') (gsB : M × B ~> A' × B),
+  gs ⊗ id_ B ≃ gsB -> (g ∘ gs) ⊗ id_ B ≃ g ⊗ id_ B ∘ gsB.
+Proof.
+  intros.
+  rewrite <- (right_unit (f:=id_ B)) at 1.
+  rewrite compose2_map.
+  apply compose_compat; easy.
+Qed.
+
+Lemma show_equiv_stack_comp_id_top_helper {C} `{MonoidalCategory C} 
+  {A B M B' : C} : forall (g : B ~> M) (gs : M ~> B') (Ags : A × M ~> A × B'),
+  id_ A ⊗ gs ≃ Ags -> id_ A ⊗ (g ∘ gs) ≃ id_ A ⊗ g ∘ Ags.
+Proof.
+  intros.
+  rewrite <- (right_unit (f:=id_ A)) at 1.
+  rewrite compose2_map.
+  apply compose_compat; easy.
+Qed.
+
+Lemma show_equiv_unfold_tensor_stack_helper {C} `{MonoidalCategory C} 
+  {fA fB gA gB : C} (f uf : fA ~> fB) (g ug : gA ~> gB) 
+  (ufs : fA × gA ~> fB × gA) (ugs : fB × gA ~> fB × gB) :
+  f ≃ uf -> g ≃ ug -> 
+  uf ⊗ id_ gA ≃ ufs -> id_ fB ⊗ ug ≃ ugs ->
+  f ⊗ g ≃ ufs ∘ ugs.
+Proof.
+  intros Hf Hg Huf Hug.
+  rewrite Hf, Hg.
+  rewrite <- (right_unit (f:=uf)), <- (left_unit (f:=ug)), compose2_map.
+  apply compose_compat; easy.
+Qed.
+
+Close Scope Cat_scope.
+
+
+(* Shows the goal f ≃ right_associate f by mirroring the code
+   path of right_associate with `apply`s. *)
+Ltac show_equiv_right_associate f :=
+  let rec show_equiv_right_associate f :=
+  match f with 
+  | ((?g ∘ ?h) ∘ ?i)%Cat => 
+    (* RHS is `right_associate (g ∘ (h ∘ i))` *)
+    apply assoc_compat_helper;
+    show_equiv_right_associate ((g ∘ (h ∘ i))%Cat)
+  | (?g ∘ ?h)%Cat => (* g shouldn't be a composition *)
+      (* RHS is `(g ∘ right_associate h)` *)
+      apply compose_compat_right;
+      show_equiv_right_associate h
+  | _ => 
+    (* RHS is `constr:(f)` *)
+    reflexivity
+  end
+  in show_equiv_right_associate f.
+
+(* Shows the goal f ≃ merge_stack_composition f by mirroring the 
+   code path of merge_stacked_composition with `apply`s. *)
+Ltac show_equiv_merge_stacked_composition gh := 
+  let rec show_equiv_merge_stacked_composition gh :=
+  match type of gh with @morphism ?C ?cC _ _ =>
+  match gh with
+    @morphism2_map C _ _ cC _ _ (@tensor C cC ?mC) ?gA ?gB ?hA ?hB ?g ?h =>
+  lazymatch g with
+  | (?g0 ∘ ?g1)%Cat => 
+    lazymatch h with 
+    | (?h0 ∘ ?h1)%Cat =>
+        (* RHS is g0 ⊗ h0 ∘ merge_stacked_composition (g1 ⊗ h1) *)
+        apply stack_compose_distr_compat;
+        show_equiv_merge_stacked_composition (mC.(tensor) @@ g1, h1)
+    | _ => 
+        (* RHS is g0 ⊗ h0 ∘ merge_stacked_composition (g1 ⊗ id_ hB) *)
+        apply stack_distr_pushout_r_bot_compat;
+        show_equiv_merge_stacked_composition (mC.(tensor) @@ g1, (cC.(c_identity) hB))
+    end
+  | _ => 
+    lazymatch h with 
+    | (?h0 ∘ ?h1)%Cat =>
+        (* RHS is g0 ⊗ h0 ∘ merge_stacked_composition (id_ gB ⊗ h1) *)
+        apply stack_distr_pushout_r_top_compat;
+        show_equiv_merge_stacked_composition (mC.(tensor) @@ (cC.(c_identity) gB), h1)
+    | _ => 
+        (* RHS is g ⊗ h *)
+        reflexivity
+    end
+  end
+  end end
+  in show_equiv_merge_stacked_composition gh. 
+
+(* Shows the goal f ≃ weak_fencepost_form f by mirroring the code
+   path of weak_fencepost_form with `apply`s. *)
+Ltac show_equiv_weak_fencepost_form f :=
+  let weak_fencepost := weak_fencepost_form in 
+  let rec show_equiv_weak_fencepost_form f :=
+  match f with
+  | @compose ?C ?cC _ _ _ ?g ?h => 
+      let Ng := weak_fencepost g in
+      let Nh := weak_fencepost h in 
+      let res := right_associate (cC.(compose) Ng Nh) in
+      apply (compose_compat_trans_helper (cC:=cC) g Ng h Nh res 
+        ltac:(show_equiv_weak_fencepost_form g)
+        ltac:(show_equiv_weak_fencepost_form h)
+        ltac:(show_equiv_right_associate (cC.(compose) Ng Nh)))
+  | @morphism2_map ?C _ _ ?cC _ _ (@tensor ?C ?cC ?mC) _ _ _ _ ?g ?h =>
+      let Ng := weak_fencepost g in
+      let Nh := weak_fencepost h in 
+      let res := merge_stacked_composition (mC.(tensor) @@ Ng, Nh) in
+      apply (stack_compat_trans_helper (cC:=cC) g Ng h Nh res 
+        ltac:(show_equiv_weak_fencepost_form g)
+        ltac:(show_equiv_weak_fencepost_form h)
+        ltac:(show_equiv_merge_stacked_composition (mC.(tensor) @@ Ng, Nh)))
+  | _ => (* f "is const or unsupported" *)
+      (* constr:(f) *)
+      reflexivity
+  end
+  in show_equiv_weak_fencepost_form f.
+
+(* TODO: Generalize these to fold_compose base *)
+(* If f = f0 ∘ (f1 ∘ (...)), this gives f0 ⊗ id_ B ∘ (f1 ⊗ id_ B ∘ (...))
+   in the given monoidal category mC. *)
+Ltac stack_comp_id_bot f B mC :=
+  let base g :=
+    constr:(mC.(tensor) @@ g, id_ B) in
+  let rec stack_comp h :=
+  match h with
+  | (?g ∘ ?gs)%Cat => 
+      let stg := base g in
+      let stgs := stack_comp gs in
+      constr:((stg ∘ stgs)%Cat)
+  | ?g => 
+      base h
+  end
+  in stack_comp f.
+
+(* If f = f0 ∘ (f1 ∘ (...)), this gives id_ A ⊗ f0 ∘ (id_ A ⊗ f1 ∘ (...))
+   in the given monoidal category mC. *)
+Ltac stack_comp_id_top f A mC :=
+  let base g :=
+    constr:(mC.(tensor) @@ id_ A, g) in
+  let rec stack_comp h :=
+  match h with
+  | (?g ∘ ?gs)%Cat => 
+      let stg := base g in
+      let stgs := stack_comp gs in
+      constr:((stg ∘ stgs)%Cat)
+  | ?g => 
+      base h
+  end
+  in stack_comp f.
+
+
+
+(* Given f ⊗ g ⊗ h ⊗ ..., gives f ⊗ id ⊗ ... ∘ id ⊗ g ⊗ ...
+   (this tactic allows for irregularly-associated ⊗, which 
+   that example may not suggest). *)
+Ltac unfold_tensor_stack f :=
+  let rec unfold_tensor_stack f :=
+  lazymatch f with 
+  | @morphism2_map _ _ _ _ _ _ (@tensor _ _ ?mC) ?gA ?gB ?hA ?hB ?g ?h =>
+      let ug := unfold_tensor_stack g in 
+      let uh := unfold_tensor_stack h in 
+      let sg := stack_comp_id_bot ug hA mC in
+      let sh := stack_comp_id_top uh gB mC in
+      constr:((sg ∘ sh)%Cat)
+  | _ => constr:(f)
+  end
+  in unfold_tensor_stack f.
+
+
+Ltac unfold_tensor_stack_no_id f :=
+  let rec unfold_tensor_stack f :=
+  lazymatch f with 
+    (* TODO: is this case smart to have? *)
+  | @morphism2_map _ _ _ _ _ _ (@tensor _ ?cC ?mC) 
+    ?gA ?gA ?hA ?hA (id_ ?gA)%Cat (id_ ?hA) => 
+      constr:(cC.(c_identity) (mC.(tensor) gA hA))
+  
+  | @morphism2_map _ _ _ _ _ _ (@tensor _ _ ?mC) ?gA ?gA ?hA ?hB (id_ ?gA)%Cat ?h => 
+      let uh := unfold_tensor_stack h in 
+      let sh := stack_comp_id_top uh gA mC in
+      constr:(sh)
+      
+  | @morphism2_map _ _ _ _ _ _ (@tensor _ _ ?mC) ?gA ?gB ?hA ?hA ?g (id_ ?hA)%Cat => 
+      let ug := unfold_tensor_stack g in 
+      let sg := stack_comp_id_bot ug hA mC in
+      constr:(sg)
+
+  | @morphism2_map _ _ _ _ _ _ (@tensor _ _ ?mC) ?gA ?gB ?hA ?hB ?g ?h =>
+      let ug := unfold_tensor_stack g in 
+      let uh := unfold_tensor_stack h in 
+      let sg := stack_comp_id_bot ug hA mC in
+      let sh := stack_comp_id_top uh gB mC in
+      constr:((sg ∘ sh)%Cat)
+  | _ => constr:(f)
+  end
+  in unfold_tensor_stack f.
+
+(* Returns the strong fencepost term of a weakly fenceposted term 
+   (in fact, not even requiring the term be right-associated, though
+    the resulting fencepost will be. )*)
+Ltac strong_fencepost_form_of_weak f :=
+  let rec strong_fence f :=
+  lazymatch f with
+  | (?g ∘ ?h)%Cat => 
+      let ug := strong_fence g in
+      let uh := strong_fence h in
+      right_associate (ug ∘ uh)%Cat
+  | _ => 
+      unfold_tensor_stack f
+  end
+  in strong_fence f.
+
+(* Additionally avoids taking id ⊗ id to id ⊗ id ∘ id ⊗ id and similar *)
+Ltac strong_fencepost_form_of_weak_no_id f :=
+  let rec strong_fence f :=
+  lazymatch f with
+  | (?g ∘ ?h)%Cat => 
+      let ug := strong_fence g in
+      let uh := strong_fence h in
+      right_associate (ug ∘ uh)%Cat
+  | _ => 
+      unfold_tensor_stack_no_id f
+  end
+  in strong_fence f.
+
+
+Ltac show_equiv_stack_comp_id_bot f B mC :=
+  let base g :=
+    constr:(mC.(tensor) @@ g, id_ B) in
+  let rec show_stack_comp h :=
+  match h with
+  | (?g ∘ ?gs)%Cat => 
+      (* let stg := base g in
+      let stgs := stack_comp gs in
+      constr:(stg ∘ stgs)%Cat *)
+      apply show_equiv_stack_comp_id_bot_helper;
+      show_stack_comp gs
+  | ?g => 
+      (* base h *)
+      reflexivity
+  end
+  in show_stack_comp f.
+
+Ltac show_equiv_stack_comp_id_top f A mC :=
+  let base g :=
+    constr:(mC.(tensor) @@ id_ A, g) in
+  let rec show_stack_comp h :=
+  match h with
+  | (?g ∘ ?gs)%Cat => 
+      (* let stg := base g in
+      let stgs := stack_comp gs in
+      constr:(stg ∘ stgs)%Cat *)
+      apply show_equiv_stack_comp_id_top_helper;
+      show_stack_comp gs
+  | ?g => 
+      (* base h *)
+      reflexivity
+  end
+  in show_stack_comp f.
+  
+
+Ltac show_equiv_unfold_tensor_stack f :=
+  let rec show_unfold f :=
+  lazymatch f with 
+  | @morphism2_map _ _ _ _ _ _ (@tensor _ ?cC ?mC) ?gA ?gB ?hA ?hB ?g ?h =>
+      let ug := unfold_tensor_stack g in 
+      let uh := unfold_tensor_stack h in 
+      let sg := stack_comp_id_bot ug hA mC in
+      let sh := stack_comp_id_top uh gB mC in
+      (* constr:(sg ∘ sh)%Cat *)
+      apply (show_equiv_unfold_tensor_stack_helper
+        g ug h uh sg sh
+        ltac:(show_unfold g) 
+        ltac:(show_unfold h)
+        ltac:(show_equiv_stack_comp_id_bot ug hA mC)
+        ltac:(show_equiv_stack_comp_id_top uh gB mC)
+      )
+  | _ => (* constr:(f) *)
+      reflexivity
+  end
+  in show_unfold f.
+
+Ltac show_equiv_unfold_tensor_stack_no_id f :=
+  let unfold_tensor_stack := unfold_tensor_stack_no_id in
+  let rec show_unfold f :=
+  lazymatch f with 
+    (* TODO: is this case smart to have? *)
+  | @morphism2_map _ _ _ _ _ _ (@tensor _ _ ?mC) 
+    ?gA ?gA ?hA ?hA (id_ ?gA)%Cat (id_ ?hA) => 
+      (* constr:(cC.(c_identity) (mC.(tensor) gA hA)) *)
+      apply (mC.(tensor).(id2_map) (A1:=gA) (A2:=hA))
+  
+  | @morphism2_map _ _ _ _ _ _ (@tensor _ ?cC ?mC) ?gA ?gA ?hA ?hB (id_ ?gA)%Cat ?h => 
+      let uh := unfold_tensor_stack h in 
+      let sh := stack_comp_id_top uh gA mC in   (* constr:(sh) *)
+      apply (stack_compat_trans_helper
+        (cC.(c_identity) gA) (cC.(c_identity) gA) h uh sh
+        ltac:(reflexivity) ltac:(show_unfold h)
+        ltac:(show_equiv_stack_comp_id_top h gA mC))
+      
+  | @morphism2_map _ _ _ _ _ _ (@tensor _ ?cC ?mC) ?gA ?gB ?hA ?hA ?g (id_ ?hA)%Cat => 
+      let ug := unfold_tensor_stack g in 
+      let sg := stack_comp_id_bot ug hA mC in   (* constr:(sg) *)
+      apply (stack_compat_trans_helper
+        g ug (cC.(c_identity) hA) (cC.(c_identity) hA) sg
+        ltac:(show_unfold g) ltac:(reflexivity)
+        ltac:(show_equiv_stack_comp_id_bot g hA mC))
+
+  | @morphism2_map _ _ _ _ _ _ (@tensor _ _ ?mC) ?gA ?gB ?hA ?hB ?g ?h =>
+      let ug := unfold_tensor_stack g in 
+      let uh := unfold_tensor_stack h in 
+      let sg := stack_comp_id_bot ug hA mC in
+      let sh := stack_comp_id_top uh gB mC in   (* constr:((sg ∘ sh)%Cat) *)
+      apply (show_equiv_unfold_tensor_stack_helper
+        g ug h uh sg sh
+        ltac:(show_unfold g) 
+        ltac:(show_unfold h)
+        ltac:(show_equiv_stack_comp_id_bot ug hA mC)
+        ltac:(show_equiv_stack_comp_id_top uh gB mC)
+      )
+  | _ => (* constr:(f) *)
+      reflexivity
+  end
+  in show_unfold f.
+
+Ltac show_equiv_unfold_tensor_stack_no_id_debug f :=
+  let unfold_tensor_stack := unfold_tensor_stack_no_id in 
+  let rec show_unfold f :=
+  lazymatch f with 
+    (* TODO: is this case smart to have? *)
+  | @morphism2_map _ _ _ _ _ _ (@tensor _ _ ?mC) ?gA _ ?hA _ (id_ ?gA)%Cat (id_ ?hA) => 
+      idtac "id id case:"; print_state;
+      (* constr:(cC.(c_identity) (mC.(tensor) gA hA)) *)
+      apply (mC.(tensor).(id2_map) (A1:=gA) (A2:=hA))
+  
+  | @morphism2_map _ _ _ _ _ _ (@tensor _ ?cC ?mC) ?gA ?gA ?hA ?hB (id_ ?gA)%Cat ?h => 
+      let uh := unfold_tensor_stack h in 
+      let sh := stack_comp_id_top uh gA mC in   (* constr:(sh) *)
+      idtac "left id case:"; print_state;
+      apply (stack_compat_trans_helper
+        (cC.(c_identity) gA) (cC.(c_identity) gA) h uh sh
+        ltac:(reflexivity) ltac:(show_unfold h)
+        ltac:(show_equiv_stack_comp_id_top h gA mC))
+      
+  | @morphism2_map _ _ _ _ _ _ (@tensor _ ?cC ?mC) ?gA ?gB ?hA ?hA ?g (id_ ?hA)%Cat => 
+      let ug := unfold_tensor_stack g in 
+      let sg := stack_comp_id_bot ug hA mC in   (* constr:(sg) *)
+      idtac "right id case:"; print_state;
+      apply (stack_compat_trans_helper
+        g ug (cC.(c_identity) hA) (cC.(c_identity) hA) sg
+        ltac:(show_unfold g) ltac:(reflexivity)
+        ltac:(show_equiv_stack_comp_id_bot g hA mC))
+
+  | @morphism2_map _ _ _ _ _ _ (@tensor _ _ ?mC) ?gA ?gB ?hA ?hB ?g ?h =>
+      let ug := unfold_tensor_stack g in let uh := unfold_tensor_stack h in 
+      let sg := stack_comp_id_bot ug hA mC in
+      let sh := stack_comp_id_top uh gB mC in
+      idtac "true compose case:"; print_state;
+      apply (show_equiv_unfold_tensor_stack_helper
+        g ug h uh sg sh   ltac:(show_unfold g) ltac:(show_unfold h)
+        ltac:(show_equiv_stack_comp_id_bot ug hA mC)
+        ltac:(show_equiv_stack_comp_id_top uh gB mC)
+      )
+  | _ => (* constr:(f) *) reflexivity
+  end
+  in show_unfold f.
+
+
+Ltac show_equiv_strong_fencepost_form_of_weak f :=
+  let strong_fence := strong_fencepost_form_of_weak in
+  let rec show_strong_fence f :=
+  lazymatch f with
+  | (?g ∘ ?h)%Cat => 
+      let ug := strong_fence g in
+      let uh := strong_fence h in
+      let rassoc := right_associate (ug ∘ uh)%Cat in
+      (* right_associate (ug ∘ uh)%Cat *)
+      apply (compose_compat_trans_helper
+        g ug  h uh rassoc
+        ltac:(show_strong_fence g)
+        ltac:(show_strong_fence h)
+        ltac:(show_equiv_right_associate (ug ∘ uh)%Cat)
+      )
+  | _ => 
+      (* unfold_tensor_stack f *)
+      show_equiv_unfold_tensor_stack f
+  end
+  in show_strong_fence f.
+
+
+Ltac show_equiv_strong_fencepost_form_of_weak_no_id f :=
+  let strong_fence := strong_fencepost_form_of_weak_no_id in
+  let rec show_strong_fence f :=
+  lazymatch f with
+  | (?g ∘ ?h)%Cat => 
+      let ug := strong_fence g in
+      let uh := strong_fence h in
+      let rassoc := right_associate (ug ∘ uh)%Cat in
+      (* right_associate (ug ∘ uh)%Cat *)
+      apply (compose_compat_trans_helper
+        g ug  h uh rassoc
+        ltac:(show_strong_fence g)
+        ltac:(show_strong_fence h)
+        ltac:(show_equiv_right_associate (ug ∘ uh)%Cat)
+      )
+  | _ => 
+      (* unfold_tensor_stack f *)
+      show_equiv_unfold_tensor_stack_no_id f
+  end
+  in show_strong_fence f.
+
+Ltac show_equiv_strong_fencepost_form_of_weak_no_id_debug f :=
+  let strong_fence := strong_fencepost_form_of_weak_no_id in
+  let rec show_strong_fence f :=
+  lazymatch f with
+  | (?g ∘ ?h)%Cat => 
+      let ug := strong_fence g in
+      let uh := strong_fence h in
+      let rassoc := right_associate (ug ∘ uh)%Cat in
+      (* right_associate (ug ∘ uh)%Cat *)
+      apply (compose_compat_trans_helper
+        g ug  h uh rassoc
+        ltac:(show_strong_fence g)
+        ltac:(show_strong_fence h)
+        ltac:(show_equiv_right_associate (ug ∘ uh)%Cat)
+      )
+  | _ => 
+      (* unfold_tensor_stack f *)
+      show_equiv_unfold_tensor_stack_no_id_debug f
+  end
+  in show_strong_fence f.
+
+Ltac weak_fencepost f :=
+  let wf := weak_fencepost_form f in
+  let H := fresh in 
+  assert (H: (f ≃ wf)%Cat) by (show_equiv_weak_fencepost_form f);
+  setoid_rewrite H;
+  clear H.
+
+Ltac strong_fencepost f :=
+  let wf := weak_fencepost_form f in
+  let sf := strong_fencepost_form_of_weak wf in
+  let H := fresh in 
+  assert (H: (f ≃ sf)%Cat) by (
+    transitivity wf;
+    [ show_equiv_weak_fencepost_form f 
+    | show_equiv_strong_fencepost_form_of_weak wf]);
+  setoid_rewrite H;
+  clear H.
+
+Ltac strong_fencepost_no_id f :=
+  let wf := weak_fencepost_form f in
+  let sf := strong_fencepost_form_of_weak_no_id wf in
+  let H := fresh in 
+  assert (H: (f ≃ sf)%Cat) by (
+    transitivity wf;
+    [ show_equiv_weak_fencepost_form f 
+    | show_equiv_strong_fencepost_form_of_weak_no_id wf]);
+  setoid_rewrite H;
+  clear H.
+
+Ltac strong_fencepost_no_id_debug f :=
+  let wf := weak_fencepost_form f in
+  let sf := strong_fencepost_form_of_weak_no_id wf in
+  let H := fresh in 
+  assert (H: (f ≃ sf)%Cat) by (
+    transitivity wf;
+    [ show_equiv_weak_fencepost_form f 
+    | show_equiv_strong_fencepost_form_of_weak_no_id_debug wf]);
+  setoid_rewrite H;
+  clear H.
+
+Section Testing.
+Local Open Scope Cat_scope.
+Variables (C : Type) (cC cC' cC'' : Category C)
+  (mC0   mC1   : @MonoidalCategory C cC)
+  (mC0'  mC1'  : @MonoidalCategory C cC')
+  (mC0'' mC1'' : @MonoidalCategory C cC'')
+  (A B M N : C)
+  (f   f0   : cC.(morphism)   A B) 
+  (g   g0   : cC.(morphism)   B M) 
+  (h   h0   : cC.(morphism)   A M)
+  (i   i0   : cC.(morphism)   M N)
+  (j   j0   : cC.(morphism)   B M)
+  (k   k0   : cC.(morphism)   A M)
+  (f'  f0'  : cC'.(morphism)  A B) 
+  (g'  g0'  : cC'.(morphism)  B M) 
+  (h'  h0'  : cC'.(morphism)  A M)
+  (i'  i0'  : cC'.(morphism)  M N)
+  (j'  j0'  : cC'.(morphism)  B M)
+  (k'  k0'  : cC'.(morphism)  A M)
+  (f'' f0'' : cC''.(morphism) A B) 
+  (g'' g0'' : cC''.(morphism) B M) 
+  (h'' h0'' : cC''.(morphism) A M)
+  (i'' i0'' : cC''.(morphism) M N)
+  (j'' j0'' : cC''.(morphism) B M)
+  (k'' k0'' : cC''.(morphism) A M).
+(* Goal True. *)
+
+Existing Instance cC.
+Existing Instance cC'.
+Existing Instance cC''.
+Existing Instance mC0.   Existing Instance mC1.
+Existing Instance mC0'.  Existing Instance mC1'.
+Existing Instance mC0''. Existing Instance mC1''.
+
+Lemma test_weak_fencepost : forall {C : Type}
+  `{Cat : Category C} `{MonCat : MonoidalCategory C}
+  {a b m n o} (f : a ~> b) (g : m ~> n) (h : n ~> o),
+  f ⊗ (g ∘ h) ≃ f ⊗ g ∘ (id_ b ⊗ h).
+Proof.
+  intros.
+  match goal with
+  |- ?T ≃ _ => weak_fencepost T
+  end.
+  easy.
+Qed.
+
+Lemma test_strong_fencepost : forall {C : Type}
+  `{Cat : Category C} `{MonCat : MonoidalCategory C}
+  {a b m n o} (f : a ~> b) (g : m ~> n) (h : n ~> o),
+  f ⊗ (g ∘ h) ≃ f ⊗ g ∘ (id_ b ⊗ h).
+Proof.
+  intros.
+  match goal with
+  |- ?T ≃ ?T' => strong_fencepost T; strong_fencepost T'
+  end.
+  easy.
+Qed.
+
+Lemma test_strong_fencepost_no_id_1 : forall {C : Type}
+  `{Cat : Category C} `{MonCat : MonoidalCategory C}
+  {a b m n o} (f : a ~> b) (g : m ~> n) (h : n ~> o),
+  f ⊗ (g ∘ h) ≃ f ⊗ g ∘ (id_ b ⊗ h).
+Proof.
+  intros.
+  match goal with
+  |- ?T ≃ ?T' => strong_fencepost_no_id T; strong_fencepost_no_id T'
+  end.
+  easy.
+Qed.
+
+(* Lemma test_strong_fencepost_no_id_2 : forall {C : Type}
+  `{Cat : Category C} `{MonCat : MonoidalCategory C}
+  {a b m n o} (f : a ~> b) (g : m ~> n) (h : n ~> o),
+  f ⊗ (g ∘ h ∘ id_ _) ⊗ (id_ a ⊗ id_ b) ≃ 
+  f ⊗ g ⊗ (id_ a ⊗ id_ b) ∘ ((id_ b ⊗ h) ⊗ (id_ a ⊗ id_ b)).
+Proof.
+  intros.
+  match goal with
+  |- ?T ≃ ?T' => strong_fencepost_no_id_debug T
+  (* ; strong_fencepost_no_id T' *)
+  end.
+  easy.
+Qed. *)
+
+Goal True.
+
+
+Local Ltac test_show_unfold_no_id_of_wf f :=
+  let wf := weak_fencepost_form f in
+  let sf := unfold_tensor_stack_no_id wf in
+  (* idtac sf; *)
+  let H := fresh in 
+  assert (H : wf ≃ sf) by (show_equiv_unfold_tensor_stack_no_id wf);
+  clear H.
+
+test_show_unfold_no_id_of_wf (f ⊗ (f0 ∘ g0 ∘ id_ _) ⊗ (id_ A ⊗ id_ B)).
+
+
+
+
+Local Ltac test_show_unfold_no_id f :=
+  let sf := unfold_tensor_stack_no_id f in
+  (* idtac sf; *)
+  let H := fresh in 
+  assert (H : f ≃ sf) by (show_equiv_unfold_tensor_stack_no_id f; print_state);
+  clear H.
+
+test_show_unfold_no_id ((id_ B ⊗ id_ M ⊗ id_ (A × B))).
+test_show_unfold_no_id (f ⊗ (f0 ∘ g0 ∘ id_ _) ⊗ (id_ A ⊗ id_ B)).
+test_show_unfold_no_id (f ⊗ f0 ⊗ (id_ A ⊗ id_ B)).
+test_show_unfold_no_id (id_ B ⊗ g0 ⊗ id_ (A × B)).
+
+
+
+Local Ltac test_show_st_of_wk f :=
+  let wf := weak_fencepost_form f in
+  let sf := strong_fencepost_form_of_weak wf in
+  let H := fresh in 
+  assert (H: wf ≃ sf) by (show_equiv_strong_fencepost_form_of_weak wf);
+  clear H.
+
+test_show_st_of_wk f.
+test_show_st_of_wk (f ∘ g).
+test_show_st_of_wk (f ⊗ g).
+
+test_show_st_of_wk (f ⊗ (f ∘ g)).
+test_show_st_of_wk ((f ⊗ ((f ∘ g) ⊗ (f0 ∘ g0)))).
+
+
+
+
+Local Ltac test_show_unfold f :=
+  let sf := unfold_tensor_stack f in
+  let H := fresh in 
+  assert (H : f ≃ sf) by (show_equiv_unfold_tensor_stack f);
+  clear H.
+
+test_show_unfold f.
+test_show_unfold (f ∘ g).
+test_show_unfold (f ⊗ g).
+
+test_show_unfold ((f ⊗ (f ∘ g) ⊗ (f0 ∘ g0))).
+
+test_show_unfold ((f ∘ g) ⊗ (f0 ∘ g0)).
+test_show_unfold ((f ∘ g) ⊗ (f0)).
+test_show_unfold ((f ⊗ ((f ∘ g) ⊗ (f0 ∘ g0)))).
+
+
+
+Local Ltac test_show_st_bot f B mC :=
+  let sf := stack_comp_id_bot f B mC in
+  let H := fresh in 
+  assert (H : f ⊗ id_ B ≃ sf) by (show_equiv_stack_comp_id_bot f B mC);
+  clear H.
+
+Local Ltac test_show_st_top f A mC :=
+  let sf := stack_comp_id_top f A mC in
+  let H := fresh in 
+  assert (H : id_ A ⊗ f ≃ sf) by (show_equiv_stack_comp_id_top f A mC);
+  clear H.
+
+Local Ltac test_show_st_top_bot f A mC :=
+  test_show_st_bot f A mC;
+  test_show_st_top f A mC.
+
+test_show_st_top_bot f B mC0.
+test_show_st_top_bot (f ∘ g) B mC0.
+test_show_st_top_bot (f ∘ g ∘ i) B mC0.
+test_show_st_top_bot (f ∘ g ∘ i ∘ id_ _ ∘ id_ _) B mC0.
+test_show_st_top_bot (f ∘ (g ∘ id_ _) ∘ i ∘ id_ _ ∘ id_ _) B mC0.
+test_show_st_top_bot ((f ⊗ g) ∘ (g ⊗ i)) B mC0.
+
+
+Local Ltac test_st_of_wk f :=
+  let wf := weak_fencepost_form f in
+  let sf := strong_fencepost_form_of_weak wf in
+  (* idtac wf "=~=>" sf. *)
+  (* For compile: *)
+  idtac.
+
+test_st_of_wk f.
+test_st_of_wk (f ∘ g).
+test_st_of_wk (f ⊗ g).
+
+
+Local Ltac test_ust g :=
+  let u := unfold_tensor_stack g in
+  (* idtac u. *)
+  (* For compile: *)
+  idtac.
+
+test_ust f.
+test_ust (f ∘ g).
+test_ust (f ⊗ g).
+test_ust ((f ⊗ (f ∘ g) ⊗ (f0 ∘ g0))).
+
+
+
+
+
+
+
+
+Local Ltac test_show_wf f :=
+  let H := fresh in 
+  let wf := weak_fencepost_form f in 
+  assert (H: f ≃ wf) by (show_equiv_weak_fencepost_form f);
+  clear H.
+
+test_show_wf f.
+
+
+test_show_wf (f ∘ g).
+test_show_wf (f ⊗ g).
+test_show_wf ((f ∘ g) ⊗ (id_ A)).
+test_show_wf ((f ⊗ id_ _) ∘ (g ⊗ h)).
+test_show_wf (f ⊗ (f0 ∘ g0)).
+test_show_wf (f ⊗ (id_ _ ∘ (g ⊗ h))).
+test_show_wf ((f ⊗ (f ∘ g) ⊗ (f0 ∘ g0))).
+
+test_show_wf ((f ∘ g) ⊗ (f0 ∘ g0)).
+test_show_wf ((f ∘ g) ⊗ (f0)).
+test_show_wf ((f ⊗ ((f ∘ g) ⊗ (f0 ∘ g0)))).
+test_show_wf ((f ⊗ ((f ⊗ g) ∘ (g ⊗ id_ _)))).
+
+test_show_wf ((f ∘ id_ _ ∘ id_ _ ∘ id_ _ ∘ id_ _) 
+  ⊗ ((f ⊗ f0) ∘ (g ⊗ g0) ⊗ (f0 ∘ g0 ∘ id_ _))).
+
+
+
+
+
+
+
+
+Local Ltac test_merge gh :=
+  (* let Mg := merge_stacked_composition_debug gh in
+    idtac "merged:" Mg;
+  let Mg := merge_stacked_composition gh in
+    idtac "merged:" Mg. *)
+  (* For compile: *)
+  let Mg := merge_stacked_composition gh in
+  idtac.
+
+test_merge (mC0.(tensor) @@ f, g).
+test_merge (mC0.(tensor) @@ (mC0.(tensor) @@ f, g), (cC.(compose) f0 g0)).
+
+
+
+Local Ltac test_fence f :=
+  (* let Nf := weak_fencepost_form_debug f in 
+    idtac "fenceposted:" Nf. *)
+  (* For compile: *)
+  let Nf := weak_fencepost_form f in 
+  idtac. 
+
+test_fence ((f ⊗ g ⊗ h) ∘ id_ _).
+test_fence ((f ⊗ g ⊗ h) ∘ id_ _ ∘ id_ _).
+test_fence ((f ⊗ g ⊗ (f0 ∘ g0)) ∘ id_ _ ∘ id_ _).
+test_fence ((f ⊗ g ⊗ (f0 ∘ g0))).
+test_fence ((f ⊗ (f ∘ g) ⊗ (f0 ∘ g0))).
+test_fence ((f ⊗ (f ∘ g) ⊗ (f0 ∘ g0 ∘ id_ _))).
+test_fence (((f ∘ id_ _ ∘ id_ _ ∘ id_ _ ∘ id_ _) 
+  ⊗ (f ∘ g) ⊗ (f0 ∘ g0 ∘ id_ _))).
+test_fence ((f ∘ id_ _ ∘ id_ _ ∘ id_ _ ∘ id_ _) 
+  ⊗ ((f ⊗ f0) ∘ (g ⊗ g0) ⊗ (f0 ∘ g0 ∘ id_ _))).
+
+
+
+tensor_free f.
+Fail tensor_free (f ⊗ g).
+tensor_free (f ∘ g).
+
+tensor_only f.
+tensor_only (f ⊗ g).
+Fail tensor_only (f ∘ g).
+tensor_only ((g⊗h) ⊗ f ⊗ (g⊗(g⊗(g⊗h)))).
+Fail tensor_only ((g⊗h) ⊗ f ⊗ (g⊗(g⊗(g⊗h ∘ id_ _)))).
+(* Note this will match any tensor products, so less useful in Rig category *)
+tensor_only (mC0.(tensor) @@ f, (mC1.(tensor) @@ g, h)).
+
+
+
+is_weak_fenced f.
+is_weak_fenced (f ∘ g).
+is_weak_fenced (f ⊗ g).
+Fail is_weak_fenced ((f ∘ g) ⊗ g).
+is_weak_fenced ((f ⊗ g ⊗ h) ∘ id_ _).
+is_weak_fenced ((f ⊗ (g ⊗ h)) ∘ id_ _).
+is_weak_fenced ((f ⊗ (g ⊗ h)) ∘ (id_ _ ⊗ id_ _)).
+(* We require left_associativity: *)
+Fail is_weak_fenced ((f ⊗ (g ⊗ h)) ∘ (id_ _ ⊗ id_ _) ∘ id_ _).
+     is_weak_fenced ((f ⊗ (g ⊗ h)) ∘ ((id_ _ ⊗ id_ _) ∘ id_ _)).
+(* Note this also works over multiple tensors at once, perhaps undesirably: *)
+is_weak_fenced (mC0.(tensor) @@ (mC1.(tensor) @@ g, h), f).
+is_weak_fenced (mC0.(tensor) @@ f, (mC1.(tensor) @@ g, h)).
+
+
+exact Logic.I.
+Qed.
+
+End Testing.
+
+Local Close Scope Cat_scope.
+
+Module FutureDirections.
+
+Local Open Scope Cat_scope.
+
+Section CatExpr_orig.
+
+Inductive cat_expr_o {C} `{cC : Category C}
+    : forall {A B : C}, A ~> B -> Prop := 
+      (* This _might_ want to be to Type instead? *)
+  | expr_const {A B : C} (f : A ~> B) 
+    : cat_expr_o f
+  | expr_compose {A B M : C} (f : A ~> M) (g : M ~> B) 
+    : cat_expr_o (f ∘ g)
+  | expr_tensor {A1 A2 B1 B2 : C} {mC : @MonoidalCategory C cC} 
+      (g : A1 ~> A2) (h : B1 ~> B2) 
+    : cat_expr_o (g ⊗ h).
+  (* Optionally, 
+  | expr_cast `{ccC: CastCategory C} {A B A' B'} 
+      (HA : A = A') (HB : B = B') (f : A' ~> B')
+    : cat_expr (cast A B HA HB f) *)
+
+End CatExpr_orig.
+
+Require Import RigCategory.
+
+Section CatExpr_hierarchy.
+
+Local Open Scope Rig_scope.
+
+Inductive cat_expr {C} `{cC : Category C}
+    : forall {A B : C}, A ~> B -> Prop := 
+  | cat_id {A : C} : cat_expr (id_ A)
+  | cat_const {A B : C} (f : A ~> B) 
+    : cat_expr f
+  | cat_compose {A B M : C} (f : A ~> M) (g : M ~> B) 
+    : cat_expr (f ∘ g). 
+
+Inductive moncat_expr {C} `{mC : MonoidalCategory C}
+    : forall {A B : C}, A ~> B -> Prop :=
+  | moncat_cat {A B} {f : A ~> B} 
+      : cat_expr f -> moncat_expr f
+  | moncat_tensor {A1 A2 B1 B2 : C} (g : A1 ~> A2) (h : B1 ~> B2) 
+      : moncat_expr (g ⊗ h)
+  | moncat_assoc_for {A B M : C}
+      : moncat_expr (associator (A:=A) (B:=B) (M:=M)).(forward)
+  | moncat_assoc_rev {A B M : C}
+      : moncat_expr (associator (A:=A) (B:=B) (M:=M)).(reverse)
+  (* ... and so on with left_unit, etc. *).
+
+Inductive rigcat_expr {C} `{mC : PreDistributiveBimonoidalCategory C}
+    : forall {A B : C}, A ~> B -> Prop :=
+  | rigcat_cat {A B} {f : A ~> B} 
+    : cat_expr f -> rigcat_expr f
+  | rigcat_plus {A1 A2 B1 B2 : C} (g : A1 ~> A2) (h : B1 ~> B2) 
+    : rigcat_expr (g ⊞ h)
+  | rigcat_times {A1 A2 B1 B2 : C} (g : A1 ~> A2) (h : B1 ~> B2) 
+    : rigcat_expr (g ⊠ h).
+
+End CatExpr_hierarchy.
+
+End FutureDirections.
+
diff --git a/ViCaR/Classes/BraidedMonoidal.v b/ViCaR/Classes/BraidedMonoidal.v
index bbe1685..df0aa02 100644
--- a/ViCaR/Classes/BraidedMonoidal.v
+++ b/ViCaR/Classes/BraidedMonoidal.v
@@ -2,6 +2,8 @@ Require Import Category.
 Require Import Monoidal.
 Require Import Setoid.
 
+#[local] Set Universe Polymorphism.
+
 Local Open Scope Cat.
 
 Notation CommuteBifunctor' F := ({|
diff --git a/ViCaR/Classes/CastCategory.v b/ViCaR/Classes/CastCategory.v
index 47c5f8f..9973fff 100644
--- a/ViCaR/Classes/CastCategory.v
+++ b/ViCaR/Classes/CastCategory.v
@@ -1,8 +1,10 @@
 Require Import Setoid.
 
 Require Export CategoryTypeclass.
+Require Logic.Eqdep_dec. (* only for UIP_dec *)
+Require PeanoNat. (* only for eq_dep on nat *)
 
-Require Import ExamplesAutomation.
+#[local] Set Universe Polymorphism.
 
 Local Open Scope Cat.
 
@@ -605,7 +607,7 @@ Definition CastCategory_of_DecEq_Category {C : Type} (cC: Category C)
     match HA in (_ = a) return (a ~> B' -> A ~> B) with (* Tell coq that A = A' *)
     | eq_refl =>
       fun f => 
-      match HB in (_ = a) return (A ~> a -> A ~> B) with 
+      match HB in (_ = b) return (A ~> b -> A ~> B) with 
       | eq_refl => fun f' => f'
       end f
     end;
@@ -616,7 +618,17 @@ Definition CastCategory_of_DecEq_Category {C : Type} (cC: Category C)
 |}.
 
 Definition CastCategory_of_NatCategory (cC: Category nat) :
-  @CastCategory nat cC.
-apply CastCategory_of_DecEq_Category.
-apply PeanoNat.Nat.eq_dec.
-Defined.
\ No newline at end of file
+  @CastCategory nat cC := {|
+  cast := fun A B A' B' HA HB =>
+    match HA in (_ = a) return (a ~> B' -> A ~> B) with (* Tell coq that A = A' *)
+    | eq_refl =>
+      fun f => 
+      match HB in (_ = b) return (A ~> b -> A ~> B) with 
+      | eq_refl => fun f' => f'
+      end f
+    end;
+  cast_refl := ltac:(intros A B HA HB; 
+    rewrite (Eqdep_dec.UIP_refl_nat _ HA);
+    rewrite (Eqdep_dec.UIP_refl_nat _ HB);
+    reflexivity);
+|}.
\ No newline at end of file
diff --git a/ViCaR/Classes/Category.v b/ViCaR/Classes/Category.v
index b1d03d5..d3b76ea 100644
--- a/ViCaR/Classes/Category.v
+++ b/ViCaR/Classes/Category.v
@@ -4,6 +4,8 @@ Declare Scope Cat_scope.
 Delimit Scope Cat_scope with Cat.
 Local Open Scope Cat.
 
+#[local] Set Universe Polymorphism.
+
 Reserved Notation "A ~> B" (at level 55).
 Reserved Notation "f ≃ g" (at level 60).
 Reserved Notation "A ≅ B" (at level 60).
@@ -354,8 +356,6 @@ Qed.
 Definition ContravariantFunctor {C D : Type} (cC: Category C) (cD : Category D) : Type :=
   Functor (cC^op) cD.
 
-Require Import ExamplesAutomation.
-
 Definition ContravariantFunctor_of_ContraFunctor {C D : Type} 
   `{cC : Category C} `{cD : Category D} (F : ContraFunctor cC cD) : 
   ContravariantFunctor cC cD := {|
diff --git a/ViCaR/Classes/CategoryAutomation.v b/ViCaR/Classes/CategoryAutomation.v
deleted file mode 100644
index 41c3d22..0000000
--- a/ViCaR/Classes/CategoryAutomation.v
+++ /dev/null
@@ -1,305 +0,0 @@
-Require Export CategoryTypeclass.
-
-Ltac assert_not_dup x := 
-  (* try match goal with *)
-  try match goal with
-  | f := ?T : ?T', g := ?T : ?T' |- _ => tryif unify x f then fail 2 else fail 1
-  end.
-
-Ltac saturate_instances class :=
-  (progress repeat (
-    let x:= fresh in let o := open_constr:(class _) in
-    unshelve evar (x:o); [typeclasses eauto|]; 
-    (* let t:= type of x in idtac x ":" t; *) assert_not_dup x))
-  || (progress repeat (
-    let x:= fresh in let o := open_constr:(class _ _) in
-    unshelve evar (x:o); [typeclasses eauto|]; assert_not_dup x))
-  || (progress repeat (
-    let x:= fresh in let o := open_constr:(class _ _ _) in
-    unshelve evar (x:o); [typeclasses eauto|]; assert_not_dup x))
-  || (progress repeat (
-    let x:= fresh in let o := open_constr:(class _ _ _ _) in
-    unshelve evar (x:o); [typeclasses eauto|]; assert_not_dup x))
-  || (progress repeat (
-    let x:= fresh in let o := open_constr:(class _ _ _ _ _) in
-    unshelve evar (x:o); [typeclasses eauto|]; assert_not_dup x))
-  || (progress repeat (
-    let x:= fresh in let o := open_constr:(class _ _ _ _ _ _) in
-    unshelve evar (x:o); [typeclasses eauto|]; assert_not_dup x))
-  || idtac.
-
-Ltac fold_Category cC :=
-  match type of cC with Category ?C =>
-  let catify f := constr:(@f C cC) in
-  let base_fn f := (let raw := catify f in
-    let t := eval cbn in raw in constr:(t)) in
-  let cat_fold f :=
-    (let base := base_fn @f in 
-    let catted := catify @f in
-    change base with catted in *) in
-  try cat_fold @morphism; (* has issues, e.g., with ZX - 
-    might be fixable, but likely not necessary*)
-  cat_fold @compose;
-  cat_fold @c_identity;
-  let cid := base_fn @c_identity in
-    (repeat progress (
-      let H := fresh in let x := fresh in evar (x : C); 
-        let x' := eval unfold x in x in 
-        let cidx := eval cbn in (cid x') in 
-        pose (eq_refl : cidx = cC.(c_identity) x') as H;
-        erewrite H; clear x H));
-  let eqbase := base_fn @equiv in
-  let eqcat := catify @equiv in
-  change eqbase with eqcat; (* I think this is a no-op *)
-  repeat (progress match goal with
-  |- eqbase ?A ?B ?f ?g 
-    => change (eqbase A B f g) with (eqcat A B f g)
-  end);
-  try let H' := fresh in 
-    enough (H':(@equiv _ _ _ _ _ _)) by (eapply H')
-  end.
-
-Ltac fold_all_categories :=
-  saturate_instances Category;
-  repeat match goal with
-  | x := ?cC : Category ?C |- _ => (* idtac x ":=" cC ": Category" C ; *) 
-      fold_Category cC; subst x
-  (* | x : Category ?C |- _ => idtac x; fold_Category x; subst x *)
-  end.
-
-Ltac fold_MonoidalCategory mC :=
-  match type of mC with @MonoidalCategory ?C ?cC =>
-  let catify f := constr:(@f C cC) in
-  let mcatify f := constr:(@f C cC mC) in
-  let base_fn f := 
-    (let t := eval cbn in f in constr:(t)) in
-  let cbase_fn f := (let raw := catify f in
-    let t := eval cbn in raw in constr:(t)) in
-  let mbase_fn f := (let raw := mcatify f in
-    let t := eval cbn in raw in constr:(t)) in
-  let f_fold f :=
-    (let base := base_fn @f in 
-     change base with f) in
-  let cat_fold f :=
-    (let base := cbase_fn @f in 
-    let catted := catify @f in
-    change base with catted in *) in
-  let mcat_fold f :=
-    (let base := mbase_fn @f in 
-    let catted := mcatify @f in
-    change base with catted in *) in
-  let tens := mbase_fn @tensor in
-    let ob_base := base_fn (@obj2_map C C C cC cC cC tens) in
-      change ob_base with mC.(tensor).(obj2_map);
-    let mor_base := base_fn (@morphism2_map C C C cC cC cC tens) in
-      change mor_base with (@morphism2_map C C C cC cC cC mC.(tensor))
-      (* (@tensor C cC mC).(@morphism2_map C C C cC cC cC) *);
-  mcat_fold @I;
-  let lunit := mbase_fn @left_unitor in
-    repeat progress (
-      let H := fresh in let x := fresh in 
-      evar (x : C);  (* TODO: Test this - last I tried it was uncooperative *)
-      let x' := eval unfold x in x in 
-      let lunitx := eval cbn in ((lunit x').(forward)) in
-      pose (eq_refl : lunitx = (mC.(left_unitor) (A:=x')).(forward)) as H;
-      erewrite H; clear x H);
-  let runit := mbase_fn @right_unitor in 
-    repeat progress (
-      let H := fresh in let x := fresh in 
-      evar (x : C);  (* TODO: Test this - last I tried it was uncooperative *)
-      let x' := eval unfold x in x in 
-      let runitx := eval cbn in ((runit x').(forward)) in
-      pose (eq_refl : runitx = (mC.(right_unitor) (A:=x')).(forward)) as H;
-      erewrite H; clear x H)
-  end.
-
-Ltac fold_all_monoidal_categories :=
-  saturate_instances MonoidalCategory;
-  repeat match goal with
-  | x := ?mC : MonoidalCategory ?C |- _ => (* idtac x ":=" cC ": Category" C ; *) 
-      fold_MonoidalCategory mC; subst x
-  (* | x : Category ?C |- _ => idtac x; fold_Category x; subst x *)
-  end.
-
-Ltac fold_BraidedMonoidalCategory bC :=
-  match type of bC with @BraidedMonoidalCategory ?C ?cC ?mC =>
-  let catify f := constr:(@f C cC) in
-  let mcatify f := constr:(@f C cC mC) in
-  let bcatify f := constr:(@f C cC mC bC) in
-  let base_fn f := 
-    (let t := eval cbn in f in constr:(t)) in
-  let cbase_fn f := (let raw := catify f in
-    let t := eval cbn in raw in constr:(t)) in
-  let mbase_fn f := (let raw := mcatify f in
-    let t := eval cbn in raw in constr:(t)) in
-  let bbase_fn f := (let raw := bcatify f in
-    let t := eval cbn in raw in constr:(t)) in
-  let f_fold f :=
-    (let base := base_fn @f in 
-     change base with f) in
-  let cat_fold f :=
-    (let base := cbase_fn @f in 
-    let catted := catify @f in
-    change base with catted in *) in
-  let mcat_fold f :=
-    (let base := mbase_fn @f in 
-    let catted := mcatify @f in
-    change base with catted in *) in
-  let bcat_fold f :=
-    (let base := bbase_fn @f in 
-    let catted := bcatify @f in
-    change base with catted in *) in
-  let braid := bbase_fn @braiding in
-    let braidbase := constr:(ltac:(first [exact (ltac:(eval unfold braid in braid)) | exact braid])) in
-    let braidforw := eval cbn in 
-      (fun A B => (braidbase.(component2_iso) A B).(forward)) in
-    repeat progress (let H := fresh in let y := fresh in let x := fresh in
-      evar (y : C); evar (x : C); 
-      let x' := eval unfold x in x in let y' := eval unfold y in y in
-      let braidforwxy := eval cbn in (braidforw x' y') in
-      pose (eq_refl : braidforwxy = 
-        (bC.(braiding).(component2_iso) x' y').(forward)) as H;
-      erewrite H; clear x y H);
-    
-    let braidrev := eval cbn in
-      (fun A B => (braidbase.(component2_iso) A B).(reverse)) in
-    repeat progress (let H := fresh in let y := fresh in let x := fresh in
-      evar (y : C); evar (x : C); 
-      let x' := eval unfold x in x in let y' := eval unfold y in y in
-      let braidrevxy := eval cbn in (braidrev x' y') in
-      pose (eq_refl : braidrevxy = 
-        (bC.(braiding).(component2_iso) x' y').(reverse)) as H;
-      erewrite H; clear x y H)
-  end.
-
-Ltac fold_all_braided_monoidal_categories :=
-  saturate_instances BraidedMonoidalCategory;
-  repeat match goal with
-  | x := ?bC : BraidedMonoidalCategory ?C |- _ => 
-      fold_BraidedMonoidalCategory bC; subst x
-  end.
-
-Ltac fold_CompactClosedCategory ccC :=
-  match type of ccC with @CompactClosedCategory ?C ?cC ?mC ?bC ?sC =>
-  let catify f := constr:(@f C cC) in
-  let mcatify f := constr:(@f C cC mC) in
-  let bcatify f := constr:(@f C cC mC bC) in
-  let cccatify f := constr:(@f C cC mC bC sC ccC) in
-  let base_fn f := 
-    (let t := eval cbn in f in constr:(t)) in
-  let cbase_fn f := (let raw := catify f in
-    let t := eval cbn in raw in constr:(t)) in
-  let mbase_fn f := (let raw := mcatify f in
-    let t := eval cbn in raw in constr:(t)) in
-  let bbase_fn f := (let raw := bcatify f in
-    let t := eval cbn in raw in constr:(t)) in
-  let ccbase_fn f := (let raw := cccatify f in
-    let t := eval cbn in raw in constr:(t)) in
-  let f_fold f :=
-    (let base := base_fn @f in 
-     change base with f) in
-  let cat_fold f :=
-    (let base := cbase_fn @f in 
-    let catted := catify @f in
-    change base with catted in *) in
-  let mcat_fold f :=
-    (let base := mbase_fn @f in 
-    let catted := mcatify @f in
-    change base with catted in *) in
-  let bcat_fold f :=
-    (let base := bbase_fn @f in 
-    let catted := bcatify @f in
-    change base with catted in *) in
-  let cccat_fold f :=
-    (let base := ccbase_fn @f in 
-    let catted := cccatify @f in
-    change base with catted in *) in
-  
-  let dua := ccbase_fn @dual in
-    (unify dua (@id C) (*; idtac "would loop" *) ) || (
-    repeat progress (
-      let H := fresh in let x := fresh in 
-        evar (x : C);  (* TODO: Test this - last I tried it was uncooperative *)
-        let x' := eval unfold x in x in 
-        let duax := eval cbn in (dua x') in
-        pose (eq_refl : duax = ccC.(dual) x') as H;
-        erewrite H; clear x H));
-  
-  cccat_fold @unit;
-  cccat_fold @counit;
-
-  let uni := ccbase_fn @unit in
-    repeat progress (let H := fresh in let x := fresh in
-      evar (x : C); 
-      let x' := eval unfold x in x in 
-      let unix := eval cbn in (uni x') in
-      pose (eq_refl : unix = 
-        ccC.(unit) (A:=x')) as H;
-      erewrite H; clear x H);
-  
-  let couni := ccbase_fn @counit in
-    repeat progress (let H := fresh in let x := fresh in
-      evar (x : C); 
-      let x' := eval unfold x in x in 
-      let counix := eval cbn in (couni x') in
-      pose (eq_refl : counix = 
-        ccC.(counit) (A:=x')) as H;
-      erewrite H; clear x H)
-  end.
-
-Ltac fold_all_compact_closed_categories :=
-  saturate_instances CompactClosedCategory;
-  repeat match goal with
-  | x := ?ccC : CompactClosedCategory ?C |- _ => 
-      fold_CompactClosedCategory ccC; subst x
-  end.
-
-
-Ltac fold_DaggerCategory dC :=
-  match type of dC with @DaggerCategory ?C ?cC =>
-  let catify f := constr:(@f C cC) in
-  let dcatify f := constr:(@f C cC dC) in
-  let base_fn f := 
-    (let t := eval cbn in f in constr:(t)) in
-  let cbase_fn f := (let raw := catify f in
-    let t := eval cbn in raw in constr:(t)) in
-  let dbase_fn f := (let raw := dcatify f in
-    let t := eval cbn in raw in constr:(t)) in
-  let f_fold f :=
-    (let base := base_fn @f in 
-     change base with f) in
-  let cat_fold f :=
-    (let base := cbase_fn @f in 
-    let catted := catify @f in
-    change base with catted in *) in
-  let dcat_fold f :=
-    (let base := dbase_fn @f in 
-    let catted := dcatify @f in
-    change base with catted in *) in
-  
-  dcat_fold @adjoint;
-
-  let adj := dbase_fn @adjoint in
-    repeat progress (let H := fresh in 
-    let x := fresh in let y := fresh in
-      evar (x : C); evar (y : C);
-      let x' := eval unfold x in x in 
-      let y' := eval unfold y in y in 
-      let adjxy := eval cbn in (adj x' y') in
-      pose (eq_refl : adjxy = 
-        dC.(adjoint) (A:=x') (B:=y')) as H;
-      erewrite H; clear x y H)
-  end.
-
-Ltac fold_all_dagger_categories :=
-  saturate_instances DaggerCategory;
-  repeat match goal with
-  | x := ?dC : DaggerCategory ?C |- _ => 
-      fold_DaggerCategory dC; subst x
-  end.
-
-Ltac to_Cat :=
-  fold_all_categories; fold_all_monoidal_categories;
-  fold_all_braided_monoidal_categories; 
-  fold_all_compact_closed_categories;
-  fold_all_dagger_categories.
\ No newline at end of file
diff --git a/ViCaR/Classes/CompactClosed.v b/ViCaR/Classes/CompactClosed.v
index d3c2261..4883346 100644
--- a/ViCaR/Classes/CompactClosed.v
+++ b/ViCaR/Classes/CompactClosed.v
@@ -3,6 +3,8 @@ Require Import Monoidal.
 Require Import BraidedMonoidal.
 Require Import SymmetricMonoidal.
 
+#[local] Set Universe Polymorphism.
+
 Local Open Scope Cat.
 
 Reserved Notation "A ★" (at level 0).
diff --git a/ViCaR/Classes/Dagger.v b/ViCaR/Classes/Dagger.v
index d883751..1ccacc3 100644
--- a/ViCaR/Classes/Dagger.v
+++ b/ViCaR/Classes/Dagger.v
@@ -1,6 +1,8 @@
 Require Import Setoid.
 Require Import Category.
 
+#[local] Set Universe Polymorphism.
+
 Local Open Scope Cat.
 
 Reserved Notation "f †" (at level 0).
diff --git a/ViCaR/Classes/DaggerBraidedMonoidal.v b/ViCaR/Classes/DaggerBraidedMonoidal.v
index 7ca1dd8..3688210 100644
--- a/ViCaR/Classes/DaggerBraidedMonoidal.v
+++ b/ViCaR/Classes/DaggerBraidedMonoidal.v
@@ -4,6 +4,8 @@ Require Import Monoidal.
 Require Import BraidedMonoidal.
 Require Import DaggerMonoidal.
 
+#[local] Set Universe Polymorphism.
+
 Local Open Scope Cat.
 
 Class DaggerBraidedMonoidalCategory (C : Type) 
diff --git a/ViCaR/Classes/DaggerMonoidal.v b/ViCaR/Classes/DaggerMonoidal.v
index 693f167..d381838 100644
--- a/ViCaR/Classes/DaggerMonoidal.v
+++ b/ViCaR/Classes/DaggerMonoidal.v
@@ -2,6 +2,8 @@ Require Import Category.
 Require Import Dagger.
 Require Import Monoidal.
 
+#[local] Set Universe Polymorphism.
+
 Local Open Scope Cat.
 
 Class DaggerMonoidalCategory (C : Type) 
diff --git a/ViCaR/Classes/DaggerSymmetricMonoidal.v b/ViCaR/Classes/DaggerSymmetricMonoidal.v
index 07f5dc9..3818f05 100644
--- a/ViCaR/Classes/DaggerSymmetricMonoidal.v
+++ b/ViCaR/Classes/DaggerSymmetricMonoidal.v
@@ -5,6 +5,8 @@ Require Import BraidedMonoidal.
 Require Import DaggerMonoidal.
 Require Import SymmetricMonoidal.
 
+#[local] Set Universe Polymorphism.
+
 Local Open Scope Cat.
 
 Class DaggerSymmetricMonoidalCategory (C : Type) 
diff --git a/ViCaR/Classes/Monoidal.v b/ViCaR/Classes/Monoidal.v
index d6ec279..0ac9fb6 100644
--- a/ViCaR/Classes/Monoidal.v
+++ b/ViCaR/Classes/Monoidal.v
@@ -1,6 +1,8 @@
 Require Import Category.
 Require Import Setoid.
 
+#[local] Set Universe Polymorphism.
+
 Local Open Scope Cat_scope.
 
 Reserved Notation "x × y" (at level 40, left associativity). (* \times *)
diff --git a/ViCaR/Classes/RigCategory.v b/ViCaR/Classes/RigCategory.v
index b7b884d..bef6713 100644
--- a/ViCaR/Classes/RigCategory.v
+++ b/ViCaR/Classes/RigCategory.v
@@ -5,8 +5,9 @@ Require Import Monoidal.
 Require Import BraidedMonoidal.
 Require Import SymmetricMonoidal.
 
-Local Open Scope Cat_scope.
+#[local] Set Universe Polymorphism.
 
+Local Open Scope Cat_scope.
 
 Class PreDistributiveBimonoidalCategory {C : Type} `{cC : Category C}
   `(AddC : SymmetricMonoidalCategory C (cC:=cC))
@@ -45,6 +46,7 @@ Class PreDistributiveBimonoidalCategory {C : Type} `{cC : Category C}
 }.
 
 Declare Scope Rig_scope.
+Delimit Scope Rig_scope with Rig.
 Open Scope Rig_scope.
 
 Definition add_of_prerig {C} {cC}
diff --git a/ViCaR/Classes/SymmetricMonoidal.v b/ViCaR/Classes/SymmetricMonoidal.v
index fed3ec0..2f11b8b 100644
--- a/ViCaR/Classes/SymmetricMonoidal.v
+++ b/ViCaR/Classes/SymmetricMonoidal.v
@@ -2,6 +2,8 @@ Require Import Category.
 Require Import Monoidal.
 Require Import BraidedMonoidal.
 
+#[local] Set Universe Polymorphism.
+
 Local Open Scope Cat.
 
 Class SymmetricMonoidalCategory (C : Type) `{BraidedMonoidalCategory C} : Type := {
diff --git a/ViCaR/GeneralLemmas.v b/ViCaR/GeneralLemmas.v
index c0d962a..d7703be 100644
--- a/ViCaR/GeneralLemmas.v
+++ b/ViCaR/GeneralLemmas.v
@@ -59,7 +59,7 @@ Proof.
   easy.
 Qed.
 
-Ltac fencestep :=
+(* Ltac fencestep :=
   let test_simple t := match t with
     | context[(_ ⊗ _) ∘ _] => fail 2
     | context[_ ∘ (_ ⊗ _)] => fail 2
@@ -80,7 +80,7 @@ Ltac fencestep :=
   |- context[(?f ∘ ?g) ⊗ (?h)] =>
       test_simple f; test_simple g; test_simple h;
       rewrite (stack_distr_pushout_r_bot f g h)
-  end].
+  end]. *)
 
 
 
@@ -100,7 +100,12 @@ Ltac fencestep :=
       id  id  id  id                          id  id
       ). I suspect the strict spec will make reasoning
       much easier, i.e. to process f⊗g, we *must* push it out
-      to f⊗id ∘ id⊗g. *) *)
+      to f⊗id ∘ id⊗g. *) 
+*)
+
+
+
+
 
 
 
@@ -128,8 +133,6 @@ Proof.
   easy.
 Qed.
 
-Require Import ExamplesAutomation.
-
 Lemma stack_id_compose_split_top : forall {C : Type}
   {Cat: Category C} {MonCat : MonoidalCategory C}
   {topIn topMid topOut bot : C} 
@@ -152,136 +155,5 @@ Proof.
   easy.
 Qed.
 
-(* Ignore this stuff for now: *)
-
-Ltac _fencepost term :=
-  match term with
-  | id_ ?A => idtac
-  | ?f ⊗ id_ _ => _fencepost f; idtac "fix:"; print_state
-  | id_ _ ⊗ ?f => _fencepost f; idtac "fix:"; print_state
-  | ?f ∘ ?g => idtac f "∘" g; _fencepost f; _fencepost g
-  | ?f ⊗ ?g => idtac f "⊗" g; match type of f with
-    | ?topIn ~> ?topOut => match type of g with
-    | ?botIn ~> ?botOut => rewrite <- (nwire_stackcompose_topright_general f g);
-      _fencepost (f ⊗ c_identity botIn); _fencepost (c_identity topOut ⊗ g)
-    end end
-  | ?f => idtac "should be clean:" f
-  end.
-
-Ltac __fencepost term :=
-  match term with
-  | id_ ?A => idtac
-  | ?f ∘ ?g => (* idtac f "∘" g; *) __fencepost f; __fencepost g
-  | ?f ⊗ id_ _ => __fencepost f  (* ; idtac "fix:"; print_state *)
-  | id_ _ ⊗ ?f => __fencepost f  (* ; idtac "fix:"; print_state *)
-  | (?f ∘ ?g) ⊗ (?h ∘ ?i) => first [
-    first [progress __fencepost f; rewrite ?assoc |
-    progress __fencepost g; rewrite ?assoc |
-    progress __fencepost h; rewrite ?assoc |
-    progress __fencepost i; rewrite ?assoc];
-    idtac "hit1"; __fencepost term; idtac "hit2" |
-    rewrite (compose2_map f g h i); __fencepost (f⊗h); __fencepost (g⊗i)]
-  | (?f ∘ ?g) ⊗ ?h => first [
-    progress __fencepost f; rewrite ?assoc |
-    progress __fencepost g; rewrite ?assoc |
-    progress __fencepost h; rewrite ?assoc |
-    rewrite (stack_distr_pushout_r_bot f g h)]
-  | ?f ⊗ (?g ∘ ?h) => first [
-    progress __fencepost f; rewrite ?assoc |
-    progress __fencepost g; rewrite ?assoc |
-    progress __fencepost h; rewrite ?assoc |
-    rewrite (stack_distr_pushout_r_top f g h)]
-  | ?f ⊗ ?g => first [
-    progress __fencepost f; rewrite ?assoc |
-    progress __fencepost g; rewrite ?assoc |
-    rewrite <- (nwire_stackcompose_topright_general f g)]
-  (* | ?f ⊗ ?g => idtac f "⊗" g; match type of f with
-    | ?topIn ~> ?topOut => match type of g with
-    | ?botIn ~> ?botOut => rewrite <- (nwire_stackcompose_topright_general f g);
-      __fencepost (f ⊗ c_identity botIn); __fencepost (c_identity topOut ⊗ g)
-    end end *)
-  | ?f => idtac "should be clean:" f
-  end.
-
-Ltac weak_fencepost term := 
-  let fence f := progress (weak_fencepost f) in
-  match term with
-  | id_ ?A => idtac
-  | ?f ∘ ?g => (* idtac f "∘" g; *) weak_fencepost f; weak_fencepost g
-  (* | ?f ⊗ id_ _ => fence f  (* ; idtac "fix:"; print_state *)
-  | id_ _ ⊗ ?f => fence f  (* ; idtac "fix:"; print_state *) *)
-  | (?f ∘ ?g) ⊗ (?h ∘ ?i) => first [
-    (* first [fence f | fence g | fence h | fence i]; 
-      rewrite ?assoc; weak_fencepost term | *)
-    rewrite (compose2_map f g h i); 
-      weak_fencepost (f⊗h); weak_fencepost (g⊗i)]
-  | (?f ∘ ?g) ⊗ ?h => first [
-    (* first [fence f | fence g | fence h]; 
-      rewrite ?assoc; weak_fencepost term | *)
-    rewrite (stack_distr_pushout_r_bot f g h)]
-  | ?f ⊗ (?g ∘ ?h) => first [
-    (* first [fence f | fence g | fence h]; 
-      idtac term; rewrite ?assoc; idtac term; weak_fencepost term | *)
-    rewrite (stack_distr_pushout_r_top f g h)]
-  | ?f ⊗ ?g => first [
-    (* first [fence f | fence g]; 
-      rewrite ?assoc; weak_fencepost term | *)
-    rewrite <- (nwire_stackcompose_topright_general f g)]
-  (* | ?f ⊗ ?g => idtac f "⊗" g; match type of f with
-    | ?topIn ~> ?topOut => match type of g with
-    | ?botIn ~> ?botOut => rewrite <- (nwire_stackcompose_topright_general f g);
-      __fencepost (f ⊗ c_identity botIn); __fencepost (c_identity topOut ⊗ g)
-    end end *)
-  | ?f => idtac "should be clean:" f
-  end.
-
-Ltac weak_fencepost' term := 
-  match term with
-  | id_ ?A => idtac
-  | ?f ∘ ?g => (* idtac f "∘" g; *) weak_fencepost f; weak_fencepost g
-  (* | ?f ⊗ id_ _ => fence f  (* ; idtac "fix:"; print_state *)
-  | id_ _ ⊗ ?f => fence f  (* ; idtac "fix:"; print_state *) *)
-  | (?f ∘ ?g) ⊗ (?h ∘ ?i) => first [
-    (* first [fence f | fence g | fence h | fence i]; 
-      rewrite ?assoc; weak_fencepost term | *)
-    rewrite (compose2_map f g h i); 
-      weak_fencepost (f⊗h); weak_fencepost (g⊗i)]
-  | (?f ∘ ?g) ⊗ ?h => first [
-    (* first [fence f | fence g | fence h]; 
-      rewrite ?assoc; weak_fencepost term | *)
-    rewrite (stack_distr_pushout_r_bot f g h)]
-  | ?f ⊗ (?g ∘ ?h) => first [
-    (* first [fence f | fence g | fence h]; 
-      idtac term; rewrite ?assoc; idtac term; weak_fencepost term | *)
-    rewrite (stack_distr_pushout_r_top f g h)]
-  | ?f ⊗ ?g => first [
-    (* first [fence f | fence g]; 
-      rewrite ?assoc; weak_fencepost term | *)
-    rewrite <- (nwire_stackcompose_topright_general f g)]
-  (* | ?f ⊗ ?g => idtac f "⊗" g; match type of f with
-    | ?topIn ~> ?topOut => match type of g with
-    | ?botIn ~> ?botOut => rewrite <- (nwire_stackcompose_topright_general f g);
-      __fencepost (f ⊗ c_identity botIn); __fencepost (c_identity topOut ⊗ g)
-    end end *)
-  | ?f => idtac "should be clean:" f
-  end.
-
-Definition cast_fn {C : Type} `{Category C} (A B : C) {A' B' : C} 
-  (prfA : A = A') (prfB : B = B') (f : A' ~> B') : A ~> B.
-Proof.
-  destruct prfA.
-  destruct prfB.
-  exact f.
-Defined.
-
-Add Parametric Morphism {C : Type} `{cC : Category C} {A B : C} {A' B' : C}
-  {prfA : A = A'} {prfB : B = B'} : (@cast_fn C cC A B A' B' prfA prfB)
-  with signature
-  (@Category.equiv C cC A' B') ==> (@Category.equiv C cC A B) as cast_fn_equiv_morphism.
-Proof.
-  intros. 
-  subst.
-  easy.
-Qed.
 
 Local Close Scope Cat.
diff --git a/examples/DirectSumMatrixExample.v b/examples/DirectSumMatrixExample.v
index af0c0bb..897a7d7 100644
--- a/examples/DirectSumMatrixExample.v
+++ b/examples/DirectSumMatrixExample.v
@@ -1,6 +1,6 @@
 Require Import MatrixExampleBase.
 Require Import MatrixPermBase.
-From ViCaR Require Import ExamplesAutomation.
+Require Import ExamplesAutomation.
 
 #[export] Instance MxCategory : Category nat := {
   morphism := Matrix;
diff --git a/ViCaR/Classes/ExamplesAutomation.v b/examples/ExamplesAutomation.v
similarity index 100%
rename from ViCaR/Classes/ExamplesAutomation.v
rename to examples/ExamplesAutomation.v
diff --git a/examples/KronComm.v b/examples/KronComm.v
index 0882023..30714fd 100644
--- a/examples/KronComm.v
+++ b/examples/KronComm.v
@@ -6,7 +6,7 @@ From VyZX Require Import PermutationRules.
 Require Import MatrixExampleBase.
 Require Import MatrixPermBase.
 From ViCaR Require Export CategoryTypeclass.
-From ViCaR Require Import ExamplesAutomation.
+Require Import ExamplesAutomation.
 
 Local Open Scope matrix_scope.
 
diff --git a/examples/KronComm_orig.v b/examples/KronComm_orig.v
index c83fff2..4059149 100644
--- a/examples/KronComm_orig.v
+++ b/examples/KronComm_orig.v
@@ -359,7 +359,7 @@ Proof.
   - rewrite (Nat.div_small i m),
   (Nat.mod_small i m), Nat.eqb_refl, andb_true_r, andb_true_l by easy.
   replace ((j / o =? k) && (j / o <? n)) with (j / o =? k) by bdestructΩ'.
-  ExamplesAutomation.bdestruct_one_old; [|easy].
+  (*mark*) bdestruct_one; [|easy].
   rewrite mod_eq_sub; f_equal;
   lia.
   - bdestructΩ'.
@@ -380,7 +380,7 @@ Proof.
   - rewrite (Nat.div_small j o),
   (Nat.mod_small j o), Nat.eqb_refl, andb_true_r, andb_true_l by easy.
   replace ((i / m =? k) && (i / m <? n)) with (i / m =? k) by bdestructΩ'.
-  ExamplesAutomation.bdestruct_one_old; [|easy].
+  (*mark*) bdestruct_one; [|easy].
   rewrite mod_eq_sub; f_equal;
   lia.
   - bdestructΩ'.
@@ -401,7 +401,7 @@ Proof.
   - rewrite (Nat.div_small i m), Nat.eqb_refl, andb_true_r, andb_true_l by easy.
   rewrite Nat.mod_small by easy.
   replace ((j / o =? k) && (j / o <? n)) with ((k * o <=? j) && (j <? S k * o)).
-  + do 2 ExamplesAutomation.bdestruct_one_old; simpl; try easy.
+  + do 2 (*mark*) bdestruct_one; simpl; try easy.
     destruct o; [lia|].
     f_equal.
     rewrite mod_eq_sub, Nat.mul_comm.
@@ -434,7 +434,7 @@ Proof.
   - rewrite (Nat.div_small j o), Nat.eqb_refl, andb_true_r, andb_true_l by easy.
   rewrite (Nat.mod_small j o) by easy.
   replace ((i / m =? k) && (i / m <? n)) with ((k * m <=? i) && (i <? S k * m)).
-  + do 2 ExamplesAutomation.bdestruct_one_old; simpl; try easy.
+  + do 2 (*mark*) bdestruct_one; simpl; try easy.
     destruct m; [lia|].
     f_equal.
     rewrite mod_eq_sub, Nat.mul_comm.
@@ -501,7 +501,7 @@ Proof.
   [| rewrite Nat.mul_eq_0; lia].
   unfold Matrix.I.
   rewrite <- 2!andb_if.
-  ExamplesAutomation.bdestruct_one_old; [
+  (*mark*) bdestruct_one; [
   rewrite 2!andb_true_r, andb_true_l | rewrite 4!andb_false_r; easy
   ].
   easy.
@@ -528,7 +528,7 @@ Proof.
   simpl.
   replace (i / n <? m) with true by (
   symmetry; rewrite Nat.ltb_lt; apply Nat.div_lt_upper_bound; lia).
-  ExamplesAutomation.bdestruct_one_old; [ExamplesAutomation.bdestruct_one_old|]; simpl; symmetry; [
+  (*mark*) bdestruct_one; [(*mark*) bdestruct_one|]; simpl; symmetry; [
   apply big_sum_unique;
   exists (j / m)%nat;
   split; [ apply Nat.div_lt_upper_bound; lia | ];
diff --git a/examples/KronMatrixExample.v b/examples/KronMatrixExample.v
index 45b2404..66f3277 100644
--- a/examples/KronMatrixExample.v
+++ b/examples/KronMatrixExample.v
@@ -2,7 +2,7 @@
 Require Import MatrixPermBase.
 Require Import KronComm.
 Require Export MatrixExampleBase.
-From ViCaR Require Import ExamplesAutomation.
+Require Import ExamplesAutomation.
 
 
 #[export] Instance MxCategory : Category nat := {
diff --git a/examples/MatrixExampleBase.v b/examples/MatrixExampleBase.v
index cd7935e..5bb9e28 100644
--- a/examples/MatrixExampleBase.v
+++ b/examples/MatrixExampleBase.v
@@ -7,7 +7,7 @@ Ltac Zify.zify_post_hook ::= PreOmega.Z.div_mod_to_equations.
 From VyZX Require Export PermutationAutomation PermutationFacts PermutationInstances.
 From ViCaR Require Export CategoryTypeclass.
 From QuantumLib Require Export Matrix.
-From ViCaR Require Import ExamplesAutomation.
+Require Import ExamplesAutomation.
 
 Open Scope matrix_scope.
 
diff --git a/examples/MatrixPermBase.v b/examples/MatrixPermBase.v
index 79f8bcb..ee57cb4 100644
--- a/examples/MatrixPermBase.v
+++ b/examples/MatrixPermBase.v
@@ -1,5 +1,5 @@
 Require Export MatrixExampleBase.
-From ViCaR Require Import ExamplesAutomation.
+Require Import ExamplesAutomation.
 
 Lemma perm_mat_permutes_ei_r : forall n f k, (k < n)%nat ->
   (perm_mat n f) × (e_i k) = e_i (f k).
diff --git a/examples/NatRelationsExample.v b/examples/NatRelationsExample.v
index 7129a9a..bdbbb21 100644
--- a/examples/NatRelationsExample.v
+++ b/examples/NatRelationsExample.v
@@ -4,7 +4,7 @@ From ViCaR Require Export CategoryTypeclass.
 Require Import Psatz.
 
 From QuantumLib Require Import Prelim.
-From ViCaR Require Import ExamplesAutomation.
+Require Import ExamplesAutomation.
 From ViCaR Require Export CategoryTypeclass.
 
 
diff --git a/examples/ZXExample.v b/examples/ZXExample.v
index 373a1b7..69a6499 100644
--- a/examples/ZXExample.v
+++ b/examples/ZXExample.v
@@ -1592,6 +1592,11 @@ Qed.
 
 #[export] Instance ZXDaggerSymmetricMonoidalCategory : DaggerSymmetricMonoidalCategory nat := {}. 
 
+
+
+
+
+(* 
 Ltac not_evar' v :=
   not_evar v; try (let v := eval unfold v in v in 
   tryif not_evar v then idtac else fail 1).
@@ -1670,7 +1675,7 @@ Lemma gen_id {n} : forall (zx : ZX n n) prfn prfm,
   evarify_cast'. (* Replace all proofs with evars *)
   rewrite temp_id.
   reflexivity.
-Qed.
+Qed. *)
 
 
 
@@ -1686,10 +1691,28 @@ Lemma test  :  forall {n m o} (zx0 : ZX n m) (zx1 : ZX m o),
 	(zx0 ⟷ zx1) ↕ —  ∝ (zx0 ↕ —) ⟷ (zx1 ↕ —).
 Proof.
   (* setoid_rewrite wire_to_n_wire. *)
-  to_Cat.
   intros.
   rewrite wire_to_n_wire.
-  
+  fold_all_categories;
+  fold_all_monoidal_categories.
+  match goal with
+  |- (?T ≃ ?T')%Cat => 
+    strong_fencepost_no_id T
+  end.
+  easy.
+Qed.
+
+Lemma test2 :  forall {n m o p} (zx0 : ZX n m) (zx1 : ZX o p),
+	(zx0 ↕ zx1)  ∝ (zx0 ↕ n_wire _) ⟷ (n_wire _ ↕ zx1).
+Proof.
+  (* setoid_rewrite wire_to_n_wire. *)
+  intros.
   to_Cat.
-  Admitted.
-  
+  (* fold_all_categories;
+  fold_all_monoidal_categories. *)
+  match goal with
+  |- (?T ≃ ?T')%Cat => 
+    strong_fencepost_no_id T
+  end.
+  easy.
+Qed.
\ No newline at end of file