diff --git a/ViCaR/AutomaticParsing.v b/ViCaR/AutomaticParsing.v
new file mode 100644
index 0000000..aa46c8c
--- /dev/null
+++ b/ViCaR/AutomaticParsing.v
@@ -0,0 +1,216 @@
+Require Import CategoryTypeclass.
+
+Open Scope Cat_scope.
+Open Scope Mor_scope.
+Open Scope Mon_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).
+
+Arguments cat_expr {_} _%Cat {_ _}%Obj _%Mor.
+
+Inductive moncat_expr {C} {cC : Category C} {mC : MonoidalCategory cC}
+    : forall {A B : C}, A ~> B -> Prop :=
+  | moncat_id (A : C) 
+    : moncat_expr (id_ A)
+  | moncat_assoc_for (A B M : C)
+    : moncat_expr (associator A B M).(forward)
+  | moncat_assoc_rev (A B M : C)
+    : moncat_expr (associator A B M).(reverse)
+  | moncat_lunit_for (A : C)
+    : moncat_expr (left_unitor A).(forward)
+  | moncat_lunit_rev (A : C)
+    : moncat_expr (left_unitor A).(reverse)
+  | moncat_runit_for (A : C) 
+    : moncat_expr (right_unitor A).(forward)
+  | moncat_runit_rev (A : C) 
+    : moncat_expr (right_unitor A).(reverse)
+  | moncat_compose {A B M : C} {f : A ~> B} {g : B ~> M}
+    : moncat_expr f -> moncat_expr g -> moncat_expr (f ∘ g)
+  | moncat_tensor {A1 A2 B1 B2 : C} {f : A1 ~> A2} {g : B1 ~> B2}
+    : moncat_expr f -> moncat_expr g -> moncat_expr (f ⊗ g)
+  | moncat_const {A B : C} (f : A ~> B) 
+    : moncat_expr f.
+
+Arguments moncat_expr {_} {_}%Cat _%Cat {_ _}%Obj _%Mor.
+
+Ltac make_moncat_expr (* mC *) t :=
+  let rec make_mon (* mC *) t :=
+  (* lazymatch type of mC with
+  | @MonoidalCategory ?C ?cC => *)
+  match t with
+  | id_ ?A => constr:(moncat_id A)
+  | (associator ?A ?B ?C).(forward) => constr:(moncat_assoc_for A B C)
+  | (associator ?A ?B ?C).(forward) => constr:(moncat_assoc_for A B C)
+  | (left_unitor ?A).(forward) => constr:(moncat_lunit_for A)
+  | (left_unitor ?A).(reverse) => constr:(moncat_lunit_rev A)
+  | (right_unitor ?A).(forward) => constr:(moncat_runit_for A)
+  | (right_unitor ?A).(reverse) => constr:(moncat_runit_rev A)
+  | (?g ∘ ?h)%Mor => let mcg := make_mon g in let mch := make_mon h in 
+      constr:(moncat_compose mcg mch)
+  | (?g ⊗ ?h)%Mon => let mcg := make_mon g in let mch := make_mon h in 
+      constr:(moncat_tensor mcg mch)
+  | _ => constr:(moncat_const t)
+  end
+  (* end *)
+  in make_mon (* mC *) t.
+
+Ltac make_moncat_expr_debug (* mC *) t :=
+  let rec make_mon (* mC *) t :=
+  (* lazymatch type of mC with
+  | @MonoidalCategory ?C ?cC => *)
+  lazymatch t with
+  | id_ ?A => 
+      
+    constr:(moncat_id A)
+  | (associator ?A ?B ?C).(forward) => 
+    constr:(moncat_assoc_for A B C)
+  | (associator ?A ?B ?C).(forward) => 
+    constr:(moncat_assoc_for A B C)
+  | (left_unitor ?A).(forward) => constr:(moncat_lunit_for A)
+  | (left_unitor ?A).(reverse) => constr:(moncat_lunit_rev A)
+  | (right_unitor ?A).(forward) => constr:(moncat_runit_for A)
+  | (right_unitor ?A).(reverse) => constr:(moncat_runit_rev A)
+  | (?g ∘ ?h)%Mor => let mcg := make_mon g in let mch := make_mon h in 
+      constr:(moncat_compose mcg mch)
+  | (?g ⊗ ?h)%Mon => let mcg := make_mon g in let mch := make_mon h in 
+      constr:(moncat_tensor mcg mch)
+  | _ => constr:(moncat_const t)
+  end
+  (* end *)
+  in make_mon (* mC *) t.
+
+Require Import String.
+
+(* Definition moncat_to_str :  *)
+
+Lemma parse_test_0 : forall {C : Type}
+  {cC : Category C} {mC : MonoidalCategory cC}
+  {top botIn botMid botOut : C} 
+  (f0 : botIn ~> botMid) (f1 : botMid ~> botOut),
+  (id_ top) ⊗ (f0 ∘ f1) ≃ id_ top ⊗ f0 ∘ (id_ top ⊗ f1).
+Proof.
+  intros.
+  match goal with 
+  |- (?t ≃ ?t')%Cat => let mct := make_moncat_expr_debug t in pose mct;
+    let mct' := make_moncat_expr_debug t' in pose mct'
+  end.
+  Admitted.
+
+Lemma parse_test_1 : forall {C : Type}
+  {cC : Category C} {mC : MonoidalCategory cC}
+  {top botIn botMid botOut : C} 
+  (f0 : botIn ~> botMid) (f1 : botMid ~> botOut),
+  (id_ top) ⊗ (f0 ∘ f1) ∘ (λ_ _)^-1 ≃ id_ top ⊗ f0 ∘ (id_ top ⊗ f1) ∘ (λ_ _)^-1.
+Proof.
+  intros.
+  match goal with 
+  |- (?t ≃ ?t')%Cat => let mct := make_moncat_expr_debug t in pose mct;
+    let mct' := make_moncat_expr_debug t' in pose mct'
+  end.
+  Admitted.
+
+
+Ltac print_moncat_expr m :=
+  first [lazymatch m with
+  | moncat_id ?A => 
+    idtac "['id', (1), (1), ['" A "'], 'id_{&1}']"
+    (* : moncat_expr (id_ A) *)
+  | moncat_assoc_for ?A ?B ?M => 
+    idtac "['assoc_for', ((1,2),3), (1,(2,3)), ['" A "','" B "','" M "'], 'α^-1_{&1,&2,&3}']"
+    (* : moncat_expr (associator A B M).(forward) *)
+  | moncat_assoc_rev ?A ?B ?M => 
+    idtac "['assoc_rev', ((1,2),3), (1,(2,3)), ['" A "','" B "','" M "'], 'α_{&1,&2,&3}']"
+    (* : moncat_expr (associator A B M).(reverse) *)
+  | moncat_lunit_for ?A =>
+    idtac "['lunit_for', ('I',1), (1), ['" A "'], 'λ_{&1}']"
+    (* : moncat_expr (left_unitor A).(forward) *)
+  | moncat_lunit_rev ?A => 
+    idtac "['lunit_rev', (1), ('I',1), ['" A "'], 'λ^-1_{&1}']"
+    (* : moncat_expr (left_unitor A).(reverse) *)
+  | moncat_runit_for ?A =>
+    idtac "['runit_for', (1,'I'), (1), ['" A "'], 'ρ_{&1}']"
+    (* : moncat_expr (right_unitor A).(forward) *)
+  | moncat_runit_rev ?A =>
+    idtac "['runit_rev', (1), (1,'I'), ['" A "'], 'ρ^-1_{&1}']"
+    (* : moncat_expr (right_unitor A).(reverse) *)
+  | @moncat_compose _ _ _ ?A ?B ?M _ _ ?mcf ?mcg =>
+    idtac "['*compose', (1), (2), ['" A "','" M "'], [";
+    print_moncat_expr mcf; idtac ","; print_moncat_expr mcg; idtac "]]"
+    (* : moncat_expr f -> moncat_expr g -> moncat_expr (f ∘ g) *)
+  | @moncat_tensor _ _ _ ?A1 ?A2 ?B1 ?B2 _ _ ?mcf ?mcg =>
+    idtac "['*tensor', (1,2), (3,4), ['" A1 "','" B1 "','" A2 "','" B2 "'], [";
+    print_moncat_expr mcf; idtac ","; print_moncat_expr mcg; idtac "]]"
+    (* : moncat_expr g -> moncat_expr h -> moncat_expr (g ⊗ h) *)
+  | @moncat_const _ _ _ ?A ?B ?f =>
+    idtac "['const', ('" A "'), ('" A "'), '" f "']"
+    (* : moncat_expr f. *)
+  end | idtac "BAD EXPR" m].
+
+
+Ltac print_moncat_expr_JSON m :=
+  first [lazymatch m with
+  | moncat_id ?A => 
+    idtac "['id', [1], [1], ['"A"'], 'id_{&1}']"
+    (* : moncat_expr (id_ A) *)
+  | moncat_assoc_for ?A ?B ?M => 
+    idtac "['assoc_for', [[1,2],3], [1,[2,3]], ['"A"','"B"','"M"'], 'α^-1_{&1,&2,&3}']"
+    (* : moncat_expr (associator A B M).(forward) *)
+  | moncat_assoc_rev ?A ?B ?M => 
+    idtac "['assoc_rev', [[1,2],3], [1,[2,3]], ['"A"','"B"','"M"'], 'α_{&1,&2,&3}']"
+    (* : moncat_expr (associator A B M).(reverse) *)
+  | moncat_lunit_for ?A =>
+    idtac "['lunit_for', ['I',1], [1], ['"A"'], 'λ_{&1}']"
+    (* : moncat_expr (left_unitor A).(forward) *)
+  | moncat_lunit_rev ?A => 
+    idtac "['lunit_rev', [1], ['I',1], ['"A"'], 'λ^-1_{&1}']"
+    (* : moncat_expr (left_unitor A).(reverse) *)
+  | moncat_runit_for ?A =>
+    idtac "['runit_for', [1,'I'], [1], ['"A"'], 'ρ_{&1}']"
+    (* : moncat_expr (right_unitor A).(forward) *)
+  | moncat_runit_rev ?A =>
+    idtac "['runit_rev', [1], [1,'I'], ['"A"'], 'ρ^-1_{&1}']"
+    (* : moncat_expr (right_unitor A).(reverse) *)
+  | @moncat_compose _ _ _ ?A ?B ?M _ _ ?mcf ?mcg =>
+    idtac "['*compose', [1], [2], ['"A"','"M"'], [";
+    print_moncat_expr mcf; idtac ","; print_moncat_expr mcg; idtac "]]"
+    (* : moncat_expr f -> moncat_expr g -> moncat_expr (f ∘ g) *)
+  | @moncat_tensor _ _ _ ?A1 ?A2 ?B1 ?B2 _ _ ?mcf ?mcg =>
+    idtac "['*tensor', [1,2], [3,4], ['"A1"','"B1"','"A2"','"B2"'], [";
+    print_moncat_expr mcf; idtac ","; print_moncat_expr mcg; idtac "]]"
+    (* : moncat_expr g -> moncat_expr h -> moncat_expr (g ⊗ h) *)
+  | @moncat_const _ _ _ ?A ?B ?f =>
+    idtac "['const', ['"A"'], ['"A"'], '"f"']"
+    (* : moncat_expr f. *)
+  end | idtac "BAD EXPR" m].
+
+Lemma print_test_0 : forall {C : Type}
+  {cC : Category C} {mC : MonoidalCategory cC}
+  {top botIn botMid botOut : C} 
+  (f0 : botIn ~> botMid) (f1 : botMid ~> botOut),
+  (id_ top) ⊗ (f0 ∘ f1) ≃ id_ top ⊗ f0 ∘ (id_ top ⊗ f1).
+Proof.
+  intros.
+  match goal with 
+  |- (?t ≃ ?t')%Cat => let mct := make_moncat_expr_debug t in print_moncat_expr_JSON mct
+    (* let mct' := make_moncat_expr_debug t' in pose mct' *)
+  end.
+  Admitted.
+
+Lemma print_test_1 : forall {C : Type}
+  {cC : Category C} {mC : MonoidalCategory cC}
+  {top botIn botMid botOut : C} 
+  (f0 : botIn ~> botMid) (f1 : botMid ~> botOut),
+  (id_ top) ⊗ (f0 ∘ f1) ∘ (λ_ _)^-1 ≃ id_ top ⊗ f0 ∘ (id_ top ⊗ f1) ∘ (λ_ _)^-1.
+Proof.
+  intros.
+  match goal with 
+  |- (?t ≃ ?t')%Cat => let mct := make_moncat_expr_debug t in pose mct;
+    let mct' := make_moncat_expr_debug t' in pose mct'
+  end.
+  Admitted.
diff --git a/ViCaR/Classes/RigCategory.v b/ViCaR/Classes/RigCategory.v
index 4558883..3ea7e2e 100644
--- a/ViCaR/Classes/RigCategory.v
+++ b/ViCaR/Classes/RigCategory.v
@@ -283,7 +283,7 @@ Definition condition_XV `{@BraidedMonoidalCategory DD cC MulC} :=
 
 
 
-(* 
+
 
 
 
@@ -887,7 +887,7 @@ Proof.
     rewrite e; clear e.
     Admitted.
 
-. *)
+.
 End CoherenceConditions.
 
 Class SemiCoherent_DistributiveBimonoidalCategory {DD : Type} {cC : Category DD}
diff --git a/ViCaR/MonoidalCoherence.v b/ViCaR/MonoidalCoherence.v
new file mode 100644
index 0000000..124fa77
--- /dev/null
+++ b/ViCaR/MonoidalCoherence.v
@@ -0,0 +1,1042 @@
+Require Import String.
+Require Import Psatz.
+Require Import CategoryTypeclass.
+Require Import Arith.
+
+Section BWord.
+
+Inductive W :=
+  | e0 : W
+  | var : W
+  | tens : W -> W -> W.
+
+Inductive W0 :=
+  | var0 : W0
+  | tens0 : W0 -> W0 -> W0.
+
+Fixpoint W_eqb (b b' : W) : bool :=
+  match b, b' with
+  | e0, e0 => true
+  | var, var => true
+  | tens b0 b1, tens b0' b1' => W_eqb b0 b0' && W_eqb b1 b1'
+  | _, _ => false
+  end.
+
+Fixpoint W0_eqb (b b' : W0) : bool :=
+  match b, b' with
+  | var0, var0 => true
+  | tens0 b0 b1, tens0 b0' b1' => W0_eqb b0 b0' && W0_eqb b1 b1'
+  | _, _ => false
+  end.
+
+
+
+Require Import Bool.
+
+Lemma W_eqbP : forall b b', b = b' <-> W_eqb b b' = true.
+Proof.
+  intros b b'.
+  split.
+  - intros H; subst b'; induction b; 
+    simpl; try apply andb_true_intro; easy.
+  - revert b'.
+    induction b;
+    intros b' H; destruct b'; try easy.
+    simpl in H.
+    rewrite andb_true_iff in H.
+    erewrite IHb1, IHb2 by apply H.
+    easy.
+Qed.
+
+Lemma W0_eqbP : forall b b', b = b' <-> W0_eqb b b' = true.
+Proof.
+  intros b b'.
+  split.
+  - intros H; subst b'; induction b; 
+    simpl; try apply andb_true_intro; easy.
+  - revert b'.
+    induction b;
+    intros b' H; destruct b'; try easy.
+    simpl in H.
+    rewrite andb_true_iff in H.
+    erewrite IHb1, IHb2 by apply H.
+    easy.
+Qed.
+
+Lemma bw_eq_dec : forall b b' : W, {b = b'} + {b <> b'}.
+Proof.
+  intros b b'.
+  destruct (W_eqb b b') eqn:e.
+  - rewrite <- W_eqbP in e.
+    left; exact e.
+  - right.
+    intros Heq.
+    rewrite (proj1 (W_eqbP b b') Heq) in e.
+    discriminate e.
+Qed.
+
+
+Fixpoint eval_W {A} (a : A) (zero : A) 
+  (bind : A -> A -> A) (b : W) : A :=
+  match b with
+  | e0 => zero
+  | var => a
+  | tens b0 b1 => 
+    bind (eval_W a zero bind b0) (eval_W a zero bind b0)
+  end.
+
+Fixpoint print_word (b : W) : string :=
+  match b with
+  | e0 => "e"%string
+  | var => "—"%string
+  | tens b0 b1 => 
+    ("(" ++ print_word b0 ++ ")⊗(" ++ print_word b1 ++ ")")%string
+  end.
+
+
+
+Fixpoint interp_W0 {C} {cC : Category C} {mC : MonoidalCategory cC}
+  (c : C) (b : W0) := 
+  match b with
+  | var0 => c
+  | tens0 b0 b1 => interp_W0 c b0 × interp_W0 c b1
+  end.
+
+End BWord.
+
+Section Associativity.
+
+Inductive aS :=
+  | as_W0 : W0 -> aS
+  | as_assoc : W0 -> W0 -> W0 -> aS
+  | as_invassoc : W0 -> W0 -> W0 -> aS
+  | as_tensor_l : aS -> W0 -> aS
+  | as_tensor_r : aS -> W0 -> aS.
+
+Fixpoint a_dom (s : aS) : W0 :=
+  match s with
+  | as_W0 b => b
+  | as_assoc u v w => tens0 u (tens0 v w)
+  | as_invassoc u v w => tens0 (tens0 u v) w
+  | as_tensor_l a b =>
+      tens0 b (a_dom a)
+  | as_tensor_r a b =>
+      tens0 (a_dom a) b
+  end.
+
+Fixpoint a_codom (s : aS) : W0 :=
+  match s with
+  | as_W0 b => b
+  | as_assoc u v w => tens0 (tens0 u v) w
+  | as_invassoc u v w => tens0 u (tens0 v w)
+  | as_tensor_l a b =>
+      tens0 b (a_codom a)
+  | as_tensor_r a b =>
+      tens0 (a_codom a) b
+  end.
+
+Fixpoint w_Sn (n : nat) : W0 :=
+  match n with
+  | 0 => var0
+  | S n' => tens0 (w_Sn n') var0
+  end.
+
+Fixpoint len0 (b : W0) : nat :=
+  match b with
+  | var0 => 1
+  | tens0 b0 b1 => len0 b0 + len0 b1
+  end.
+
+Lemma len0_pos : forall b, len0 b > 0.
+Proof. induction b; simpl; lia. Qed.
+
+Lemma len_w_Sn : forall n, len0 (w_Sn n) = S n.
+Proof.
+  induction n; simpl; lia.
+Qed.
+
+Fixpoint rho0 (b : W0) : nat :=
+  match b with
+  | var0 => 0
+  | tens0 v w => rho0 v + rho0 w + len0 w - 1
+  end.
+
+Lemma rho0_w_Sn : forall n, 
+  rho0 (w_Sn n) = 0.
+Proof.
+  induction n; simpl; lia.
+Qed.
+
+Lemma rho_eq0_iff : forall b : W0,
+  rho0 b = 0 <-> b = w_Sn (len0 b - 1).
+Proof.
+  intros b.
+  split.
+  - induction b; [easy|].
+    destruct b2.
+    + simpl in *.
+      intros.
+      assert (rho0 b1 = 0) by lia.
+      rewrite IHb1 at 1 by lia.
+      assert (H':len0 b1 > 0) by (apply len0_pos); revert H'.
+      generalize (len0 b1) as n.
+      intros n. 
+      induction n; [easy|].
+      intros _.
+      simpl; rewrite 2!Nat.sub_0_r, Nat.add_1_r.
+      easy.
+    + intros H.
+      contradict H.
+      simpl.
+      pose (len0_pos b2_1); pose (len0_pos b2_2).
+      lia.
+  - intros H; rewrite H.
+    apply rho0_w_Sn.
+Qed.
+
+Inductive a_dir : aS -> Prop :=
+  | a_dir_assoc u v w : a_dir (as_assoc u v w)
+  | a_dir_tens_l s b : a_dir s -> a_dir (as_tensor_l s b)
+  | a_dir_tens_r s b : a_dir s -> a_dir (as_tensor_r s b).
+
+Inductive a_antidir : aS -> Prop :=
+  | a_antidir_invassoc u v w : a_antidir (as_invassoc u v w)
+  | a_antidir_tens_l s b : a_antidir s -> a_antidir (as_tensor_l s b)
+  | a_antidir_tens_r s b : a_antidir s -> a_antidir (as_tensor_r s b).
+
+Lemma ne_tens0_l : forall b b' : W0,
+  b <> tens0 b b'.
+Proof.
+  intros b.
+  induction b; [easy|].
+  intros b' H.
+  inversion H.
+  eapply IHb1; eassumption.
+Qed.
+
+Lemma ne_tens0_r : forall b b' : W0,
+  b <> tens0 b' b.
+Proof.
+  intros b.
+  induction b; [easy|].
+  intros b' H.
+  inversion H.
+  eapply IHb2; eassumption.
+Qed.
+
+Lemma ne_tens0_assoc : forall b b' b'' : W0, 
+  tens0 (tens0 b b') b'' <> tens0 b (tens0 b' b'').
+Proof.
+  intros b.
+  induction b; [easy|].
+  intros b' b'' H; inversion H.
+  symmetry in H1.
+  eapply ne_tens0_l, H1.
+Qed.
+
+Ltac W0cong :=
+  simpl in *; subst; intros; try easy; try lia; first [
+    exfalso; eapply ne_tens0_r; solve [eauto] |
+    exfalso; eapply ne_tens0_l; solve [eauto] |
+    exfalso; eapply ne_tens0_assoc; solve [eauto] |
+    match goal with
+    | H : ?f _ _ = ?g _ _ |- _ => inversion H; clear H; W0cong
+    end |
+    match goal with
+    | H : forall _, _ |- _ => apply H; clear H; W0cong
+    end |
+    (progress f_equal); solve [eauto] |
+    (progress hnf); W0cong
+  ].
+
+Ltac W0cong_debug :=
+  simpl in *; subst; intros; try easy; try lia; first [
+    exfalso; eapply ne_tens0_r; idtac "ner"; solve [eauto] |
+    exfalso; eapply ne_tens0_l; idtac "nel"; solve [eauto] |
+    exfalso; eapply ne_tens0_assoc; idtac "nea"; solve [eauto] |
+    match goal with
+    | H : ?f _ _ = ?g _ _ |- _ => inversion H; 
+    idtac "invers" H; clear H; W0cong_debug
+    end |
+    match goal with
+    | H : forall _, _ |- _ => apply H; idtac "apply" H; clear H; W0cong_debug
+    end |
+    (progress f_equal); idtac "feq"; solve [eauto] |
+    (progress hnf); idtac "hnf"; W0cong_debug
+  ].
+
+Hint Resolve ne_tens0_r ne_tens0_l ne_tens0_assoc : tens0_db.
+
+Lemma a_dir_not_id : forall s : aS, a_dir s -> a_dom s <> a_codom s.
+Proof.
+  intros s Hs.
+  induction Hs; W0cong.
+Qed.
+
+Lemma a_dir_len_dom_codom : forall s : aS, 
+  a_dir s ->
+  len0 (a_dom s) = len0 (a_codom s).
+Proof.
+  intros s Hs; induction Hs; simpl; auto with arith.
+Qed.
+
+Lemma a_no_parallel_dir : forall s s' : aS,
+  a_dir s -> a_dir s' ->
+  a_dom s = a_dom s' -> a_codom s = a_codom s' -> s = s'.
+Proof.
+  intros s s' Hs Hs'; revert s' Hs'.
+  induction Hs.
+  - simpl; intros s' Hs'; inversion Hs'; W0cong.
+  - simpl. intros s' Hs'.
+    inversion Hs'; try W0cong.
+    pose proof a_dir_not_id.
+    simpl.
+    intros.
+    subst.
+    inversion H2; inversion H3.
+    exfalso; eapply H1; eauto; subst; easy.
+  - simpl. intros s' Hs'.
+    inversion Hs'; try W0cong.
+    pose proof a_dir_not_id.
+    simpl.
+    intros.
+    subst.
+    inversion H2; inversion H3.
+    exfalso; eapply H1; eauto; subst; easy.
+Qed.
+
+Lemma rho0_dir_decreasing : forall s, 
+  a_dir s ->
+  rho0 (a_codom s) < rho0 (a_dom s).
+Proof.
+  intros s Hs.
+  induction Hs.
+  - simpl.
+    pose (len0_pos u); 
+    pose (len0_pos v);
+    pose (len0_pos w).
+    lia.
+  - simpl. 
+    pose (len0_pos (a_dom s)).
+    rewrite <- a_dir_len_dom_codom by easy.
+    lia.
+  - simpl.
+    pose (len0_pos b).
+    lia.
+Qed.
+
+Fixpoint a_inv (s : aS) : aS :=
+  match s with
+  | as_W0 b => as_W0 b
+  | as_assoc u v w => as_invassoc u v w
+  | as_invassoc u v w => as_assoc u v w
+  | as_tensor_l a b => as_tensor_l (a_inv a) b
+  | as_tensor_r a b => as_tensor_r (a_inv a) b
+  end.
+
+Lemma a_inv_involutive : forall s, 
+  a_inv (a_inv s) = s.
+Proof. induction s; simpl; rewrite ?IHs; easy. Qed.
+
+Lemma a_inv_dom : forall s,
+  a_dom (a_inv s) = a_codom s.
+Proof. induction s; simpl; rewrite ?IHs; easy. Qed.
+
+Lemma a_inv_codom : forall s,
+  a_codom (a_inv s) = a_dom s.
+Proof. induction s; simpl; rewrite ?IHs; easy. Qed.
+
+Lemma a_inv_dir : forall s, 
+  a_dir s -> a_antidir (a_inv s).
+Proof.
+  intros s Hs.
+  induction Hs; constructor; assumption.
+Qed.
+
+Lemma a_inv_antidir : forall s, 
+  a_antidir s -> a_dir (a_inv s).
+Proof.
+  intros s Hs.
+  induction Hs; constructor; assumption.
+Qed.
+
+
+Inductive a_lst :=
+  | a_lst_init : aS -> a_lst
+  | a_lst_cons : aS -> a_lst -> a_lst.
+
+Definition a_lst_dom (ls : a_lst) : W0 :=
+  match ls with
+  | a_lst_init s
+  | a_lst_cons s _ => a_dom s
+  end.
+
+Fixpoint a_lst_codom (ls : a_lst) : W0 :=
+  match ls with
+  | a_lst_init s => a_codom s
+  | a_lst_cons _ l => a_lst_codom l
+  end.
+
+Fixpoint a_path (ls : a_lst) : bool :=
+  match ls with
+  | a_lst_init s => true
+  | a_lst_cons s l => W0_eqb (a_codom s) (a_lst_dom l) && a_path l
+  end.
+
+Fixpoint a_path_prop (ls : a_lst) : Prop :=
+  match ls with
+  | a_lst_init s => True
+  | a_lst_cons s l => (a_codom s) = (a_lst_dom l) /\ a_path_prop l
+  end.
+
+Fixpoint assoc_free (b : W0) : bool :=
+  match b with 
+  | var0 => true
+  | tens0 b' b'' => match b'' with
+    | var0 => assoc_free b'
+    | tens0 _ _ => false
+    end
+  end.
+
+Lemma assoc_free_iff_rho0_eq_0 : forall b, 
+  assoc_free b = true <-> rho0 b = 0.
+Proof.
+  intros b.
+  rewrite rho_eq0_iff.
+  split.
+  - intros H.
+    induction b; [easy|].
+    simpl in H.
+    destruct b2; [|easy].
+    simpl.
+    rewrite Nat.add_sub.
+    rewrite IHb1 at 1 by easy.
+    pose proof (len0_pos b1) as e ; revert e.
+    generalize (len0 b1) as n; induction n; [easy|].
+    intros _.
+    simpl; rewrite Nat.sub_0_r; easy.
+  - generalize (len0 b).
+    intros n Hb; subst b.
+    destruct n; [easy|].
+    simpl; rewrite Nat.sub_0_r.
+    induction n; easy.
+Qed.
+
+Fixpoint a_can_next_step (b : W0) : aS :=
+  match b with
+  | var0 => as_W0 var0
+  | tens0 c d => match d with
+    | var0 => as_tensor_r (a_can_next_step c) var0
+    | tens0 d' d'' => as_assoc c d' d''
+    end 
+  end.
+
+Lemma a_can_next_step_dom : forall b, 
+  a_dom (a_can_next_step b) = b.
+Proof.
+  intros b; induction b; [easy|]; simpl.
+  induction b2; [|easy].
+  simpl; rewrite IHb1; easy.
+Qed.
+
+Lemma a_can_next_step_dir : forall b,
+  rho0 b <> 0 ->
+  a_dir (a_can_next_step b).
+Proof.
+  intros b H.
+  induction b as [|b0 b1]; [easy|].
+  intros. simpl.
+  destruct b2; constructor.
+  apply b1.
+  simpl in H.
+  lia.
+Qed.
+
+Lemma rho0_a_can_next_step_codom : forall b,
+  assoc_free b = false ->
+  rho0 (a_codom (a_can_next_step b)) < rho0 b.
+Proof.
+  intros.
+  rewrite <- (a_can_next_step_dom b) at 2.
+  apply rho0_dir_decreasing, a_can_next_step_dir.
+  rewrite <- assoc_free_iff_rho0_eq_0.
+  rewrite H; easy.
+Qed.
+
+Require Coq.Program.Wf.
+Require Import FunInd Recdef.
+
+Function a_can_path (b : W0) {measure rho0 b} : a_lst :=
+  match assoc_free b as H with
+  | true => a_lst_init (as_W0 b)
+  | false =>
+    let cns := a_can_next_step b in 
+    a_lst_cons (cns) (a_can_path (a_codom cns))
+  end.
+apply rho0_a_can_next_step_codom.
+Qed.
+
+
+(* Function a_can_path (b : W0) {measure (rho0 b)} : a_lst :=
+  match assoc_free b as H with
+  | true => a_lst_init (as_W0 b)
+  | false =>
+    let cns := a_can_next_step b in 
+    a_lst_cons (cns) (a_can_path (a_codom cns))
+  end.
+Next Obligation.
+  apply rho0_a_can_next_step_codom; easy.
+Qed. *)
+
+Lemma a_can_path_dom : forall b, a_lst_dom (a_can_path b) = b.
+Proof.
+  intros b.
+  pattern (a_can_path b).
+  revert b.
+  apply a_can_path_ind; [easy|].
+  intros b Hb.
+  simpl.
+  intros _.
+  apply a_can_next_step_dom.
+Qed.
+
+Lemma a_can_path_codom_rho0 : forall b, 
+  rho0 (a_lst_codom (a_can_path b)) = 0.
+Proof.
+  intros b;
+  pattern (a_can_path b);
+  revert b.
+  apply a_can_path_ind; [|easy].
+  intros b Hb.
+  rewrite assoc_free_iff_rho0_eq_0 in Hb.
+  easy.
+Qed.
+
+Lemma a_can_next_step_codom_len : forall b,
+  len0 (a_codom (a_can_next_step b)) = len0 b.
+Proof.
+  induction b; [easy|].
+  simpl.
+  destruct b2; simpl; lia.
+Qed.
+
+Lemma a_can_path_codom_len : forall b,
+  len0 (a_lst_codom (a_can_path b)) = len0 b.
+Proof.
+  intros b; 
+  pattern (a_can_path b);
+  revert b.
+  apply a_can_path_ind; [easy|].
+  simpl; intros.
+  rewrite <- (a_can_next_step_codom_len b).
+  easy.
+Qed.
+
+Lemma a_can_path_codom : forall b, 
+  a_lst_codom (a_can_path b) = w_Sn (len0 b - 1).
+Proof.
+  intros b.
+  pose proof (a_can_path_codom_rho0 b) as H.
+  rewrite rho_eq0_iff in H.
+  rewrite H, a_can_path_codom_len.
+  easy.
+Qed.
+
+Lemma a_can_path_path : forall b, a_path_prop (a_can_path b).
+Proof.
+  apply a_can_path_ind.
+  - easy.
+  - intros b Hb.
+    simpl.
+    intros Hpath; split; [|easy].
+    rewrite a_can_path_dom.
+    easy.
+Qed.
+
+
+
+Fixpoint interp_aS {C} {cC : Category C} {mC : MonoidalCategory cC}
+  (c : C) (s : aS) 
+  : cC.(morphism) (interp_W0 c (a_dom s)) (interp_W0 c (a_codom s)) :=
+  match s with
+  | as_W0 b => id_ _
+  | as_assoc u v w => (associator _ _ _)^-1
+  | as_invassoc u v w => (associator _ _ _)
+  | as_tensor_l a b => (id_ _) ⊗ (interp_aS c a)
+  | as_tensor_r a b => (interp_aS c a) ⊗ (id_ _)
+  end%Mor.
+
+Fixpoint a_dir_lst (l : a_lst) : Prop :=
+  match l with
+  | a_lst_init s => a_dir s
+  | a_lst_cons s ls => a_dir s /\ a_dir_lst ls
+  end.
+
+Definition a_dir_path (l : a_lst) := a_path_prop l /\ a_dir_lst l.
+
+Fixpoint interp_a_path_prop {C} {cC : Category C}
+  {mC : MonoidalCategory cC} (c : C) (l : a_lst) 
+  (H : a_path_prop l) {struct l} : 
+  (interp_W0 c (a_lst_dom l) ~> interp_W0 c (a_lst_codom l))%Cat.
+destruct l.
+- apply interp_aS.
+- simpl.
+  eapply compose.
+  + apply interp_aS.
+  + destruct H as [Ha Hl].
+    rewrite Ha.
+    apply interp_a_path_prop, Hl.
+Defined.
+
+Definition unique_directed_path_image_prop : Prop.
+  refine ( forall C (cC : Category C)
+  (mC : MonoidalCategory cC) (c : C) (v : W0) (l l' : a_lst)
+    (Hl : a_dir_path l) (Hl' : a_dir_path l')
+    (Hdoml : a_lst_dom l = v) (Hdoml' : a_lst_dom l' = v)
+    (Hcodoml : a_lst_codom l = w_Sn (len0 v - 1))
+    (Hcodoml' : a_lst_codom l' = w_Sn (len0 v - 1)),
+    (interp_a_path_prop c l (proj1 Hl) ≃ _)%Cat).
+  rewrite Hdoml, <- Hdoml', Hcodoml, <- Hcodoml'.
+  exact (interp_a_path_prop c l' (proj1 Hl')).
+Defined.
+
+Lemma generalized_induction {T} {P : T -> Prop} 
+  (f : T -> nat) : 
+  (forall t, f t = 0 -> P t) ->
+  (forall t, (forall s, f s < f t -> P s) -> P t) ->
+  forall t, P t.
+Proof.
+  intros Hbase Hrec.
+  enough (Hen: forall n, forall t, f t <= n -> P t)
+  by (intros t; apply (Hen (f t) t (le_n _))).
+  intros n.
+  induction n.
+  - intros t Hft.
+    apply Hbase; lia.
+  - intros t Hft.
+    destruct (Nat.lt_trichotomy (f t) (S n)) 
+      as [Hlt | [Heq | Hfalse]]; [| | lia].
+    + apply IHn; lia.
+    + apply Hrec. 
+      intros s Hs.
+      apply IHn; lia.
+Qed.
+
+Lemma generalized_induction_base {T} {P : T -> Prop} 
+  (f : T -> nat) (base : nat) : 
+  (forall t, f t <= base -> P t) ->
+  (forall t, (forall s, f s < f t -> P s) -> P t) ->
+  forall t, P t.
+Proof.
+  intros Hbase Hrec.
+  apply (generalized_induction (fun t => f t - base)).
+  - intros t Ht; apply Hbase; lia.
+  - intros t Hless.
+    apply Hrec.
+    intros s Hs.
+    destruct (Nat.lt_trichotomy (f s) base) as [Hlt | [Heq | Hgt]];
+    [apply Hbase; lia | apply Hbase; lia |].
+    apply Hless; lia.
+Qed.
+
+Require Import Coq.Init.Wf.
+
+Lemma generalized_double_induction {T} {P : T -> Prop} 
+  (f g : T -> nat) : 
+  (forall t, f t = 0 -> P t) ->
+  (forall t, g t = 0 -> P t) ->
+  (forall t, 
+    (forall s, f s = f t -> g s < g t -> P s) ->
+    (forall s, f s < f t -> P s) -> P t) ->
+  forall t, P t.
+Proof.
+
+  intros Hbasef Hbaseg Hrec.
+  enough (Hpair:forall s t : T, P s /\ P t) by 
+  (intros t; apply (Hpair t t)).
+  set (lexico_rel (* : nat * nat -> nat * nat -> Prop *) :=
+    fun ab cd :nat*nat=> let (a,b) := ab in let (c,d):=cd in
+      a < c \/ (a = c /\ b < d)).
+  intros s t; pattern t; revert t; pattern s; revert s.
+  apply well_founded_induction_type_2 with lexico_rel.
+  - intros (a, b).
+    induction a; induction b.
+    + constructor.
+      intros (c, d) Hy; unfold lexico_rel in *.
+      lia.
+    + constructor.
+      intros (c, d).
+      intros [Hfalse | [Hc Hd]]; [unfold lexico_rel in *; lia|]. subst c.
+      destruct (Nat.lt_trichotomy d b) as [Hlt | [Heq | Hf]];
+      [ | | lia].
+      * apply Acc_inv with (0, b). 
+        apply IHb.
+        hnf; lia.
+      * subst d; easy. 
+    + constructor.
+      intros (a', b').
+      unfold lexico_rel.
+      intros [Ha' | Hf]; [|lia].
+      destruct (Nat.lt_trichotomy a' a) as [Hlt | [Heq | Hf]];
+      [ | | lia].
+      * apply Acc_inv with (a, 0); easy || lia.
+      * subst a'.
+        induction b'; [easy|].
+        constructor.
+        intros (a'', b'').
+        intros [Has | [Haeq Hb]];
+        [ apply Acc_inv with (a, b'); easy || lia | ].
+        subst a''.
+        destruct (Nat.lt_trichotomy b'' b') as [Hlt | [Heq | Hf]];
+        [ | | lia].
+        --apply Acc_inv with (a, b'); easy || lia.
+        --subst b''; easy.
+    + specialize (IHb ltac:(apply Acc_inv with (a, S b); hnf; easy || lia)).
+      constructor.
+      intros (c, d).
+      intros [Halt | [Haeq Hblt]].
+      * apply Acc_inv with (S a, b); hnf; easy || lia.
+      * subst c. 
+        induction d.
+        --destruct b; [easy|].
+          apply Acc_inv with (S a, S b); hnf; easy || lia.
+        --constructor.
+          intros (c', d').
+          intros [Hclt | [Hceq Hdlt]].
+          ++apply Acc_inv with (S a, b); hnf; easy || lia.
+          ++destruct (Nat.lt_trichotomy d' d) as [Hlt | [Heq | Hf]];
+            [ | | lia].
+            **apply Acc_inv with (S a, d); hnf; apply IHd || lia; lia.
+            **subst; apply IHd; lia.
+  - intros x x' Hind.
+    Abort.
+
+
+Lemma unique_directed_path_image : unique_directed_path_image_prop.
+Proof.
+  unfold unique_directed_path_image_prop.
+  intros C cC mC c v.
+  pattern v.
+  match goal with |- ?f ?v => set (gP := f) end.
+  assert (HwSn: forall w, (exists n, w = w_Sn n) -> gP w). 1:{
+    subst gP.
+    intros w [n Hn].
+    subst w.
+    intros.
+    unfold a_dir_path in Hl.
+    destruct l.
+    + simpl in *.
+      pose proof (rho0_dir_decreasing a (proj2 Hl)) as H.
+      replace (a_dom a) in H.
+      rewrite rho0_w_Sn in H.
+      easy.
+    + simpl in *.
+      pose proof (rho0_dir_decreasing a (proj1 (proj2 Hl))) as H.
+      replace (a_dom a) in H.
+      rewrite rho0_w_Sn in H; easy.
+  }
+  apply (generalized_induction rho0).
+  - intros t.
+    rewrite rho_eq0_iff.
+    intros Ht.
+    apply HwSn.
+    exists (len0 t - 1); easy.
+  - intros t;
+    pattern t; revert t.
+    apply (generalized_induction_base len0 1).
+    + intros t Ht.
+      destruct t; try (simpl in Ht; lia).
+      * intros _.
+        apply HwSn.
+        exists 0; easy.
+      * simpl in Ht.
+        pose (len0_pos t1); pose (len0_pos t2); lia.
+    + 
+  
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+  Search "a_can_path".
+  apply (generalized_induction rho0).
+  - intros b Hb.
+    
+    destruct (assoc_free b).
+  
+  Search "a_can_path".
+  
+
+
+
+
+
+
+Inductive arrow_S' :=
+  | arr_W (b : W)
+  | arr_assoc (u v w : W)
+  | arr_invassoc (u v w : W)
+  | arr_lunit (b : W)
+  | arr_invlunit (b : W)
+  | arr_runit (b : W)
+  | arr_invrunit (b : W)
+  | arr_tensor_l : arrow_S' -> W -> arrow_S'
+  | arr_tensor_r : arrow_S' -> W -> arrow_S'.
+
+Class Quiver := {
+  q_edges : Type;
+  q_verts : Type;
+  dom : q_edges -> q_verts;
+  codom : q_edges -> q_verts;
+}.
+
+Fixpoint arrow_dom (a : arrow_S') : W :=
+  match a with
+  | arr_W b => b
+  | arr_assoc u v w => tens (tens u v) w
+  | arr_invassoc u v w => tens u (tens v w)
+  | arr_lunit b => tens e0 b
+  | arr_invlunit b => b
+  | arr_runit b => tens b e0
+  | arr_invrunit b => b
+  | arr_tensor_l a b =>
+      tens b (arrow_dom a)
+  | arr_tensor_r a b =>
+      tens (arrow_dom a) b
+  end.
+
+Fixpoint arrow_codom (a : arrow_S') : W :=
+  match a with
+  | arr_W b => b
+  | arr_assoc u v w => tens u (tens v w)
+  | arr_invassoc u v w => tens (tens u v) w
+  | arr_lunit b => b
+  | arr_invlunit b => tens e0 b
+  | arr_runit b => b
+  | arr_invrunit b => tens b e0
+  | arr_tensor_l s b =>
+      tens b (arrow_codom s)
+  | arr_tensor_r s b =>
+      tens (arrow_codom s) b
+  end.
+
+#[export] Instance quiver_S' : Quiver := {
+  q_edges := arrow_S';
+  q_verts := W;
+  dom := arrow_dom;
+  codom := arrow_codom;
+}.
+
+Fixpoint len (b : W) : nat :=
+  match b with
+  | e0 => 0
+  | var => 1
+  | tens b0 b1 => len b0 + len b1
+  end.
+
+Lemma len_dom_codom : forall s,
+  len (arrow_dom s) = len (arrow_codom s).
+Proof.
+  induction s; simpl; lia.
+Qed.
+
+
+Fixpoint word_to_mc {C} {cC : Category C} (mC : MonoidalCategory cC) 
+  (b : W) : C -> C :=
+  fun c => 
+  match b with
+  | e0 => mC.(mon_I)
+  | var => c
+  | tens b0 b1 => (word_to_mc mC b0 c) × (word_to_mc mC b1 c)
+  end.
+
+
+(* Local Open Scope Mor_scope. *)
+Fixpoint arr_to_mc {C} {cC : Category C} (mC : MonoidalCategory cC) 
+  (s : arrow_S') (c : C) : 
+    ((word_to_mc mC (arrow_dom s) c) ~> 
+      (word_to_mc mC (arrow_codom s) c))%Cat :=
+  match s with 
+  | arr_W b => id_ _
+  | arr_assoc u v w => 
+      associator (word_to_mc mC u c) (word_to_mc mC v c) (word_to_mc mC w c)
+  | arr_invassoc u v w =>
+      (associator (word_to_mc mC u c) (word_to_mc mC v c) (word_to_mc mC w c))^-1
+  | arr_lunit b => 
+      λ_ _
+  | arr_invlunit b => (λ_ _)^-1
+  | arr_runit b => (ρ_ _)
+  | arr_invrunit b => (ρ_ _)^-1
+  | arr_tensor_l s' b =>
+      id_ (word_to_mc mC b c) ⊗ (arr_to_mc mC s' c)
+  | arr_tensor_r s' b =>
+      (arr_to_mc mC s' c) ⊗ id_ (word_to_mc mC b c)
+  end%Mor.
+
+Inductive arr_lst :=
+  | lst_init : arrow_S' -> arr_lst
+  | lst_cons : arrow_S' -> arr_lst -> arr_lst.
+
+Definition arr_lst_dom (ls : arr_lst) : W :=
+  match ls with
+  | lst_init s
+  | lst_cons s _ => dom s
+  end.
+
+Fixpoint arr_lst_codom (ls : arr_lst) : W :=
+  match ls with
+  | lst_init s => codom s
+  | lst_cons _ l => arr_lst_codom l
+  end.
+
+Fixpoint arr_path (ls : arr_lst) : bool :=
+  match ls with
+  | lst_init s => true
+  | lst_cons s l => W_eqb (codom s) (arr_lst_dom l) && arr_path l
+  end.
+
+Fixpoint arr_path_prop (ls : arr_lst) : Prop :=
+  match ls with
+  | lst_init s => True
+  | lst_cons s l => (codom s) = (arr_lst_dom l) /\ arr_path_prop l
+  end.
+
+Lemma arr_lst_pathP (ls : arr_lst) : 
+  arr_path_prop ls <-> arr_path ls = true.
+Proof.
+  induction ls; [easy|].
+  - simpl.
+    rewrite andb_true_iff, W_eqbP.
+    split; intros []; split; easy || apply IHls; easy.
+Qed.
+
+Definition morphism_of_arr_path {C} {cC : Category C} (mC : MonoidalCategory cC)
+  (c : C) (ls : arr_lst) (H : arr_path_prop ls) : 
+    (word_to_mc mC (arr_lst_dom ls) c ~> word_to_mc mC (arr_lst_codom ls) c)%Cat.
+induction ls.
+- apply arr_to_mc.
+- eapply compose.
+  + apply arr_to_mc.
+  + simpl in H. rewrite (proj1 H).
+    apply IHls, H.
+Defined.
+
+  
+
+Definition coherence_theorem_v1 : Prop.
+refine (
+  forall {C} {cC : Category C} (mC : MonoidalCategory cC) (c : C)
+  (v w : W) (Hlen : len v = len w) (ls ls' : arr_lst) 
+  (Hls : arr_path_prop ls) (Hls' : arr_path_prop ls')
+  (Hdom : arr_lst_dom ls = arr_lst_dom ls') 
+  (Hcodom : arr_lst_codom ls = arr_lst_codom ls'),
+  _ : Prop).
+pose (morphism_of_arr_path mC c ls Hls) as morls;
+pose (morphism_of_arr_path mC c ls' Hls') as morls'.
+rewrite Hdom, Hcodom in morls.
+exact (morls ≃ morls')%Cat.
+Defined.
+
+Section VersionTwo.
+
+Require Import Arith.
+
+#[export, program] Instance WordCat : Category W := {
+  morphism := fun b b' => if len b =? len b' then True else False;
+  c_equiv := fun b b' f f' => True;
+  compose := fun b b' b'' f g => _;
+}.
+Next Obligation.
+  split; destruct (len A =? len B); easy.
+Qed.
+Next Obligation.
+  destruct (len b =? len b') eqn:e.
+  - rewrite Nat.eqb_eq in e.
+    rewrite e.
+    apply g.
+  - destruct f.
+Defined.
+Next Obligation.
+  rewrite Nat.eqb_refl.
+  exact Logic.I.
+Defined.
+
+Local Open Scope Cat_scope.
+
+
+Context {C : Type} {cC : Category C} {D : Type} {cD : Category D}.
+
+Class StrictMonoidalFunctor 
+  (mC : MonoidalCategory cC) (mD : MonoidalCategory cD) : Type := {
+  strict_functor : Functor cC cD;
+  mon_I_eq : strict_functor I = I;
+  tensor_eq (c c' : C) : 
+    strict_functor (c × c') = strict_functor c × strict_functor c';
+  mon_mu_ij (i j : C) : 
+  strict_functor i × strict_functor j <~> strict_functor (i × j) := 
+    eq_rect_r (fun d : D => strict_functor i × strict_functor j <~> d) 
+    (IdentityIsomorphism (strict_functor i × strict_functor j))
+    (tensor_eq i j);
+  mon_eps : I <~> strict_functor I :=
+    eq_rect_r (fun d : D => I <~> d)
+    (IdentityIsomorphism I)
+    mon_I_eq;
+}.
+
+Coercion strict_functor : StrictMonoidalFunctor >-> Functor.
+
+Context {mC : MonoidalCategory cC} {mD : MonoidalCategory cD}.
+
+(* Definition mu_ij (F : StrictMonoidalFunctor mC mD) : forall (i j : C),
+F i × F j <~> F (i × j).
+intros.
+rewrite tensor_eq.
+apply IdentityIsomorphism.
+Defined. *)
+
+Lemma strict_monoidal_functor_assoc (F : StrictMonoidalFunctor mC mD)
+  : forall (x y z : C), 
+  associator (F x) (F y) (F z) ∘ id_ (F x) ⊗ mon_mu_ij y z ∘ mon_mu_ij x (y × z)
+  ≃ 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.
+
+
+
+
+
+  
diff --git a/examples/RelationsExample.v b/examples/RelationsExample.v
index 7ad995d..4ab462d 100644
--- a/examples/RelationsExample.v
+++ b/examples/RelationsExample.v
@@ -1,6 +1,6 @@
 Require Import Setoid.
 Require Import Logic.
-Require Import Basics.
+Require Import Basics (flip).
 From ViCaR Require Export CategoryTypeclass.
 From ViCaR Require Import RigCategory.
 
@@ -122,7 +122,7 @@ Ltac __solve_relations_end :=
 Ltac solve_relations := idtac. (* Hack to allow "mutual recursion" *)
 
 Ltac __setup_solve_relations :=
-  simpl; unfold unitary; simpl;
+  simpl;
   unfold compose_relns, reln_equiv, idn, reln_sum, 
     reln_prod, reln_unit, flip in *;
   simpl.
@@ -205,6 +205,9 @@ Ltac solve_relations ::=
   __solve_relations_end || __solve_relations_end_forward.
 (* End tactics *)
 
+Obligation Tactic := (hnf; solve_relations).
+Unset Program Cases.
+
 Lemma reln_equiv_refl {A B : Type} (f : reln A B) :
   f ~ f.
 Proof. easy. Qed.
@@ -290,7 +293,7 @@ Qed.
   morphism_bicompat := @prod_compat;
 }.
 
-#[export] Instance RelAssociator {A B C : Type} : 
+#[export, program] Instance RelAssociator {A B C : Type} : 
   Isomorphism (A * B * C) (A * (B * C)) := {
   forward := fun ab_c a_bc =>
     match ab_c with ((a, b), c) => 
@@ -302,39 +305,31 @@ Qed.
     match a_bc with (a',(b',c')) =>
       a = a' /\ b = b' /\ c = c'
     end end;
-  isomorphism_inverse := ltac:(abstract(solve_relations));
 }.
 
 (* Set Printing Universes. *)
 
-#[export] Instance RelLeftUnitor {A : Type} :
+#[export, program] Instance RelLeftUnitor {A : Type} :
   @Isomorphism Type Rel (⊤ * A) (A) := {
   forward := fun topa b => match topa with (_, a) => a = b end;
   reverse := fun a topb => match topb with (_, b) => a = b end;
-  isomorphism_inverse := ltac:(abstract(solve_relations))
 }.
 
-#[export] Instance RelRightUnitor {A : Type} :
+#[export, program] Instance RelRightUnitor {A : Type} :
   @Isomorphism Type Rel (A * ⊤) (A) := {
   forward := fun atop b => match atop with (a, _) => a = b end;
   reverse := fun a btop => match btop with (b, _) => a = b end;
-  isomorphism_inverse := ltac:(abstract(solve_relations))
 }.
 
-#[export] Instance RelMonoidal : MonoidalCategory Type | 0 := {
+#[export, program] Instance RelMonoidal : MonoidalCategory Rel | 0 := {
   tensor := ProductRelation;
-	I := ⊤;
+	mon_I := ⊤;
   associator := @RelAssociator;
   left_unitor := @RelLeftUnitor;
   right_unitor := @RelRightUnitor;
-  associator_cohere := ltac:(abstract(solve_relations));
-  left_unitor_cohere := ltac:(abstract(solve_relations));
-  right_unitor_cohere := ltac:(abstract(solve_relations));
-  triangle := ltac:(abstract(solve_relations));
-  pentagon := ltac:(abstract(solve_relations));
 }.
 
-#[export] Instance RelBraidingIsomorphism {A B} : 
+#[export, program] Instance RelBraidingIsomorphism {A B} : 
   Isomorphism (A * B) (B * A) := {
   forward := fun ab ba' => match ab with (a, b) => match ba' with (b', a') =>
     a = a' /\ b = b'
@@ -342,47 +337,35 @@ Qed.
   reverse := fun ba ab' => match ba with (b, a) => match ab' with (a', b') => 
     a = a' /\ b = b'
     end end;
-  isomorphism_inverse := ltac:(abstract(solve_relations))
 }.
 
-#[export] Instance RelBraiding : 
+#[export, program] Instance RelBraiding : 
   NaturalBiIsomorphism ProductRelation (CommuteBifunctor ProductRelation) := {
   component_biiso := @RelBraidingIsomorphism;
-  component_biiso_natural := ltac:(abstract(solve_relations))
 }.
 
-#[export] Instance RelBraidedMonoidal : BraidedMonoidalCategory Type | 0 := {
+#[export, program] Instance RelBraidedMonoidal 
+  : BraidedMonoidalCategory RelMonoidal | 0 := {
   braiding := RelBraiding;
-  hexagon_1 := ltac:(abstract(solve_relations));
-  hexagon_2 := ltac:(abstract(solve_relations));
 }.
 
-#[export] Instance RelSymmetricMonoidal : 
-  SymmetricMonoidalCategory Type | 0 := {
-  symmetry := ltac:(abstract(solve_relations));
+#[export, program] Instance RelSymmetricMonoidal : 
+  SymmetricMonoidalCategory RelBraidedMonoidal | 0 := {
 }.
 
-#[export] Instance RelCompactClosed : CompactClosedCategory Type := {
+#[export, program] Instance RelCompactClosed 
+  : CompactClosedCategory RelSymmetricMonoidal := {
   dual := fun A => A;
   unit := @reln_unit;
   counit := fun A => flip reln_unit;
-  triangle_1 := ltac:(abstract(solve_relations));
-  triangle_2 := ltac:(abstract(solve_relations));
 }.
 
-#[export] Instance RelDagger : DaggerCategory Type := {
+#[export, program] Instance RelDagger : DaggerCategory Rel := {
   adjoint := fun A B => @flip A B Prop;
-  adjoint_involutive := ltac:(easy);
-  adjoint_id := ltac:(easy);
-  adjoint_contravariant := ltac:(abstract(solve_relations));
-  adjoint_compat := ltac:(abstract(solve_relations));
 }.
 
-#[export] Instance RelDaggerMonoidal : DaggerMonoidalCategory Type := {
-  dagger_tensor_compat := ltac:(abstract(solve_relations));
-  associator_unitary := ltac:(abstract(solve_relations));
-  left_unitor_unitary := ltac:(abstract(solve_relations));
-  right_unitor_unitary := ltac:(abstract(solve_relations));
+#[export, program] Instance RelDaggerMonoidal 
+  : DaggerMonoidalCategory RelDagger RelMonoidal := {
 }.
 
 
@@ -400,15 +383,14 @@ Proof.
   solve_relations.
 Qed.
   
-#[export] Instance SumRelation : Bifunctor Rel Rel Rel := {
+#[export, program] Instance SumRelation : Bifunctor Rel Rel Rel := {
   obj_bimap := sum;
   morphism_bimap := @reln_sum;
   id_bimap := @sum_idn;
   compose_bimap := @sum_compose;
-  morphism_bicompat := ltac:(abstract(solve_relations));
 }.
 
-#[export] Instance RelSumAssociator {A B C : Type} : 
+#[export, program] Instance RelSumAssociator {A B C : Type} : 
   Isomorphism (A + B + C) (A + (B + C)) := {
   forward := fun ab_c a_bc =>
     match ab_c, a_bc with 
@@ -424,11 +406,10 @@ Qed.
     | inr c, inr (inr c') => c = c'
     | _, _ => False
     end;
-  isomorphism_inverse := ltac:(abstract(solve_relations));
 }.
 
 
-#[export] Instance RelSumLeftUnitor {A : Type} :
+#[export, program] Instance RelSumLeftUnitor {A : Type} :
   @Isomorphism Type Rel (⊥ + A) (A) := {
   forward := fun bota b => match bota with
     | inr a => a = b
@@ -437,10 +418,9 @@ Qed.
   reverse := fun a botb => match botb with 
     | inr b => a = b 
     | _ => False end;
-  isomorphism_inverse := ltac:(abstract(solve_relations))
 }.
 
-#[export] Instance RelSumRightUnitor {A : Type} :
+#[export, program] Instance RelSumRightUnitor {A : Type} :
   @Isomorphism Type Rel (A + ⊥) (A) := {
   forward := fun bota b => match bota with
     | inl a => a = b
@@ -449,23 +429,17 @@ Qed.
   reverse := fun a botb => match botb with 
     | inl b => a = b 
     | _ => False end;
-  isomorphism_inverse := ltac:(abstract(solve_relations))
 }.
 
-#[export] Instance RelSumMonoidal : MonoidalCategory Type | 10 := {
+#[export, program] Instance RelSumMonoidal : MonoidalCategory Rel | 10 := {
   tensor := SumRelation;
-	I := ⊥;
+	mon_I := ⊥;
   associator := @RelSumAssociator;
   left_unitor := @RelSumLeftUnitor;
   right_unitor := @RelSumRightUnitor;
-  associator_cohere := ltac:(abstract(solve_relations));
-  left_unitor_cohere := ltac:(abstract(solve_relations));
-  right_unitor_cohere := ltac:(abstract(solve_relations));
-  triangle := ltac:(abstract(solve_relations));
-  pentagon := ltac:(abstract(solve_relations));
 }.
 
-#[export] Instance RelSumBraidingIsomorphism {A B} : 
+#[export, program] Instance RelSumBraidingIsomorphism {A B} : 
   Isomorphism (A + B) (B + A) := {
   forward := fun ab ba' => 
     match ab, ba' with
@@ -479,26 +453,20 @@ Qed.
     | inl b, inr b' => b = b'
     | _, _ => False
     end;
-  isomorphism_inverse := ltac:(abstract(solve_relations))
 }.
 
-#[export] Instance RelSumBraiding : 
+#[export, program] Instance RelSumBraiding : 
   NaturalBiIsomorphism SumRelation (CommuteBifunctor SumRelation) := {
   component_biiso := @RelSumBraidingIsomorphism;
-  component_biiso_natural := ltac:(abstract(solve_relations))
 }.
 
-#[export] Instance RelSumBraidedMonoidal : 
-  @BraidedMonoidalCategory Type Rel RelSumMonoidal | 10 := {
+#[export, program] Instance RelSumBraidedMonoidal : 
+  BraidedMonoidalCategory RelSumMonoidal | 10 := {
   braiding := RelSumBraiding;
-  hexagon_1 := ltac:(abstract(solve_relations));
-  hexagon_2 := ltac:(abstract(solve_relations));
 }.
 
-#[export] Instance RelSumSymmetricMonoidal : 
-  @SymmetricMonoidalCategory Type Rel RelSumMonoidal
-  RelSumBraidedMonoidal | 10 := {
-  symmetry := ltac:(abstract(solve_relations));
+#[export, program] Instance RelSumSymmetricMonoidal : 
+  SymmetricMonoidalCategory RelSumBraidedMonoidal | 10 := {
 }.
 
 Lemma not_RelSumCompactClosed :
@@ -514,22 +482,15 @@ Proof.
   solve_relations.
 Qed.
 
-#[export] Instance RelSumDagger : DaggerCategory Type | 10 := {
+#[export, program] Instance RelSumDagger : DaggerCategory Rel | 10 := {
   adjoint := fun A B => @flip A B Prop;
-  adjoint_involutive := ltac:(easy);
-  adjoint_id := ltac:(easy);
-  adjoint_contravariant := ltac:(abstract(solve_relations));
-  adjoint_compat := ltac:(abstract(solve_relations));
 }.
 
-#[export] Instance RelSumDaggerMonoidal : DaggerMonoidalCategory Type | 10 := {
-  dagger_tensor_compat := ltac:(abstract(solve_relations));
-  associator_unitary := ltac:(abstract(solve_relations));
-  left_unitor_unitary := ltac:(abstract(solve_relations));
-  right_unitor_unitary := ltac:(abstract(solve_relations));
+#[export, program] Instance RelSumDaggerMonoidal 
+  : DaggerMonoidalCategory RelSumDagger RelSumMonoidal | 10 := {
 }.
 
-#[export] Instance RelLeftDistributivityIsomorphism (A B M : Type) :
+#[export, program] Instance RelLeftDistributivityIsomorphism (A B M : Type) :
   @Isomorphism Type Rel (A * (B + M))
   ((A * B) + (A * M)) := {
   forward := fun abm abam => match abm, abam with
@@ -542,10 +503,9 @@ Qed.
     | (a, inr m), inr (a', m') => a = a' /\ m = m'
     | _, _ => False
     end;
-  isomorphism_inverse := ltac:(abstract(solve_relations));
 }.
 
-#[export] Instance RelRightDistributivityIsomorphism (A B M : Type) :
+#[export, program] Instance RelRightDistributivityIsomorphism (A B M : Type) :
   @Isomorphism Type Rel ((A + B) * M)
   ((A * M) + (B * M)) := {
   forward := fun abm ambm => match abm, ambm with
@@ -558,7 +518,6 @@ Qed.
     | (inr b, m), inr (b', m') => b = b' /\ m = m'
     | _, _ => False
     end;
-  isomorphism_inverse := ltac:(abstract(solve_relations));
 }.
 
 Lemma rel_left_distributivity_isomorphism_natural {A B M A' B' M' : Type}
@@ -581,21 +540,19 @@ Proof.
   solve_relations.
 Qed.
 
-#[export] Instance RelLeftAbsorbtion (A : Type) :
+#[export, program] Instance RelLeftAbsorbtion (A : Type) :
   (⊥ * A <~> ⊥)%Cat := {
   forward := fun bota => match bota with | (bot, a) => match bot with end end;
   reverse := fun bot => match bot with end;
-  isomorphism_inverse := ltac:(abstract(solve_relations));
 }.
 
-#[export] Instance RelRightAbsorbtion (A : Type) :
+#[export, program] Instance RelRightAbsorbtion (A : Type) :
   (A * ⊥ <~> ⊥)%Cat := {
   forward := fun abot => match abot with | (a, bot) => match bot with end end;
   reverse := fun bot => match bot with end;
-  isomorphism_inverse := ltac:(abstract(solve_relations));
 }.
 
-#[export] Instance RelPreDistr : 
+#[export, program] Instance RelPreDistr : 
   PreDistributiveBimonoidalCategory RelSumSymmetricMonoidal
   RelMonoidal := {
     left_distr_iso := RelLeftDistributivityIsomorphism;
@@ -604,17 +561,17 @@ Qed.
     right_distr_natural := @rel_right_distributivity_isomorphism_natural;
 }.
 
-#[export] Instance RelDistrBimonoidal : 
-  DistributiveBimonoidalCategory RelSumSymmetricMonoidal RelMonoidal := {
+#[export, program] Instance RelDistrBimonoidal : 
+  DistributiveBimonoidalCategory RelPreDistr := {
   left_absorbtion_iso := RelLeftAbsorbtion;
   right_absorbtion_iso := RelRightAbsorbtion;
-  left_absorbtion_natural := ltac:(abstract(solve_relations));
-  right_absorbtion_natural := ltac:(abstract(solve_relations));
 }.
 
-(* #[export] Instance RelSemiCoherent :
+Obligation Tactic := idtac.
+
+#[export, program] Instance RelSemiCoherent :
   SemiCoherent_DistributiveBimonoidalCategory RelDistrBimonoidal := {
-  condition_I (A B C : Type) := ltac:(abstract(solve_relations));
+  (* condition_I (A B C : Type) := ltac:(abstract(solve_relations));
   condition_III (A B C : Type) := ltac:(abstract(solve_relations));
   condition_IV (A B C D : Type) := ltac:(abstract(solve_relations));
   condition_V (A B C D : Type) := ltac:(abstract(solve_relations));
@@ -635,16 +592,41 @@ Qed.
   condition_XXI (A B : Type) := ltac:(abstract(solve_relations));
   condition_XXII (A B : Type) := ltac:(abstract(solve_relations));
   condition_XXIII (A B : Type) := ltac:(abstract(solve_relations));
-  condition_XXIV (A B : Type) := ltac:(abstract(solve_relations));
-}. *)
-
-#[export] Instance RelSemiCoherentBraided :
+  condition_XXIV (A B : Type) := ltac:(abstract(solve_relations)); *)
+}.
+Next Obligation. hnf; solve_relations. Qed.
+Next Obligation. hnf; solve_relations. Qed.
+Next Obligation. hnf; solve_relations. Qed.
+Next Obligation. hnf; solve_relations. Qed.
+Next Obligation. hnf; solve_relations. Qed.
+Next Obligation. hnf; solve_relations. Qed.
+Next Obligation. hnf; solve_relations. Qed.
+Next Obligation. hnf; solve_relations. Qed.
+Next Obligation. hnf; solve_relations. Qed.
+Next Obligation. hnf; solve_relations. Qed.
+Next Obligation. hnf; solve_relations. Qed.
+Next Obligation. hnf; solve_relations. Qed.
+Next Obligation. hnf; solve_relations. Qed.
+Next Obligation. hnf; solve_relations. Qed.
+Next Obligation. hnf; solve_relations. Qed.
+Next Obligation. hnf; solve_relations. Qed.
+Next Obligation. hnf; solve_relations. Qed.
+Next Obligation. hnf; solve_relations. Qed.
+Next Obligation. hnf; solve_relations. Qed.
+Next Obligation. hnf; solve_relations. Qed.
+Next Obligation. hnf; solve_relations. Qed.
+Next Obligation. hnf; solve_relations. Qed.
+
+Obligation Tactic := (hnf; solve_relations).
+
+#[export, program] Instance RelSemiCoherentBraided :
   SemiCoherent_BraidedDistributiveBimonoidalCategory RelDistrBimonoidal RelBraidedMonoidal := {
-  condition_II (A B C : Type) := ltac:(abstract(solve_relations));
-  condition_XV (A : Type) := ltac:(abstract(solve_relations));
+  (* condition_II (A B C : Type) := ltac:(abstract(solve_relations));
+  condition_XV (A : Type) := ltac:(abstract(solve_relations)); *)
 }.
 
 Local Open Scope Cat_scope.
+Local Open Scope Obj_scope.
 Generalizable Variable C.
 
 Set Universe Polymorphism.
@@ -666,6 +648,7 @@ Class CategoryProduct `{cC : Category C} (A B : C) (AB : C) := {
     fAB' ≃ prod_mor Q fA fB
 }.
 
+Arguments CategoryProduct {_} {_}%Cat (_ _ _)%Obj.
 (* Local Notation "'@' AB" := (AB.(prod_AB)) (at level 8) : Cat_scope. *)
 
 
@@ -684,6 +667,7 @@ Proof.
   easy.
 Qed.
 
+Obligation Tactic := idtac.
 Program Definition category_product_unique `{cC : Category C} (A B : C) :
   forall {AB AB'} (HAB : CategoryProduct A B AB) 
   (HAB' : CategoryProduct A B AB'), Isomorphism AB AB' :=
@@ -702,7 +686,7 @@ Qed.
 
 Class CartesianMonoidalCategory `(mC : MonoidalCategory C) := {
   tensor_cartesian : forall (A B : C),
-    CategoryProduct A B (A × B);
+    CategoryProduct A B (A × B)%Mon;
 }.
 
 #[export, program] Instance RelCartesianMonoidalCategory :
@@ -717,37 +701,40 @@ Class CartesianMonoidalCategory `(mC : MonoidalCategory C) := {
         end
     |}
   }.
-Obligation 4. (* Only uniqueness can't be (fully) automated *)
+Obligations.
+Next Obligation.
+ solve_relations.
+Qed.
+Next Obligation.
   __setup_solve_relations.
-  intros q [a | b].
-  - rewrite H.
-    solve_relations.
-  - rewrite H0.
-    solve_relations.
+  intros A B Q fA fB fAB'.
+  repeat split;
+  __process_solve_relations_cleanup_vars;
+  rewrite 1?H, 1?H0;
+  solve_relations.
 Qed.
-Solve All Obligations with solve_relations.
 
 Module BigPredProd.
-Class CategoryBigProd `{cC : Category C} (I : C -> Prop) (prod_I : C) := {
-  p_i : forall i, I i -> prod_I ~> i;
+Class CategoryBigProd `{cC : Category C} (J : C -> Prop) (prod_J : C) := {
+  p_i : forall i, J i -> prod_J ~> i;
   big_prod_mor : 
-    forall (Q : C) (fQ_ : forall i, I i -> Q ~> i), Q ~> prod_I;
+    forall (Q : C) (fQ_ : forall i, J i -> Q ~> i), Q ~> prod_J;
   big_prod_mor_prop: 
-    forall (Q : C) (fQ_ : forall i, I i -> Q ~> i),
-    forall i (Hi : I i), 
+    forall (Q : C) (fQ_ : forall i, J i -> Q ~> i),
+    forall i (Hi : J i), 
     (big_prod_mor Q fQ_) ∘ p_i i Hi ≃ fQ_ i Hi;
   big_prod_mor_unique : 
-    forall (Q : C) (fQ_ : forall i, I i -> Q ~> i)
-    (fAB' : Q ~> prod_I), 
-    (forall i (Hi : I i), fQ_ i Hi ≃ fAB' ∘ p_i i Hi) ->
+    forall (Q : C) (fQ_ : forall i, J i -> Q ~> i)
+    (fAB' : Q ~> prod_J), 
+    (forall i (Hi : J i), fQ_ i Hi ≃ fAB' ∘ p_i i Hi) ->
     fAB' ≃ big_prod_mor Q fQ_
 }.
 
-Lemma big_prod_mor_unique' `{cC : Category C} {I} {pI : C} 
-  (HI : CategoryBigProd I pI) {Q} (fQ_ : forall i, I i -> Q ~> i) : 
-  forall (fAB fAB' : Q ~> pI),
-  (forall i (Hi : I i), fAB ∘ p_i i Hi ≃ fQ_ i Hi) ->
-  (forall i (Hi : I i), fAB' ∘ p_i i Hi ≃ fQ_ i Hi) ->
+Lemma big_prod_mor_unique' `{cC : Category C} {J} {pJ : C} 
+  (HJ : CategoryBigProd J pJ) {Q} (fQ_ : forall i, J i -> Q ~> i) : 
+  forall (fAB fAB' : Q ~> pJ),
+  (forall i (Hi : J i), fAB ∘ p_i i Hi ≃ fQ_ i Hi) ->
+  (forall i (Hi : J i), fAB' ∘ p_i i Hi ≃ fQ_ i Hi) ->
   fAB ≃ fAB'.
 Proof.
   intros.
@@ -757,13 +744,13 @@ Proof.
   easy.
 Qed.
 
-Program Definition category_big_prod_unique `{cC : Category C} I :
-  forall {pI pI'} (HI : CategoryBigProd I pI) (HI' : CategoryBigProd I pI'), 
-    Isomorphism pI pI' :=
-  fun pI pI' HI HI' =>
+Program Definition category_big_prod_unique `{cC : Category C} J :
+  forall {pJ pJ'} (HJ : CategoryBigProd J pJ) (HJ' : CategoryBigProd J pJ'), 
+    Isomorphism pJ pJ' :=
+  fun pJ pJ' HJ HJ' =>
   {|
-    forward := HI'.(big_prod_mor) pI p_i;
-    reverse := HI.(big_prod_mor) pI' p_i;
+    forward := HJ'.(big_prod_mor) pJ p_i;
+    reverse := HJ.(big_prod_mor) pJ' p_i;
   |}.
 Obligations.
 Next Obligation.
@@ -774,25 +761,25 @@ Qed.
 End BigPredProd.
 
 
-Class CategoryBigProd `{cC : Category C} {I : Type} 
-  (obj : I -> C) (prod_I : C) := {
-  p_i : forall i, prod_I ~> obj i;
+Class CategoryBigProd `{cC : Category C} {J : Type} 
+  (obj : J -> C) (prod_J : C) := {
+  p_i : forall i, prod_J ~> obj i;
   big_prod_mor : 
-    forall (Q : C) (fQ_ : forall i, Q ~> obj i), Q ~> prod_I;
+    forall (Q : C) (fQ_ : forall i, Q ~> obj i), Q ~> prod_J;
   big_prod_mor_prop: 
     forall (Q : C) (fQ_ : forall i, Q ~> obj i),
     forall i, 
     (big_prod_mor Q fQ_) ∘ p_i i ≃ fQ_ i;
   big_prod_mor_unique : 
     forall (Q : C) (fQ_ : forall i, Q ~> obj i)
-    (fAB' : Q ~> prod_I), 
+    (fAB' : Q ~> prod_J), 
     (forall i, fQ_ i ≃ fAB' ∘ p_i i) ->
     fAB' ≃ big_prod_mor Q fQ_
 }.
 
-Lemma big_prod_mor_unique' `{cC : Category C} {I} {obj : I -> C} {pI : C} 
-  (HI : CategoryBigProd obj pI) {Q} (fQ_ : forall i, Q ~> obj i) :
-  forall (fAB fAB' : Q ~> pI),
+Lemma big_prod_mor_unique' `{cC : Category C} {J} {obj : J -> C} {pJ : C} 
+  (HJ : CategoryBigProd obj pJ) {Q} (fQ_ : forall i, Q ~> obj i) :
+  forall (fAB fAB' : Q ~> pJ),
   (forall i, fAB  ∘ p_i i ≃ fQ_ i) ->
   (forall i, fAB' ∘ p_i i ≃ fQ_ i) ->
   fAB ≃ fAB'.
@@ -804,13 +791,13 @@ Proof.
   easy.
 Qed.
 
-Program Definition category_big_prod_unique `{cC : Category C} {I} {obj : I->C} :
-  forall {pI pI'} (HI : CategoryBigProd obj pI) (HI' : CategoryBigProd obj pI'), 
-    Isomorphism pI pI' :=
-  fun pI pI' HI HI' =>
+Program Definition category_big_prod_unique `{cC : Category C} {J} {obj : J->C} :
+  forall {pJ pJ'} (HJ : CategoryBigProd obj pJ) (HJ' : CategoryBigProd obj pJ'), 
+    Isomorphism pJ pJ' :=
+  fun pJ pJ' HJ HJ' =>
   {|
-    forward := HI'.(big_prod_mor) pI p_i;
-    reverse := HI.(big_prod_mor) pI' p_i;
+    forward := HJ'.(big_prod_mor) pJ p_i;
+    reverse := HJ.(big_prod_mor) pJ' p_i;
   |}.
 Obligations.
 Next Obligation.
@@ -820,8 +807,8 @@ Next Obligation.
 Qed.
 
 
-Inductive big_sum (I : Type -> Type) :=
-  | in_i i (a : I i) : big_sum I.
+Inductive big_sum (J : Type -> Type) :=
+  | in_i i (a : J i) : big_sum J.
 
 Arguments in_i {_} _ _.
 (* Set Printing Universes. *)
@@ -830,12 +817,14 @@ Definition my_f_equal [A B : Type] (f : A -> B) [x y : A] (H : x = y) :
   f x = f y := 
   match H in (_ = y') return (f x = f y') with eq_refl => eq_refl end.
 
-#[ export, program] Instance RelBigProd (I : Type -> Type) : 
-  CategoryBigProd I (big_sum I) := {
+Obligation Tactic := Tactics.program_simpl.
+
+#[export, program] Instance RelBigProd (J : Type -> Type) : 
+  CategoryBigProd J (big_sum J) := {
     p_i := fun i => fun somei a => match somei with
     | in_i i' a' => exists (H: i = i'), _
-      (* let Hi := my_f_equal I H in
-        match Hi in (_ = Ii') return Ii' with eq_refl => a end = a' *)
+      (* let Hi := my_f_equal J H in
+        match Hi in (_ = Ji') return Ji' with eq_refl => a end = a' *)
     end;
     big_prod_mor := fun Q fQ_ => fun q somei => match somei with
     | in_i i a => fQ_ i q a
@@ -875,7 +864,7 @@ Next Obligation.
 Qed.
 
 
-Section TransitiveClosure.
+(* Section TransitiveClosure.
 
 Local Open Scope Rig_scope.
 
@@ -1232,4 +1221,4 @@ Proof.
   intros f g h i.
   simpl.
   to_Cat.
-  Admitted.
+  Admitted. *)
diff --git a/examples/TypesExample.v b/examples/TypesExample.v
index 4d06621..5f7d40f 100644
--- a/examples/TypesExample.v
+++ b/examples/TypesExample.v
@@ -1,11 +1,8 @@
 Require Import Setoid.
 Require Import Logic.
-Require Import Basics.
 From ViCaR Require Export CategoryTypeclass.
 From ViCaR Require Import RigCategory.
 
-
-
 Local Notation "f '\o' g" := (fun A => g (f A)) 
   (at level 45, left associativity).
 
@@ -101,20 +98,20 @@ Ltac __solve_functions_end :=
   | H : ?A ~ ?A' |- _ => apply H
   | H : ?A ~ ?A' |- _ => symmetry; apply H
   | H : ?A ~ ?A' |- context[?A ?i] => 
-    (rewrite H; clear H; print_state; solve __solve_functions_end)
-    || (rewrite <- H; clear H; print_state; solve __solve_functions_end)
-    || (clear H; solve __solve_functions_end)
+    (rewrite H; clear H; print_state; solve [__solve_functions_end])
+    || (rewrite <- H; clear H; print_state; solve [__solve_functions_end])
+    || (clear H; solve [__solve_functions_end])
   | H : ?A ~ ?A' |- context[?A' ?i] =>   
-    (rewrite <- H; clear H; print_state; solve __solve_functions_end)
-    || (rewrite H; clear H; print_state; solve __solve_functions_end)
-    || (clear H; solve __solve_functions_end)
+    (rewrite <- H; clear H; print_state; solve [__solve_functions_end])
+    || (rewrite H; clear H; print_state; solve [__solve_functions_end])
+    || (clear H; solve [__solve_functions_end])
   end || idtac (* " no match" *)).
 
 
 Ltac solve_functions := idtac. (* Hack to allow "mutual recursion" *)
 
 Ltac __setup_solve_functions :=
-  simpl; unfold unitary; simpl;
+  simpl;
   unfold fun_equiv, id, fun_sum, 
     fun_prod in *;
   simpl.
@@ -258,7 +255,7 @@ Qed.
   right_unit := @compose_id_r;
 }.
 
-Lemma prod_id {A B} : 
+Lemma prod_jd {A B} : 
   id \* id ~ @id (A*B).
 Proof.
   intros [a b].
@@ -286,7 +283,7 @@ Qed.
 #[export] Instance ProductFunction : Bifunctor Typ Typ Typ := {
   obj_bimap := prod;
   morphism_bimap := @fun_prod;
-  id_bimap := @prod_id;
+  id_bimap := @prod_jd;
   compose_bimap := @prod_compose;
   morphism_bicompat := @prod_compat;
 }.
@@ -314,9 +311,9 @@ Qed.
     isomorphism_inverse := ltac:(abstract(solve_functions))
 }.
 
-#[export] Instance TypMonoidal : MonoidalCategory Type := {
+#[export] Instance TypMonoidal : MonoidalCategory Typ := {
   tensor := ProductFunction;
-	I := ⊤;
+	mon_I := ⊤;
   associator := @TypAssociator;
   left_unitor := @TypLeftUnitor;
   right_unitor := @TypRightUnitor;
@@ -340,14 +337,14 @@ Qed.
   component_biiso_natural := ltac:(abstract(solve_functions))
 }.
 
-#[export] Instance TypBraidedMonoidal : BraidedMonoidalCategory Type := {
+#[export] Instance TypBraidedMonoidal : BraidedMonoidalCategory TypMonoidal := {
   braiding := TypBraiding;
   hexagon_1 := ltac:(abstract(solve_functions));
   hexagon_2 := ltac:(abstract(solve_functions));
 }.
 
 #[export] Instance TypSymmetricMonoidal : 
-  SymmetricMonoidalCategory Type := {
+  SymmetricMonoidalCategory TypBraidedMonoidal := {
   symmetry := ltac:(abstract(solve_functions));
 }.
 
@@ -437,9 +434,9 @@ Qed.
   isomorphism_inverse := ltac:(abstract(solve_functions))
 }.
 
-#[export] Instance TypSumMonoidal : MonoidalCategory Type := {
+#[export] Instance TypSumMonoidal : MonoidalCategory Typ | 10 := {
   tensor := SumFunction;
-	I := ⊥;
+	mon_I := ⊥;
   associator := @TypSumAssociator;
   left_unitor := @TypSumLeftUnitor;
   right_unitor := @TypSumRightUnitor;
@@ -471,14 +468,15 @@ Qed.
   component_biiso_natural := ltac:(abstract(solve_functions))
 }.
 
-#[export] Instance TypSumBraidedMonoidal : BraidedMonoidalCategory Type := {
+#[export] Instance TypSumBraidedMonoidal 
+  : BraidedMonoidalCategory TypSumMonoidal | 10 := {
   braiding := TypSumBraiding;
   hexagon_1 := ltac:(abstract(solve_functions));
   hexagon_2 := ltac:(abstract(solve_functions));
 }.
 
 #[export] Instance TypSumSymmetricMonoidal : 
-  SymmetricMonoidalCategory Type := {
+  SymmetricMonoidalCategory TypSumBraidedMonoidal | 10 := {
   symmetry := ltac:(abstract(solve_functions));
 }.
 
@@ -491,8 +489,7 @@ Proof.
 Qed.
 
 #[export] Instance TypLeftDistributivityIsomorphism (A B M : Type) :
-  @Isomorphism Type Typ (A * (B + M))
-  ((A * B) + (A * M)) := {
+  @Isomorphism Type Typ (A * (B + M)) ((A * B) + (A * M)) := {
   forward := fun abm => match abm with
     | (a, inl b) => inl (a, b)
     | (a, inr m) => inr (a, m)
@@ -505,8 +502,7 @@ Qed.
 }.
 
 #[export] Instance TypRightDistributivityIsomorphism (A B M : Type) :
-  @Isomorphism Type Typ ((A + B) * M)
-  ((A * M) + (B * M)) := {
+  @Isomorphism Type Typ ((A + B) * M) ((A * M) + (B * M)) := {
     forward := fun abm => match abm with
     | (inl a, m) => inl (a, m)
     | (inr b, m) => inr (b, m)
@@ -562,7 +558,7 @@ Qed.
 }.
 
 #[export] Instance TypDistrBimonoidal : 
-  DistributiveBimonoidalCategory TypSumSymmetricMonoidal TypMonoidal := {
+  DistributiveBimonoidalCategory TypPreDistr := {
   left_absorbtion_iso := TypLeftAbsorbtion;
   right_absorbtion_iso := TypRightAbsorbtion;
   left_absorbtion_natural := ltac:(abstract(solve_functions));
@@ -571,6 +567,29 @@ Qed.
 
 #[export] Instance TypSemiCoherent :
   SemiCoherent_DistributiveBimonoidalCategory TypDistrBimonoidal := {
+  cond_I (A B C : Type) := ltac:(abstract(solve_functions));
+  cond_III (A B C : Type) := ltac:(abstract(solve_functions));
+  cond_IV (A B C D : Type) := ltac:(abstract(solve_functions));
+  cond_V (A B C D : Type) := ltac:(abstract(solve_functions));
+  cond_VI (A B C D : Type) := ltac:(abstract(solve_functions));
+  cond_VII (A B C D : Type) := ltac:(abstract(solve_functions));
+  cond_VIII (A B C D : Type) := ltac:(abstract(solve_functions));
+  cond_IX  (A B C D : Type) := ltac:(abstract(solve_functions));
+  cond_X := ltac:(abstract(solve_functions));
+  cond_XI (A B : Type) := ltac:(abstract(solve_functions));
+  cond_XII (A B : Type) := ltac:(abstract(solve_functions));
+  cond_XIII := ltac:(abstract(solve_functions));
+  cond_XIV := ltac:(abstract(solve_functions));
+  cond_XVI (A B : Type) := ltac:(abstract(solve_functions));
+  cond_XVII (A B : Type) := ltac:(abstract(solve_functions));
+  cond_XVIII (A B : Type) := ltac:(abstract(solve_functions));
+  cond_XIX (A B : Type) := ltac:(abstract(solve_functions));
+  cond_XX (A B : Type) := ltac:(abstract(solve_functions));
+  cond_XXI (A B : Type) := ltac:(abstract(solve_functions));
+  cond_XXII (A B : Type) := ltac:(abstract(solve_functions));
+  cond_XXIII (A B : Type) := ltac:(abstract(solve_functions));
+  cond_XXIV (A B : Type) := ltac:(abstract(solve_functions));
+(* 
   condition_I (A B C : Type) := ltac:(abstract(solve_functions));
   condition_III (A B C : Type) := ltac:(abstract(solve_functions));
   condition_IV (A B C D : Type) := ltac:(abstract(solve_functions));
@@ -592,13 +611,14 @@ Qed.
   condition_XXI (A B : Type) := ltac:(abstract(solve_functions));
   condition_XXII (A B : Type) := ltac:(abstract(solve_functions));
   condition_XXIII (A B : Type) := ltac:(abstract(solve_functions));
-  condition_XXIV (A B : Type) := ltac:(abstract(solve_functions));
+  condition_XXIV (A B : Type) := ltac:(abstract(solve_functions)); 
+*)
 }.
 
 #[export] Instance TypSemiCoherentBraided :
   SemiCoherent_BraidedDistributiveBimonoidalCategory TypDistrBimonoidal TypBraidedMonoidal := {
-  condition_II (A B C : Type) := ltac:(abstract(solve_functions));
-  condition_XV (A : Type) := ltac:(abstract(solve_functions));
+  cond_II (A B C : Type) := ltac:(abstract(solve_functions));
+  cond_XV (A : Type) := ltac:(abstract(solve_functions));
 }.
 
 
@@ -630,6 +650,8 @@ Class CategoryProduct `{cC : Category C} (A B : C) (AB : C) := {
     fAB' ≃ prod_mor Q fA fB
 }.
 
+Arguments CategoryProduct {_} {_}%Cat (_ _ _)%Obj.
+
 (* Local Notation "'@' AB" := (AB.(prod_AB)) (at level 8) : Cat_scope. *)
 
 
@@ -664,9 +686,11 @@ Next Obligation.
   all: rewrite left_unit; easy.
 Qed.
 
+
+
 Class CartesianMonoidalCategory `(mC : MonoidalCategory C) := {
   tensor_cartesian : forall (A B : C),
-    CategoryProduct A B (A × B);
+    CategoryProduct A B (A × B)%Mon;
 }.
 
 #[export, program] Instance TypCartesianMonoidalCategory :
@@ -688,25 +712,25 @@ Next Obligation.
   easy. 
 Qed.
 
-Class CategoryBigProd `{cC : Category C} {I : Type} 
-  (obj : I -> C) (prod_I : C) := {
-  p_i : forall i, prod_I ~> obj i;
+Class CategoryBigProd `{cC : Category C} {J : Type} 
+  (obj : J -> C) (prod_J : C) := {
+  p_i : forall i, prod_J ~> obj i;
   big_prod_mor : 
-    forall (Q : C) (fQ_ : forall i, Q ~> obj i), Q ~> prod_I;
+    forall (Q : C) (fQ_ : forall i, Q ~> obj i), Q ~> prod_J;
   big_prod_mor_prop: 
     forall (Q : C) (fQ_ : forall i, Q ~> obj i),
     forall i, 
     (big_prod_mor Q fQ_) ∘ p_i i ≃ fQ_ i;
   big_prod_mor_unique : 
     forall (Q : C) (fQ_ : forall i, Q ~> obj i)
-    (fAB' : Q ~> prod_I), 
+    (fAB' : Q ~> prod_J), 
     (forall i, fQ_ i ≃ fAB' ∘ p_i i) ->
     fAB' ≃ big_prod_mor Q fQ_
 }.
 
-Lemma big_prod_mor_unique' `{cC : Category C} {I} {obj : I -> C} {pI : C} 
-  (HI : CategoryBigProd obj pI) {Q} (fQ_ : forall i, Q ~> obj i) :
-  forall (fAB fAB' : Q ~> pI),
+Lemma big_prod_mor_unique' `{cC : Category C} {J} {obj : J -> C} {pJ : C} 
+  (HI : CategoryBigProd obj pJ) {Q} (fQ_ : forall i, Q ~> obj i) :
+  forall (fAB fAB' : Q ~> pJ),
   (forall i, fAB  ∘ p_i i ≃ fQ_ i) ->
   (forall i, fAB' ∘ p_i i ≃ fQ_ i) ->
   fAB ≃ fAB'.
@@ -718,13 +742,13 @@ Proof.
   easy.
 Qed. 
 
-Program Definition category_big_prod_unique `{cC : Category C} {I} {obj : I->C} :
-  forall {pI pI'} (HI : CategoryBigProd obj pI) (HI' : CategoryBigProd obj pI'), 
-    Isomorphism pI pI' :=
-  fun pI pI' HI HI' =>
+Program Definition category_big_prod_unique `{cC : Category C} {J} {obj : J->C} :
+  forall {pJ pJ'} (HI : CategoryBigProd obj pJ) (HI' : CategoryBigProd obj pJ'), 
+    Isomorphism pJ pJ' :=
+  fun pJ pJ' HI HI' =>
   {|
-    forward := HI'.(big_prod_mor) pI p_i;
-    reverse := HI.(big_prod_mor) pI' p_i;
+    forward := HI'.(big_prod_mor) pJ p_i;
+    reverse := HI.(big_prod_mor) pJ' p_i;
   |}.
 Next Obligation.
   split; eapply (big_prod_mor_unique' _ p_i); rewrite 1?assoc.
@@ -734,9 +758,9 @@ Qed.
 
 Require Import FunctionalExtensionality.
 
-Definition big_prod {I} (obj : I -> Type) := forall (i : I), obj i.
+Definition big_prod {J} (obj : J -> Type) := forall (i : J), obj i.
 
-#[export, program] Instance TypBigProd {I} {obj : I -> Type} : 
+#[export, program] Instance TypBigProd {J} {obj : J -> Type} : 
   CategoryBigProd obj (big_prod obj) := {
   p_i := fun i => fun f => f i;
   big_prod_mor := fun Q fQ_ => fun q => fun i => fQ_ i q;
@@ -801,29 +825,29 @@ Next Obligation.
   all: rewrite right_unit; easy.
 Qed.
 
-Class CategoryBigCoprod `{cC : Category C} {I : Type} 
-  (obj : I -> C) (coprod_I : C) := {
-  big_coprod_obj := coprod_I;
-  iota_i : forall i, obj i ~> coprod_I;
+Class CategoryBigCoprod `{cC : Category C} {J : Type} 
+  (obj : J -> C) (coprod_J : C) := {
+  big_coprod_obj := coprod_J;
+  iota_i : forall i, obj i ~> coprod_J;
   big_coprod_mor : 
-    forall (Q : C) (fQ_ : forall i, obj i ~> Q), coprod_I ~> Q;
+    forall (Q : C) (fQ_ : forall i, obj i ~> Q), coprod_J ~> Q;
   big_coprod_mor_prop: 
     forall (Q : C) (fQ_ : forall i, obj i ~> Q),
     forall i, 
     iota_i i ∘ (big_coprod_mor Q fQ_) ≃ fQ_ i;
   big_coprod_mor_unique : 
     forall (Q : C) (fQ_ : forall i, obj i ~> Q)
-    (fAB' : coprod_I ~> Q), 
+    (fAB' : coprod_J ~> Q), 
     (forall i, fQ_ i ≃ iota_i i ∘ fAB') ->
     fAB' ≃ big_coprod_mor Q fQ_
 }.
 
-Inductive big_sum {I} (obj : I -> Type) :=
+Inductive big_sum {J} (obj : J -> Type) :=
   | in_i i (a : obj i) : big_sum obj.
 
 Arguments in_i {_ _} _ _.
 
-#[export, program] Instance TypBigCoprod {I} {obj : I -> Type} : 
+#[export, program] Instance TypBigCoprod {J} {obj : J -> Type} : 
   CategoryBigCoprod obj (big_sum obj) := {
   iota_i := fun i => fun oi => in_i i oi;
   big_coprod_mor := fun Q fQ_ => fun oi => match oi with
@@ -859,7 +883,7 @@ Notation "f @∏ g" := (cat_mor_prod f g) (at level 40).
 
 #[program, export] Instance Category_with_Products_of_CartesianMonoidalCategory {C cC mC}
   (ccc : @CartesianMonoidalCategory C cC mC) : Category_with_Products cC := {|
-  cat_prod := tensor.(obj_bimap);
+  cat_prod := mC.(tensor).(obj_bimap);
   cat_prod_product := tensor_cartesian;
 |}.
 
diff --git a/examples/TypoidExample.v b/examples/TypoidExample.v
new file mode 100644
index 0000000..625e382
--- /dev/null
+++ b/examples/TypoidExample.v
@@ -0,0 +1,1319 @@
+Require Import Setoid Morphisms. (* Morphisms_Prop may be added? *)
+Require Import Logic.
+From ViCaR Require Export CategoryTypeclass.
+From ViCaR Require Import RigCategory.
+
+
+
+Unset Program Cases. 
+(* This makes term sizes much, much smaller, as more is abstracted.
+   It was necessary to make the proof of being a Rig category go through. *)
+
+
+
+Class Setoid : Type := {
+  base_type : Type;
+  s_equiv : relation base_type;
+  s_equiv_refl :> Reflexive s_equiv;
+  s_equiv_sym :> Symmetric s_equiv;
+  s_equiv_trans :> Transitive s_equiv;
+}.
+
+Arguments base_type _ : clear implicits.
+Coercion base_type : Setoid >-> Sortclass.
+
+#[export] Instance Setoid_equiv_Equivalence (A : Setoid) : 
+  Equivalence A.(s_equiv) := ltac:(split; apply A).
+
+Add Parametric Relation (A : Setoid) : A s_equiv
+  reflexivity proved by s_equiv_refl
+  symmetry proved by s_equiv_sym
+  transitivity proved by s_equiv_trans
+  as Setoid_relation.
+
+Local Notation "x '≡' y" := (s_equiv x y) (at level 70).
+
+Class Morphism (A B : Setoid) := {
+  base_fn : A -> B;
+  base_compat : forall (x y : A), x ≡ y -> base_fn x ≡ base_fn y;
+}.
+
+Arguments base_fn {_ _} _.
+Coercion base_fn : Morphism >-> Funclass.
+
+Add Parametric Morphism {A B} (f : Morphism A B) : (@base_fn A B f)
+  with signature A.(s_equiv) ==> B.(s_equiv) as Morphism_morphism.
+Proof. exact base_compat. Qed.
+
+Notation "A '→' B" := (Morphism A B) (at level 90 ): type_scope.
+
+Lemma compose_morphisms_base_compat {A B C} (f : A → B) (g : B → C) :
+  forall x y : A, x ≡ y -> g (f x) ≡ g (f y).
+Proof.
+  intros.
+  apply base_compat, base_compat, H.
+Qed.
+
+
+Definition compose_morphisms {A B C} (f : A → B) (g : B → C) 
+  : A → C := 
+  {|
+  base_fn := fun a => g (f a);
+  base_compat := compose_morphisms_base_compat f g;
+|}.
+
+Local Notation "f '\o' g" := (compose_morphisms f g) 
+  (at level 45, left associativity).
+
+Definition mor_equiv {A B} : relation (A → B) :=
+  fun f f' => forall x, f x ≡ f' x.
+
+Local Notation "f ~ g" := (forall a, f a ≡ g a) 
+  (at level 80, no associativity).
+
+Lemma mor_equiv_refl {A B} (f : A → B) : mor_equiv f f.
+Proof. intros ?; reflexivity. Qed.
+
+Lemma mor_equiv_sym {A B} (f f' : A → B) : mor_equiv f f' -> mor_equiv f' f.
+Proof. intros Hf ?; now symmetry. Qed.
+
+Lemma mor_equiv_trans {A B} (f f' f'' : A → B) : 
+  mor_equiv f f' -> mor_equiv f' f'' -> mor_equiv f f''.
+Proof. intros Hf Hf' ?; now etransitivity. Qed.
+
+Add Parametric Relation {A B} : (A → B) (@mor_equiv A B) 
+  reflexivity proved by mor_equiv_refl
+  symmetry proved by mor_equiv_sym
+  transitivity proved by mor_equiv_trans
+  as mor_equiv_relation.
+
+Add Parametric Morphism {A B C} : (@compose_morphisms A B C)
+  with signature mor_equiv ==> mor_equiv ==> mor_equiv
+  as compose_morphisms_morphism.
+Proof.
+  intros f f' Hf g g' Hg x.
+  simpl.
+  transitivity (g (f' x)).
+  - now apply g.
+  - apply Hg.
+Qed.
+
+#[program] Definition Setoid_top : Setoid := {| 
+  base_type := Datatypes.unit;
+  s_equiv := fun _ _ => True;
+  |}.
+Solve All Obligations with auto.
+
+#[program] Definition Setoid_bot : Setoid := {| 
+  base_type := False;
+  s_equiv := fun _ _ => False;
+  |}.
+Solve All Obligations with auto.
+
+Local Notation "⊤" := Setoid_top.
+Local Notation "⊥" := Setoid_bot.
+
+#[export, program] Instance SumSetoid (A B : Setoid) : Setoid := {
+  base_type := A + B;
+  s_equiv := fun a_b a'_b' => match a_b, a'_b' with
+  | inl a, inl a' => a ≡ a'
+  | inr b, inr b' => b ≡ b'
+  | inl a, inr b' => False
+  | inr b, inl a' => False
+  end;
+}.
+Next Obligation. intros [a | b]; reflexivity. Qed.
+Next Obligation. intros [a | b] [a' | b']; easy. Qed.
+Next Obligation. intros [a | b] [a' | b'] [a'' | b''] Ha Ha';
+  easy || etransitivity; eassumption. Qed.
+
+#[export, program] Instance ProdSetoid (A B : Setoid) : Setoid := {
+  base_type := A * B;
+  s_equiv := fun ab a'b' => 
+    let (a, b) := ab in let (a', b') := a'b' in a ≡ a' /\ b ≡ b'
+}.
+Next Obligation. intros [a b]; easy. Qed.
+Next Obligation. intros [a b] [a' b']; easy. Qed.
+Next Obligation. 
+  intros [a b] [a' b'] [a'' b''] Ha Ha'; split;
+  etransitivity; try apply Ha; apply Ha'. Qed.
+
+Local Notation "A '.+' B" := (SumSetoid A B) (at level 50).
+Local Notation "A '.*' B" := (ProdSetoid A B) (at level 40).
+
+#[program] Definition mor_sum {A B A' B'} (f : A → B) (g : A' → B') :
+  (A .+ A') → (B .+ B') := {|
+  base_fn := fun i =>
+    match i with
+    | inl a => inl (f a)
+    | inr a' => inr (g a')
+    end;
+|}.
+Next Obligation.
+  do 2 match goal with 
+  | x : ?A + ?A' |- _ => destruct x
+  end; easy || apply f || apply g; easy.
+Qed.
+
+Local Notation "f '\+' g" := (mor_sum f g) (at level 43, left associativity).
+
+#[export, program] Instance mor_prod {A B A' B'} (f : A → B) (g : A' → B') :
+  (A .* A') → (B .* B') := {|
+  base_fn := fun aa' => let (a, a') := aa' in (f a, g a')
+|}.
+Next Obligation.
+  split; apply f || apply g; easy.
+Qed.
+
+
+
+Local Notation "f '\*' g" := (mor_prod f g) (at level 41, left associativity).
+
+Ltac print_state :=
+  try (match reverse goal with | H : ?p |- _ => idtac H ":" p; fail end);
+  idtac "---------------------------------------------------------";
+  match reverse goal with |- ?P => idtac P 
+  end.
+
+(* From Adam Chipala's excellent CPDT, in Match *)
+Ltac notHyp P :=
+  match goal with
+    | [ _ : P |- _ ] => fail 1
+    | _ =>
+      match P with
+        | ?P1 /\ ?P2 => first [ notHyp P1 | notHyp P2 | fail 2 ]
+        | _ => idtac
+      end
+  end.
+Ltac extend pf :=
+  let t := type of pf in
+    notHyp t; generalize pf; intro.
+
+Ltac __saturate_funs Hf :=
+  match type of Hf with ?f ?i =>
+  repeat match goal with
+  | H : f ~ ?g |- _ => 
+    let Hg := constr:(H i) in
+      extend Hg; __saturate_funs (g i)
+  | H : ?g ~ f |- _ => 
+    let Hg := constr:(H i) in
+      extend Hg; __saturate_funs (g i)
+  end
+end.
+
+Ltac __solve_morphisms_end_forward := 
+  repeat match goal with
+  | H : ?f ?i ≡ ?g ?j |- _ => (* match type of f with ?A → ?B => *)
+      revert H
+      (* end *)
+  end;
+  repeat (let Hf := fresh "Hf" in intros Hf;
+    match type of Hf with
+    | ?f ?i ≡ ?g ?j =>
+      __saturate_funs (f i); __saturate_funs (g j)
+    end);
+  easy.
+
+Ltac __solve_morphisms_end := idtac.
+Ltac __solve_morphisms_end_match se := 
+  match goal with
+  (* | |- ?f ?x => 
+      match type of f with ?n → ?m => eassumption end *)
+  | |- base_fn ?f ?i ≡ base_fn ?f ?j => 
+      (* idtac "hitsame"; *)
+      apply f; solve [se]
+  (* | |- base_fn ?f ?i ≡ base_fn ?g ?j => (* idtac "equiv"; *) 
+      fail (* match goal with 
+      | |-  
+      let H := fresh in assert (H : i ≡ j) by solve_morphisms; *) *)
+  | H : base_fn ?A ~ base_fn ?A' |- base_fn ?A ?i ≡ base_fn ?A' ?i => 
+      (* idtac "hitexact";  *)
+      apply H
+  | H : base_fn ?A ~ base_fn ?A' |- base_fn ?A' ?i ≡ base_fn ?A ?i => 
+      (* idtac "hitsym";  *)
+      symmetry; apply H
+  | H : base_fn ?A ~ base_fn ?A' |- base_fn ?A ?i ≡ base_fn ?A' ?j => 
+      (* idtac "hitbase"; *)
+      rewrite H; try apply A'; 
+      solve [se]
+  | H : base_fn ?A ~ base_fn ?A' |- base_fn ?A' ?i ≡ base_fn ?A ?j => 
+      (* idtac "hitbasesym"; *)
+      rewrite <- H; print_state; solve [se]
+  | H : base_fn ?A ~ base_fn ?A' |- _ => apply H
+      (* ; idtac "hitdesparate" *)
+  | H : base_fn ?A ~ base_fn ?A' |- _ => symmetry; apply H
+      (* ; idtac "hitdesparatesym" *)
+  | H : base_fn ?A ~ base_fn ?A' |- context[?A ?i] => 
+      (* idtac "hitrew"; *)
+      (rewrite H; clear H; 
+        (* print_state;  *)
+        solve [se])
+      || (rewrite <- H; clear H; 
+        (* print_state;  *)
+        solve [se])
+      || (clear H; solve [se])
+  | H : base_fn ?A ~ base_fn ?A' |- context[base_fn ?A' ?i] =>   
+      (* idtac "hitrewsym"; *)
+      (rewrite <- H; clear H; 
+        (* print_state;  *)
+        solve [se])
+      || (rewrite H; clear H; 
+        (* print_state;  *)
+        solve [se])
+      || (clear H; solve [se])
+  | H : _ |- _ => apply H; clear H; solve [se]
+  (* | _ => constructor; solve [__solve_morphisms_end] *)
+  | |- ?x ≡ ?y => 
+      let H := fresh in enough (H: x = y) by (rewrite H; reflexivity);
+      solve [se]
+  end.
+
+(* Begin tactics *)
+
+Ltac __solve_morphisms_end_no_constr := 
+  try eassumption;
+  try (etransitivity; eauto);
+  try reflexivity;
+  try easy;
+  auto;  
+  try (__solve_morphisms_end_match __solve_morphisms_end_no_constr 
+    || idtac (* " no match" *)).
+
+Ltac __solve_morphisms_end ::= 
+  try eassumption;
+  try (etransitivity; eauto);
+  try reflexivity;
+  try easy;
+  auto;  
+  try (__solve_morphisms_end_match __solve_morphisms_end 
+    || constructor; solve [__solve_morphisms_end_no_constr]
+    || econstructor; solve [__solve_morphisms_end_no_constr]).
+
+
+Ltac solve_morphisms := idtac. (* Hack to allow "mutual recursion" *)
+
+Ltac __setup_solve_morphisms :=
+  simpl; 
+  unfold mor_equiv, id, compose_morphisms,
+  mor_sum, mor_prod in *;
+  simpl.
+
+Ltac __solve_morphisms_mid_step := 
+  repeat (intros ?); intros; subst; auto.
+
+Lemma exists_prod {A B} : forall P,
+  (exists ab : A * B, P ab) <-> (exists (a : A) (b : B), P (a, b)).
+Proof.
+  intros P.
+  split.
+  - intros [[a b] HPab].
+    exists a, b; exact HPab.
+  - intros [a [b HPab]].
+    exists (a, b); exact HPab.
+Qed.
+
+Lemma exists_sum {A B} : forall P,
+  (exists ab : A + B, P ab) <-> 
+  ((exists (a : A), P (inl a)) \/ exists (b : B), P (inr b)).
+Proof.
+  intros P.
+  split.
+  - intros [[a | b] HPab]; [left | right];
+    eexists; eassumption.
+  - intros [[a HPa] | [b HPb]]; 
+    eexists; eassumption.
+Qed.
+
+
+Ltac __process_solve_morphisms_cleanup_vars :=
+  repeat match goal with
+  | a : ?A * ?B |- _ => destruct a
+  | a : ⊤ |- _ => destruct a
+  | a : ?A + ?B |- _ => destruct a
+  | a : sig _ |- _ => destruct a
+  | a : sigT _ |- _ => destruct a
+  | a : sig2 _ _ |- _ => destruct a
+  | a : sigT2 _ _ |- _ => destruct a
+  end.
+
+Ltac __process_solve_morphisms_step :=
+  __process_solve_morphisms_cleanup_vars;
+  try easy;
+  match goal with
+  | H : (_, _) = (_, _) |- _ => inversion H; subst; clear H
+  | H : (_, _) ≡ (_, _) |- _ => inversion H; subst; clear H
+  | H : @eq (_ + _) _ _ |- _ => inversion H; subst; clear H
+
+  | H : (exists _, _) |- _ => destruct H
+  | H : _ /\ _ |- _ => destruct H
+  | |- _ <-> _ => split
+  | |- _ /\ _ => split
+  | H : _ \/ _ |- _ => destruct H; [solve_morphisms | solve_morphisms]
+  | |- _ \/ _ => 
+       (left; solve [solve_morphisms; auto]) 
+    || (right; solve [solve_morphisms; auto]) 
+    || (* print_state; *) fail 2
+  | |- exists (_ : ?A), _ => 
+    match A with 
+    | ?B * ?C => rewrite exists_prod
+    | ?B + ?C => rewrite exists_sum
+    | ⊤ => exists tt
+    | _ => 
+      (* idtac "trying vars"; print_state;  *)
+      match goal with
+        | x : A |- _ => 
+          exists x; (* idtac "yes" x; *) (solve [solve_morphisms; auto])
+        end; match goal with
+        | |- _ => (* idtac "none worked"; *) eexists
+      end
+    end
+  end.
+
+Ltac __process_solve_morphisms := 
+  repeat (
+  __solve_morphisms_mid_step;
+  try __process_solve_morphisms_step);
+  repeat (try __solve_morphisms_mid_step;
+  try __process_solve_morphisms_cleanup_vars).
+
+Ltac solve_morphisms ::= 
+  __setup_solve_morphisms;
+  __process_solve_morphisms;
+  __solve_morphisms_mid_step;
+  __solve_morphisms_end || __solve_morphisms_end_forward.
+(* End tactics *)
+
+#[export] Instance IdentityMorphism (A : Setoid) : Morphism A A := {|
+  base_fn := fun a => a;
+  base_compat := fun _ _ => id
+|}.
+
+Definition Id := IdentityMorphism.
+Arguments Id {_}.
+
+Lemma compose_morphisms_assoc {A B C D} : forall
+  (f : A → B) (g : B → C) (h : C → D), 
+  f \o g \o h ~ f \o (g \o h).
+Proof.
+  easy.
+Qed.
+
+Lemma compose_id_l {A B} (f : A → B) :
+  Id \o f ~ f.
+Proof. easy. Qed.
+
+Lemma compose_id_r {A B} (f : A → B) :
+  f \o Id ~ f.
+Proof. easy. Qed.
+
+Lemma compose_morphisms_compat {A B C} : forall (f f' : A → B),
+  f ~ f' -> forall (g g' : B → C), g ~ g' -> 
+  f \o g ~ f' \o g'.
+Proof.
+  solve_morphisms.
+Qed.
+
+Lemma mor_equiv_equivalence {A B} : equivalence (A → B) mor_equiv.
+Proof.
+  split; apply mor_equiv_relation.
+Qed.
+
+#[export] Instance Std : Category Setoid := {
+  morphism := Morphism;
+  c_equiv := @mor_equiv;
+  c_equiv_rel := @mor_equiv_equivalence;
+  compose := @compose_morphisms;
+  compose_compat := @compose_morphisms_compat;
+  assoc := @compose_morphisms_assoc;
+  c_identity := @IdentityMorphism;
+  left_unit := @compose_id_l;
+  right_unit := @compose_id_r;
+}.
+
+Lemma prod_id {A B} : 
+  Id \* Id ~ @Id (A .* B).
+Proof. solve_morphisms. Qed.
+
+Lemma prod_compose {A B C A' B' C'} : 
+  forall (f : A → B) (g : B → C) (f' : A' → B') (g' : B' → C'),
+  (f \o g) \* (f' \o g') ~ f \* f' \o g \* g'.
+Proof.
+  solve_morphisms.
+Qed.
+
+Lemma prod_compat {A B C D} :
+  forall (f f' : A → B) (g g' : C → D),
+  f ~ f' -> g ~ g' ->
+  f \* g ~ f' \* g'.
+Proof.
+  intros f f' g g' Hf Hg [a c].
+  simpl.
+  rewrite Hf, Hg.
+  easy.
+Qed.
+
+#[export] Instance ProductMorphism : Bifunctor Std Std Std := {
+  obj_bimap := ProdSetoid;
+  morphism_bimap := @mor_prod;
+  id_bimap := @prod_id;
+  compose_bimap := @prod_compose;
+  morphism_bicompat := @prod_compat;
+}.
+
+(* This lets us omit all obligation statements *)
+Obligation Tactic := (hnf; solve_morphisms).
+
+#[export, program] Instance StdAssociator (A B C : Setoid) : 
+  Isomorphism (A .* B .* C) (A .* (B .* C)) := {
+  forward := {| 
+    base_fn := fun ab_c : (A*B*C) => let '((a, b), c) := ab_c in (a, (b, c))
+    |};
+  reverse := {| 
+    base_fn := fun a_bc:(A*(B*C)) => let '(a, (b, c)) := a_bc in ((a, b), c)
+    |};
+}.
+
+#[export, program] Instance StdLeftUnitor (A : Setoid) :
+  @Isomorphism Setoid Std (⊤ .* A) (A) := {
+  forward := {| base_fn := fun (topa : ⊤ * A) => let (_, a) := topa in a|};
+  reverse := {| base_fn := fun (a : A) => (tt, a)|};
+}.
+
+#[export, program] Instance StdRightUnitor (A : Setoid) :
+  Isomorphism (A .* ⊤) (A) := {
+    forward := {| base_fn := fun atop : A*⊤ => let (a, _) := atop in a|};
+    reverse := {| base_fn := fun a : A => (a, tt)|};
+}.
+
+#[export, program] Instance StdMonoidal : MonoidalCategory Std := {
+  tensor := ProductMorphism;
+	mon_I := ⊤;
+  associator := @StdAssociator;
+  left_unitor := @StdLeftUnitor;
+  right_unitor := @StdRightUnitor;
+  (* associator_cohere := ltac:(abstract(solve_morphisms));
+  left_unitor_cohere := ltac:(abstract(solve_morphisms));
+  right_unitor_cohere := ltac:(abstract(solve_morphisms));
+  triangle := ltac:(abstract(solve_morphisms));
+  pentagon := ltac:(abstract(solve_morphisms)); *)
+}.
+
+
+#[export, program] Instance StdBraidingIsomorphism (A B : Setoid) : 
+  Isomorphism (A .* B) (B .* A) := {
+  forward := {| base_fn := fun ab : A*B => let (a, b) := ab in (b, a) |};
+  reverse := {| base_fn := fun ba : B*A => let (b, a) := ba in (a, b) |};
+}.
+
+#[export, program] Instance StdBraiding : 
+  NaturalBiIsomorphism ProductMorphism (CommuteBifunctor ProductMorphism) := {
+  component_biiso := @StdBraidingIsomorphism;
+  (* component_biiso_natural := ltac:(abstract(solve_morphisms)) *)
+}.
+
+#[export, program] Instance StdBraidedMonoidal : BraidedMonoidalCategory StdMonoidal := {
+  braiding := StdBraiding;
+  (* hexagon_1 := ltac:(abstract(solve_morphisms));
+  hexagon_2 := ltac:(abstract(solve_morphisms)); *)
+}.
+
+#[export, program] Instance StdSymmetricMonoidal : 
+  SymmetricMonoidalCategory StdBraidedMonoidal := {
+  (* symmetry := ltac:(abstract(solve_morphisms)); *)
+}.
+
+(* #[export] Instance StdCompactClosed : CompactClosedCategory Type := {
+  dual := fun A => A;
+  unit := @fun_unit;
+  counit := fun A => flip fun_unit;
+  triangle_1 := ltac:(abstract(solve_morphisms));
+  triangle_2 := ltac:(abstract(solve_morphisms));
+}. *)
+
+(* #[export] Instance StdDagger : DaggerCategory Type := {
+  adjoint := fun A B => @flip A B Prop;
+  adjoint_involutive := ltac:(easy);
+  adjoint_id := ltac:(easy);
+  adjoint_contravariant := ltac:(abstract(solve_morphisms));
+  adjoint_compat := ltac:(abstract(solve_morphisms));
+}.
+
+#[export] Instance StdDaggerMonoidal : DaggerMonoidalCategory Type := {
+  dagger_tensor_compat := ltac:(abstract(solve_morphisms));
+  associator_unitary := ltac:(abstract(solve_morphisms));
+  left_unitor_unitary := ltac:(abstract(solve_morphisms));
+  right_unitor_unitary := ltac:(abstract(solve_morphisms));
+}. *)
+
+
+
+
+
+Lemma sum_id {A B} : 
+  Id \+ Id ~ @Id (A .+ B).
+Proof. solve_morphisms. Qed.
+
+Lemma sum_compose {A B C A' B' C'} : 
+  forall (f : A → B) (g : B → C) (f' : A' → B') (g' : B' → C'),
+  (f \o g) \+ (f' \o g') ~ f \+ f' \o g \+ g'.
+Proof.
+  solve_morphisms.
+Qed.
+  
+#[export, program] Instance SumMorphism : Bifunctor Std Std Std | 10 := {
+  obj_bimap := SumSetoid;
+  morphism_bimap := @mor_sum;
+  id_bimap := @sum_id;
+  compose_bimap := @sum_compose;
+}.
+
+#[export, program] Instance StdSumAssociator {A B C : Setoid} : 
+  Isomorphism (A .+ B .+ C) (A .+ (B .+ C)) := {
+  forward := {|
+    base_fn := fun ab_c : A.+B.+C =>
+    match ab_c with
+    | inl (inl a) => inl a : A.+(B.+C)
+    | inl (inr b) => inr (inl b)
+    | inr c => inr (inr c)
+    end|};
+  reverse := {|
+    base_fn := fun a_bc : A.+(B.+C) =>
+    match a_bc with
+    | inl a => inl (inl a) : A.+B.+C
+    | inr (inl b) => inl (inr b)
+    | inr (inr c) => inr c
+    end|}
+  }.
+
+
+#[export, program] Instance StdSumLeftUnitor {A : Setoid} :
+  Isomorphism (⊥ .+ A) (A) := {
+  forward := {| base_fn := fun bota : ⊥.+A => match bota with
+    | inr a => a : A
+    | inl bot => match bot with end
+    end |};
+  reverse := {| base_fn := fun a => inr a : ⊥.+A |};
+}.
+
+#[export, program] Instance StdSumRightUnitor {A : Setoid} :
+  Isomorphism (A .+ ⊥) (A) := {
+  forward := {| base_fn := fun abot : A.+⊥ => match abot with
+    | inl a => a : A
+    | inr bot => match bot with end
+    end |};
+  reverse := {| base_fn := fun a => inl a : A.+⊥ |};
+}.
+
+#[export, program] Instance StdSumMonoidal : MonoidalCategory Std := {
+  tensor := SumMorphism;
+	mon_I := ⊥;
+  associator := @StdSumAssociator;
+  left_unitor := @StdSumLeftUnitor;
+  right_unitor := @StdSumRightUnitor;
+  (* associator_cohere := ltac:(abstract(solve_morphisms));
+  left_unitor_cohere := ltac:(abstract(solve_morphisms));
+  right_unitor_cohere := ltac:(abstract(solve_morphisms));
+  triangle := ltac:(abstract(solve_morphisms));
+  pentagon := ltac:(abstract(solve_morphisms)); *)
+}.
+
+#[export, program] Instance StdSumBraidingIsomorphism {A B} : 
+  Isomorphism (A .+ B) (B .+ A) := {
+  forward := {| base_fn := fun a_b : A.+B => 
+    match a_b with
+    | inl a => inr a
+    | inr b => inl b
+    end : B.+A |};
+  reverse := {| base_fn := fun b_a : B.+A => 
+    match b_a with
+    | inr a => inl a
+    | inl b => inr b 
+    end : A.+B |};
+}.
+
+#[export, program] Instance StdSumBraiding : 
+  NaturalBiIsomorphism SumMorphism (CommuteBifunctor SumMorphism) := {
+  component_biiso := @StdSumBraidingIsomorphism;
+  (* component_biiso_natural := ltac:(abstract(solve_morphisms)) *)
+}.
+
+#[export, program] Instance StdSumBraidedMonoidal 
+  : BraidedMonoidalCategory StdSumMonoidal := {
+  braiding := StdSumBraiding;
+  (* hexagon_1 := ltac:(abstract(solve_morphisms));
+  hexagon_2 := ltac:(abstract(solve_morphisms)); *)
+}.
+
+#[export, program] Instance StdSumSymmetricMonoidal : 
+  SymmetricMonoidalCategory StdSumBraidedMonoidal := {
+  (* symmetry := ltac:(abstract(solve_morphisms)); *)
+}.
+
+Lemma not_StdSumCompactClosed :
+  @CompactClosedCategory Setoid Std StdSumMonoidal 
+  StdSumBraidedMonoidal StdSumSymmetricMonoidal -> False.
+Proof.
+  intros [].
+  destruct (counit ⊤ (inl tt)).
+Qed.
+
+#[export, program] Instance StdLeftDistributivityIsomorphism (A B M : Setoid) :
+  Isomorphism (A .* (B .+ M)) ((A .* B) .+ (A .* M)) := {
+  forward := {| base_fn := fun abm : A .* (B .+ M) => match abm with
+    | (a, inl b) => inl (a, b)
+    | (a, inr m) => inr (a, m)
+    end : (A .* B) .+ (A .* M) |};
+  reverse := {| base_fn := fun abam : (A .* B) .+ (A .* M) => match abam with
+    | inl (a, b) => (a, inl b)
+    | inr (a, m) => (a, inr m)
+    end : A .* (B .+ M) |};
+}.
+
+#[export, program] Instance StdRightDistributivityIsomorphism (A B M : Setoid) :
+  Isomorphism ((A .+ B) .* M) ((A .* M) .+ (B .* M)) := {
+    forward := {| base_fn := fun abm : (A .+ B) .* M => match abm with
+    | (inl a, m) => inl (a, m)
+    | (inr b, m) => inr (b, m)
+    end : (A .* M) .+ (B .* M) |};
+  reverse := {| base_fn := fun abam => match abam : (A .* M) .+ (B .* M) with
+    | inl (a, m) => (inl a, m)
+    | inr (b, m) => (inr b, m)
+    end : (A .+ B) .* M |};
+}.
+
+Lemma rel_left_distributivity_isomorphism_natural {A B M A' B' M' : Setoid}
+  (f : A → A') (g : B → B') (h : M → M') :
+  (StdLeftDistributivityIsomorphism A B M
+  ∘ (mor_sum (mor_prod f g) (mor_prod f h))
+  ≃ mor_prod f (mor_sum g h)
+	∘ StdLeftDistributivityIsomorphism A' B' M')%Cat.
+Proof.
+  solve_morphisms.
+Qed.
+
+Lemma rel_right_distributivity_isomorphism_natural {A B M A' B' M' : Setoid}
+  (f : A → A') (g : B → B') (h : M → M') :
+  (StdRightDistributivityIsomorphism A B M
+  ∘ (mor_sum (mor_prod f h) (mor_prod g h))
+  ≃ mor_prod (mor_sum f g) h
+	∘ StdRightDistributivityIsomorphism A' B' M')%Cat.
+Proof.
+  solve_morphisms.
+Qed.
+
+#[export, program] Instance StdLeftAbsorbtion (A : Setoid) :
+  (⊥ .* A <~> ⊥)%Cat := {
+  forward := {| base_fn := fun bota : ⊥ .* A => 
+    match bota with 
+    | (bot, a) => match bot with end 
+    end : ⊥ |};
+  reverse := {| base_fn := fun bot : ⊥ => 
+    match bot with end : ⊥ .* A |};
+}.
+
+#[export, program] Instance StdRightAbsorbtion (A : Setoid) :
+  (A .* ⊥ <~> ⊥)%Cat := {
+  forward := {| base_fn := fun abot : A .* ⊥ => 
+    match abot with 
+    | (a, bot) => match bot with end 
+    end : ⊥ |};
+  reverse := {| base_fn := fun bot : ⊥ => 
+    match bot with end : A .* ⊥ |};
+}.
+
+#[export, program] Instance StdPreDistr : 
+  PreDistributiveBimonoidalCategory StdSumSymmetricMonoidal
+  StdMonoidal := {
+    left_distr_iso := StdLeftDistributivityIsomorphism;
+    right_distr_iso := StdRightDistributivityIsomorphism;
+    left_distr_natural := @rel_left_distributivity_isomorphism_natural;
+    right_distr_natural := @rel_right_distributivity_isomorphism_natural;
+}.
+
+#[export, program] Instance StdDistrBimonoidal : 
+  DistributiveBimonoidalCategory StdPreDistr := {
+  left_absorbtion_iso := StdLeftAbsorbtion;
+  right_absorbtion_iso := StdRightAbsorbtion;
+}.
+
+
+
+#[export, program] Instance StdSemiCoherent :
+  SemiCoherent_DistributiveBimonoidalCategory StdDistrBimonoidal.
+
+
+
+
+#[export, program] Instance StdSemiCoherentBraided :
+  SemiCoherent_BraidedDistributiveBimonoidalCategory StdDistrBimonoidal StdBraidedMonoidal := {
+}.
+
+
+
+
+
+
+
+Local Open Scope Cat_scope.
+Generalizable Variable C.
+
+Set Universe Polymorphism.
+
+
+Class CategoryProduct `{cC : Category C} (A B : C) (AB : C) := {
+  p_A : AB ~> A;
+  p_B : AB ~> B;
+  prod_mor : 
+    forall (Q : C) (fA : Q ~> A) (fB : Q ~> B), Q ~> AB;
+  prod_mor_prop: 
+    forall (Q : C) (fA : Q ~> A) (fB : Q ~> B),
+    (prod_mor Q fA fB) ∘ p_A ≃ fA /\
+    (prod_mor Q fA fB) ∘ p_B ≃ fB;
+  prod_mor_unique : 
+    forall (Q : C) (fA : Q ~> A) (fB : Q ~> B) 
+    (fAB' : Q ~> AB), 
+    fA ≃ fAB' ∘ p_A -> fB ≃ fAB' ∘ p_B -> 
+    fAB' ≃ prod_mor Q fA fB
+}.
+
+(* Local Notation "'@' AB" := (AB.(prod_AB)) (at level 8) : Cat_scope. *)
+
+
+
+Lemma prod_mor_unique' `{cC : Category C} {A B AB : C} 
+  (HAB : CategoryProduct A B AB) {Q} (fA : Q ~> A) (fB : Q ~> B) : 
+  forall (fAB fAB' : Q ~> AB),
+  fAB ∘ p_A ≃ fA  -> fAB ∘ p_B ≃ fB -> 
+  fAB' ∘ p_A ≃ fA -> fAB' ∘ p_B ≃ fB -> 
+  fAB ≃ fAB'.
+Proof.
+  intros.
+  rewrite (prod_mor_unique Q fA fB) by easy.
+  symmetry;
+  rewrite (prod_mor_unique Q fA fB) by easy.
+  easy.
+Qed.
+
+Definition category_product_unique `{cC : Category C} (A B : C) :
+  forall {AB AB'} (HAB : CategoryProduct A B AB) 
+  (HAB' : CategoryProduct A B AB'), Isomorphism AB AB'.
+  refine (fun AB AB' HAB HAB' =>
+  {|
+    forward := HAB'.(prod_mor) AB p_A p_B;
+    reverse := HAB.(prod_mor) AB' p_A p_B;
+  |}).
+  split; eapply (prod_mor_unique' _ p_A p_B); rewrite 1?assoc.
+  1,5: rewrite 2!(proj1 (prod_mor_prop _ _ _)); easy.
+  1,4: rewrite 2!(proj2 (prod_mor_prop _ _ _)); easy.
+  all: rewrite left_unit; easy.
+Qed.
+
+Class CartesianMonoidalCategory `(mC : MonoidalCategory C) := {
+  tensor_cartesian : forall (A B : C),
+    CategoryProduct A B (A × B)%Mon;
+}.
+
+Obligation Tactic := (try (hnf; solve_morphisms)).
+
+#[export, program] Instance StdCartesianMonoidalCategory :
+  CartesianMonoidalCategory StdMonoidal := {
+    tensor_cartesian := fun A B => {| 
+      p_A := {| base_fn := fun ab : A*B => let (a, _) := ab in a : A |};
+      p_B := {| base_fn := fun ab => let (_, b) := ab in b |};
+      prod_mor := fun Q fA fB => {| base_fn :=
+        fun q => (fA q, fB q) |}
+    |}
+  }.
+Next Obligation. 
+  __setup_solve_morphisms.
+  intros A B Q fA fB fAB' HA HB q.
+  destruct (fAB' q) eqn:e.
+  rewrite HA, HB, e.
+  easy. 
+Qed.
+
+Class CategoryBigProd `{cC : Category C} {J : Type} 
+  (obj : J -> C) (prod_J : C) := {
+  p_i : forall i, prod_J ~> obj i;
+  big_prod_mor : 
+    forall (Q : C) (fQ_ : forall i, Q ~> obj i), Q ~> prod_J;
+  big_prod_mor_prop: 
+    forall (Q : C) (fQ_ : forall i, Q ~> obj i),
+    forall i, 
+    (big_prod_mor Q fQ_) ∘ p_i i ≃ fQ_ i;
+  big_prod_mor_unique : 
+    forall (Q : C) (fQ_ : forall i, Q ~> obj i)
+    (fAB' : Q ~> prod_J), 
+    (forall i, fQ_ i ≃ fAB' ∘ p_i i) ->
+    fAB' ≃ big_prod_mor Q fQ_
+}.
+
+Lemma big_prod_mor_unique' `{cC : Category C} {J} {obj : J -> C} {pJ : C} 
+  (HI : CategoryBigProd obj pJ) {Q} (fQ_ : forall i, Q ~> obj i) :
+  forall (fAB fAB' : Q ~> pJ),
+  (forall i, fAB  ∘ p_i i ≃ fQ_ i) ->
+  (forall i, fAB' ∘ p_i i ≃ fQ_ i) ->
+  fAB ≃ fAB'.
+Proof.
+  intros.
+  rewrite (big_prod_mor_unique Q fQ_) by easy.
+  symmetry;
+  rewrite (big_prod_mor_unique Q fQ_) by easy.
+  easy.
+Qed. 
+
+Program Definition category_big_prod_unique `{cC : Category C} {J} {obj : J->C} :
+  forall {pJ pJ'} (HI : CategoryBigProd obj pJ) (HI' : CategoryBigProd obj pJ'), 
+    Isomorphism pJ pJ' :=
+  fun pJ pJ' HI HI' =>
+  {|
+    forward := HI'.(big_prod_mor) pJ p_i;
+    reverse := HI.(big_prod_mor) pJ' p_i;
+  |}.
+Next Obligation.
+  split; eapply (big_prod_mor_unique' _ p_i); rewrite 1?assoc.
+  1,3: intros i; rewrite assoc, 2!(big_prod_mor_prop _ _); easy.
+  all: intros; rewrite left_unit; easy.
+Qed.
+
+(* Require Import FunctionalExtensionality. *)
+
+#[program] Definition big_setoid_prod {J} (obj : J -> Setoid) :=  {|
+  base_type := forall (i : J), obj i;
+  s_equiv := fun is js => forall (i : J), is i ≡ js i;
+|}.
+
+#[export, program] Instance StdBigProd {J} {obj : J -> Setoid} : 
+  CategoryBigProd obj (big_setoid_prod obj) := {
+  p_i := fun i => {| base_fn := fun f => f i |};
+  big_prod_mor := fun Q fQ_ => 
+    {| base_fn := fun q => fun i => fQ_ i q |};
+}.
+
+
+Class CategoryCoproduct `{cC : Category C} (A B : C) (A_B : C) := {
+  coprod_obj := A_B;
+  iota_A : A ~> A_B;
+  iota_B : B ~> A_B;
+  coprod_mor : 
+    forall (Q : C) (fA : A ~> Q) (fB : B ~> Q), A_B ~> Q;
+  coprod_mor_prop: 
+    forall (Q : C) (fA : A ~> Q) (fB : B ~> Q),
+    iota_A ∘ (coprod_mor Q fA fB) ≃ fA /\
+    iota_B ∘ (coprod_mor Q fA fB) ≃ fB;
+  coprod_mor_unique : 
+    forall (Q : C) (fA : A ~> Q) (fB : B ~> Q) 
+    (fAB' : A_B ~> Q), 
+    fA ≃ iota_A ∘ fAB' -> fB ≃ iota_B ∘ fAB' -> 
+    fAB' ≃ coprod_mor Q fA fB
+}.
+
+Lemma coprod_mor_unique' `{cC : Category C} {A B A_B : C} 
+  (HAB : CategoryCoproduct A B A_B) {Q} (fA : A ~> Q) (fB : B ~> Q) : 
+  forall (fAB fAB' : A_B ~> Q),
+  iota_A ∘ fAB ≃ fA  -> iota_B ∘ fAB  ≃ fB -> 
+  iota_A ∘ fAB' ≃ fA -> iota_B ∘ fAB' ≃ fB -> 
+  fAB ≃ fAB'.
+Proof.
+  intros.
+  rewrite (coprod_mor_unique Q fA fB) by easy.
+  symmetry;
+  rewrite (coprod_mor_unique Q fA fB) by easy.
+  easy.
+Qed.
+
+Program Definition category_coproduct_unique `{cC : Category C} (A B : C) :
+  forall {A_B A_B'} (HA_B : CategoryCoproduct A B A_B) 
+  (HA_B' : CategoryCoproduct A B A_B'), Isomorphism A_B A_B' :=
+  fun A_B A_B' HA_B HA_B' =>
+  {|
+    forward := HA_B.(coprod_mor) A_B' iota_A iota_B;
+    reverse := HA_B'.(coprod_mor) A_B iota_A iota_B;
+  |}.
+Next Obligation.
+  split; eapply (coprod_mor_unique' _ iota_A iota_B); rewrite <- 1?assoc.
+  1,5: rewrite 2!(proj1 (coprod_mor_prop _ _ _)); easy.
+  1,4: rewrite 2!(proj2 (coprod_mor_prop _ _ _)); easy.
+  all: rewrite right_unit; easy.
+Qed.
+
+Class CategoryBigCoprod `{cC : Category C} {J : Type} 
+  (obj : J -> C) (coprod_J : C) := {
+  big_coprod_obj := coprod_J;
+  iota_i : forall i, obj i ~> coprod_J;
+  big_coprod_mor : 
+    forall (Q : C) (fQ_ : forall i, obj i ~> Q), coprod_J ~> Q;
+  big_coprod_mor_prop: 
+    forall (Q : C) (fQ_ : forall i, obj i ~> Q),
+    forall i, 
+    iota_i i ∘ (big_coprod_mor Q fQ_) ≃ fQ_ i;
+  big_coprod_mor_unique : 
+    forall (Q : C) (fQ_ : forall i, obj i ~> Q)
+    (fAB' : coprod_J ~> Q), 
+    (forall i, fQ_ i ≃ iota_i i ∘ fAB') ->
+    fAB' ≃ big_coprod_mor Q fQ_
+}.
+
+Inductive big_sum {J} (obj : J -> Setoid) :=
+  | in_i i (a : obj i) : big_sum obj.
+
+Arguments in_i {_ _} _ _.
+
+Inductive big_sum_relation {J} (obj : J -> Setoid) : relation (big_sum obj) :=
+  | rel_i (i : J) (a b : obj i) (Hab : (obj i).(s_equiv) a b) 
+    : big_sum_relation obj (in_i i a) (in_i i b)
+  | rel_trans (ia jb kc : big_sum obj) : 
+    big_sum_relation obj ia jb -> big_sum_relation obj jb kc ->
+    big_sum_relation obj ia kc.
+
+Require Import Coq.Program.Equality.
+  
+  
+
+
+#[export, program] Instance big_setoid_sum {J} (obj : J -> Setoid) : Setoid := {
+  base_type := big_sum obj;
+  s_equiv := big_sum_relation obj;
+}.
+Next Obligation.
+  intros J obj [i a]. 
+  constructor; solve_morphisms.
+Qed.
+Next Obligation.
+  intros J obj [i a] [j b] Hab.
+  induction Hab; subst.
+  - apply rel_i; easy.
+  - eapply rel_trans; eassumption.
+Qed.
+Next Obligation.
+  intros; intros ? **.
+  eapply rel_trans; eauto.
+Qed.
+
+
+#[export, program] Instance StdBigCoprod {J} {obj : J -> Setoid} : 
+  CategoryBigCoprod obj (big_setoid_sum obj) := {
+  iota_i := fun i => {| base_fn := fun oi => in_i i oi : big_setoid_sum obj |};
+  big_coprod_mor := fun Q fQ_ => {| base_fn := fun oi => match oi with
+  | in_i i ai => fQ_ i ai
+  end |};
+}.
+Next Obligation.
+  intros. simpl.
+  induction H.
+  - apply fQ_; easy.
+  - rewrite IHbig_sum_relation1, IHbig_sum_relation2.
+    easy.
+Qed.
+Next Obligation.
+  __setup_solve_morphisms.
+  intros J obj Q fQ_ fAB H x.
+  induction x.
+  rewrite H.
+  easy.
+Qed.
+
+Reserved Notation "A ∏ B" (at level 40).
+Reserved Notation "f @∏ g" (at level 40).
+
+Class Category_with_Products {C} (cC : Category C) := {
+  cat_prod : C -> C -> C
+    where "A ∏ B" := (cat_prod A B);
+  cat_prod_product : forall {A B}, CategoryProduct A B (A ∏ B);
+  cat_mor_prod : 
+    forall {A A' B B'} (fA : A ~> B) (fB : A' ~> B'), 
+      A ∏ A' ~> B ∏ B' := fun A A' B B' fA fB =>
+      cat_prod_product.(prod_mor) 
+        (A ∏ A') (p_A ∘ fA) (p_B ∘ fB)
+    where "f @∏ g" := (cat_mor_prod f g);
+}.
+
+Notation "A ∏ B" := (cat_prod A B) (at level 40).
+Notation "f @∏ g" := (cat_mor_prod f g) (at level 40).
+
+#[program, export] Instance Category_with_Products_of_CartesianMonoidalCategory {C cC mC}
+  (ccc : @CartesianMonoidalCategory C cC mC) : Category_with_Products cC := {|
+  cat_prod := mC.(tensor).(obj_bimap);
+  cat_prod_product := tensor_cartesian;
+|}.
+
+Coercion Category_with_Products_of_CartesianMonoidalCategory :
+  CartesianMonoidalCategory >-> Category_with_Products.
+
+
+Reserved Notation "'λ' g" (at level 20).
+Class CategoryExponential `{cC : Category C} {pC : Category_with_Products cC}
+  (A B A_B : C) := {
+  exp_obj := A_B;
+  eval_mor : A_B ∏ B ~> A;
+  eval_mor_transpose : forall {M : C} (f : M ∏ B ~> A), 
+    M ~> A_B
+    where "'λ' g" := (eval_mor_transpose g);
+  eval_mor_transpose_prop : forall (M : C) (f : M ∏ B ~> A),
+    f ≃ (λ f @∏ id_ B) ∘ eval_mor;
+  eval_mor_transpose_unique : forall (M : C) (f : M ∏ B ~> A)
+    (lf' : M ~> A_B), f ≃ (lf' @∏ id_ B) ∘ eval_mor -> λ f ≃ lf';
+}.
+
+#[program, export] Instance MorphismSetoid (A B : Setoid) : Setoid := {
+  base_type := A → B;
+  s_equiv := mor_equiv;
+}.
+
+#[program, export] Instance StdExponential {A B : Setoid} :
+  CategoryExponential A B (MorphismSetoid B A) := {
+  eval_mor := {| base_fn := fun fb => let (f, b) := fb in f b |};
+  eval_mor_transpose := fun M f => {| base_fn := fun m =>
+  {| base_fn := fun b => f (m, b) |} |};
+}.
+
+
+
+Class Cone {C D} {cC : Category C} {cD : Category D} 
+  (F : Functor cD cC) := {
+  cone_obj : C;
+  cone_mor : forall (d : D), cone_obj ~> F d;
+  cone_mor_prop : forall {d d' : D} (f : d ~> d'),
+    cone_mor d ∘ F @ f ≃ cone_mor d';
+}.
+
+Coercion cone_mor : Cone >-> Funclass.
+
+Reserved Notation "'lim' F" (at level 30).
+
+Class Limit {C D} {cC : Category C} {cD : Category D} 
+  (F : Functor cD cC) := {
+  limit_cone : Cone F;
+  limit_cone_factor :
+    forall (N : Cone F), N.(cone_obj) ~> limit_cone.(cone_obj);
+  limit_cone_factor_prop : forall (N : Cone F) (d : D),
+    limit_cone_factor N ∘ limit_cone d ≃ N d;
+  limit_cone_factor_unique : forall (N : Cone F) 
+    (f' : N.(cone_obj) ~> limit_cone.(cone_obj)),
+    (forall (d : D), f' ∘ limit_cone d ≃ N d) -> f' ≃ limit_cone_factor N;
+}.
+
+Lemma limit_cone_factor_unique' {C D} {cC : Category C} {cD : Category D} 
+  {F : Functor cD cC} (L : Limit F) : forall (N : Cone F) 
+  (f f' : N.(cone_obj) ~> L.(limit_cone).(cone_obj)),
+  (forall (d : D), f ∘ limit_cone d ≃ N d) -> 
+  (forall (d : D), f' ∘ limit_cone d ≃ N d) -> 
+  f ≃ f'.
+Proof.
+  intros.
+  rewrite limit_cone_factor_unique by easy.
+  symmetry.
+  rewrite limit_cone_factor_unique by easy.
+  easy.
+Qed.
+
+Coercion limit_cone : Limit >-> Cone.
+
+Notation "'lim' F" := (limit_cone (F:=F)).(cone_obj) (at level 30).
+
+#[program] Definition limit_unique {C D} {cC : Category C} {cD : Category D} 
+  {F : Functor cD cC} (L L' : Limit F) : L.(cone_obj) <~> L'.(cone_obj) := {|
+    forward := L'.(limit_cone_factor) L;
+    reverse := L.(limit_cone_factor) L'
+  |}.
+Next Obligation.
+  split; (apply limit_cone_factor_unique'; 
+    [| intros; rewrite left_unit; easy]);
+  intros; rewrite assoc, 2!limit_cone_factor_prop; easy.
+Qed.
+
+
+Class Cocone {C D} {cC : Category C} {cD : Category D} 
+  (F : Functor cD cC) := {
+  cocone_obj : C;
+  cocone_mor : forall (d : D), F d ~> cocone_obj;
+  cocone_mor_prop : forall {d d' : D} (f : d ~> d'),
+    F @ f ∘ cocone_mor d' ≃ cocone_mor d;
+}.
+
+Coercion cocone_mor : Cocone >-> Funclass.
+
+Reserved Notation "'colim' F" (at level 30).
+
+Class Colimit {C D} {cC : Category C} {cD : Category D} 
+  (F : Functor cD cC) := {
+  colimit_cocone : Cocone F;
+  colimit_cocone_factor : forall (N : Cocone F), 
+    colimit_cocone.(cocone_obj) ~> N.(cocone_obj);
+  colimit_cocone_factor_prop : forall (N : Cocone F) (d : D),
+    colimit_cocone d ∘ colimit_cocone_factor N ≃ N d;
+  colimit_cocone_factor_unique : forall (N : Cocone F) 
+    (f' : colimit_cocone.(cocone_obj) ~> N.(cocone_obj)),
+      (forall (d : D), colimit_cocone d ∘ f' ≃ N d) -> 
+      f' ≃ colimit_cocone_factor N;
+}.
+
+Lemma colimit_cocone_factor_unique' {C D} {cC : Category C} {cD : Category D} 
+  {F : Functor cD cC} (L : Colimit F) : forall (N : Cocone F) 
+  (f f' : L.(colimit_cocone).(cocone_obj) ~> N.(cocone_obj)),
+  (forall (d : D), colimit_cocone d ∘ f ≃ N d) -> 
+  (forall (d : D), colimit_cocone d ∘ f' ≃ N d) -> 
+  f ≃ f'.
+Proof.
+  intros.
+  rewrite colimit_cocone_factor_unique by easy.
+  symmetry.
+  rewrite colimit_cocone_factor_unique by easy.
+  easy.
+Qed.
+
+Coercion colimit_cocone : Colimit >-> Cocone.
+
+Notation "'colim' F" := (colimit_cocone (F:=F)).(cocone_obj) (at level 30).
+
+#[program] Definition colimit_unique {C D} {cC : Category C} {cD : Category D} 
+  {F : Functor cD cC} (L L' : Colimit F) : L.(cocone_obj) <~> L'.(cocone_obj) := {|
+    forward := L.(colimit_cocone_factor) L';
+    reverse := L'.(colimit_cocone_factor) L
+  |}.
+Next Obligation.
+  split; (apply colimit_cocone_factor_unique'; 
+    [| intros; rewrite right_unit; easy]);
+  intros; rewrite <- assoc, 2!colimit_cocone_factor_prop; easy.
+Qed.
+
+
+Class Category_with_Small_Limits {C} (cC : Category C) := {
+  take_set_limit : forall {D : Set} (cD : Category D) (F : Functor cD cC), Limit F;
+}.
+
+Class Category_with_Limits {C} (cC : Category C) := {
+  take_limit : forall {D : Type} (cD : Category D) (F : Functor cD cC), Limit F;
+}.
+
+#[export, program] Instance std_limit_setoid 
+  {D} {cD : Category D} (F : Functor cD Std) : Setoid := {
+  base_type := { s : big_setoid_prod F.(obj_map) | 
+    forall (d d' : D) (f : d ~> d'), (F @ f) (s d) ≡ s d' };
+  s_equiv := fun sP s'P => let (s, _) := sP in let (s', _) := s'P in 
+    s ≡ s';
+}.
+
+#[export, program] Instance std_limit_setoid_cone_mor 
+  {D} {cD : Category D} (F : Functor cD Std) :
+  forall (d : D), std_limit_setoid F → F d := fun d => {|
+  base_fn := fun sP => let (s, _) := sP in s d
+|}.
+
+#[export, program] Instance StdLimitCone {D} {cD : Category D} (F : Functor cD Std) 
+  : Cone F := {
+  cone_obj := std_limit_setoid F;
+  cone_mor := std_limit_setoid_cone_mor F;
+  (* cone_mor_prop := fun d d' => typ_limit_obj_cone_mor_prop F; *)
+}.  
+
+#[export, program] Instance StdLimit {D} {cD : Category D} (F : Functor cD Std) 
+  : Limit F := {
+  limit_cone := StdLimitCone F;
+  limit_cone_factor := fun N => {| 
+    base_fn := fun n : N.(cone_obj) => 
+      exist _ (fun d : D => N d n) _ : std_limit_setoid F |}
+}.
+Next Obligation.
+  __setup_solve_morphisms.
+  __process_solve_morphisms.
+  (* rewrite <- H. *)
+  destruct (f' x) as [s P] eqn:e.
+  intros i.
+  rewrite <- H.
+  rewrite e.
+  easy.
+Qed.
+
+
+
+Inductive make_equiv {A} (R : relation A) : relation A :=
+  | make_rel {a b : A} : R a b -> make_equiv R a b
+  | make_refl (a : A) : make_equiv R a a
+  | make_sym {a b : A} : make_equiv R a b -> make_equiv R b a
+  | make_trans {a b c : A} : 
+      make_equiv R a b -> make_equiv R b c ->
+      make_equiv R a c.
+
+#[export] Instance make_equiv_equivalance {A} (R : relation A) :
+  Equivalence (make_equiv R) := {
+  Equivalence_Reflexive := @make_refl A R;
+  Equivalence_Symmetric := @make_sym A R;
+  Equivalence_Transitive := @make_trans A R;
+}.
+
+Definition std_colimit_rel {D} {cD : Category D} (F : Functor cD Std) :
+  relation (big_setoid_sum F.(obj_map)) := 
+    make_equiv (
+      fun (ia jb : big_setoid_sum F.(obj_map))
+        => let (i, a) := ia in let (j, b) := jb in 
+        exists f : i ~> j, (F @ f) a ≡ b
+  ).
+
+(* Obligation Tactic := idtac. *)
+
+#[export, program] Instance std_colimit_setoid 
+  {D} {cD : Category D} (F : Functor cD Std) : Setoid := {
+  base_type := big_setoid_sum F.(obj_map);
+  s_equiv := std_colimit_rel F;
+}.
+
+
+#[export, program] Instance std_colimit_setoid_cocone_mor 
+  {D} {cD : Category D} (F : Functor cD Std) :
+  forall (d : D), F d → std_colimit_setoid F := fun d => {|
+  base_fn := fun a => in_i d a
+|}.
+
+#[export, program] Instance StdColimitCocone {D} {cD : Category D} (F : Functor cD Std) 
+  : Cocone F := {
+  cocone_obj := std_colimit_setoid F;
+  cocone_mor := std_colimit_setoid_cocone_mor F;
+  (* cone_mor_prop := fun d d' => typ_limit_obj_cone_mor_prop F; *)
+}.
+Next Obligation. 
+  simpl.
+  intros.
+  intros x.
+  simpl.
+  apply make_sym.
+  apply make_rel.
+  exists f.
+  easy.
+Qed.
+
+#[export, program] Instance StdColimit {D} {cD : Category D} (F : Functor cD Std) 
+  : Colimit F := {
+  colimit_cocone := StdColimitCocone F;
+  colimit_cocone_factor := fun N => {| 
+    base_fn := fun ia : big_setoid_sum F => let (i, a) := ia in 
+      N.(cocone_mor) i a |}
+}.
+Next Obligation.
+  __setup_solve_morphisms.
+  __process_solve_morphisms.
+  
+  dependent induction H.
+  destruct a as [i a];
+  destruct b as [j b].
+  - destruct H as [f Hf].
+    epose proof (N.(cocone_mor_prop) f) as HN.
+    revert HN;
+    __setup_solve_morphisms;
+    intros HN.
+    rewrite <- HN, Hf.
+    easy.
+  - easy.
+  - rewrite IHmake_equiv.
+    easy.
+  - etransitivity; eauto.
+Qed.
+Next Obligation.
+  __setup_solve_morphisms.
+  intros D cD F N f' Hf'.
+  intros [i a].
+  easy.
+Qed.
+
+  
+
diff --git a/examples/ZXExample.v b/examples/ZXExample.v
index 1fa3dd1..a7c3c93 100644
--- a/examples/ZXExample.v
+++ b/examples/ZXExample.v
@@ -3,7 +3,20 @@ Require Import Setoid.
 From VyZX Require Import CoreData.
 From VyZX Require Import CoreRules.
 From VyZX Require Import PermutationRules.
-From ViCaR Require Export CategoryTypeclass.
+
+(* From ViCaR Require Import Category (Category, Bifunctor, NaturalBiIsomorphism, Isomorphism).
+From ViCaR Require Import Monoidal (MonoidalCategory).
+From ViCaR Require Import BraidedMonoidal (BraidedMonoidalCategory).
+From ViCaR Require Import SymmetricMonoidal (SymmetricMonoidalCategory).
+From ViCaR Require Import Dagger (DaggerCategory).
+From ViCaR Require Import DaggerMonoidal (DaggerMonoidalCategory). *)
+
+From ViCaR Require CategoryTypeclass.
+Import -(notations) CategoryTypeclass.
+
+(* From ViCaR Require Import CategoryTypeclass (Category, MonoidalCategory, 
+BraidedMonoidalCategory, SymmetricMonoidalCategory, DaggerBraidedMonoidalCategory, 
+DaggerCategory, DaggerSymmetricMonoidalCategory). *)
 
 
 Lemma proportional_equiv {n m : nat} : equivalence (ZX n m) proportional.
@@ -191,7 +204,7 @@ Definition ZXTensorBiFunctor : Bifunctor ZXCategory ZXCategory ZXCategory := {|
   morphism_bicompat := @stack_simplify;
 |}.
 
-#[export] Instance ZXMonoidalCategory : MonoidalCategory nat := {
+#[export] Instance ZXMonoidalCategory : MonoidalCategory ZXCategory := {
   tensor := ZXTensorBiFunctor;
   
   associator := fun n m o => {|