diff --git a/test/WildCat/Opposite.v b/test/WildCat/Opposite.v
index f505a900772..ffd45c46ad0 100644
--- a/test/WildCat/Opposite.v
+++ b/test/WildCat/Opposite.v
@@ -1,11 +1,22 @@
-From HoTT Require Import Basics WildCat.Core WildCat.Opposite.
+From HoTT Require Import Basics WildCat.Core WildCat.Opposite WildCat.Equiv.
 
-(* Opposites are (almost) definitionally involutive. *)
+(** * Opposites are definitionally involutive. *)
 
 Definition test1 A : A = (A^op)^op :> Type := 1.
-Definition test2 A `{x : IsGraph A} : x = isgraph_op (A := A^op) := 1.
-Definition test3 A `{x : Is01Cat A} : x = is01cat_op (A := A^op) := 1.
-Definition test4 A `{x : Is2Graph A} : x = is2graph_op (A := A^op) := 1.
+Definition test2 A `{x : IsGraph A} : x = @isgraph_op A^op (@isgraph_op A x) := 1.
+Definition test3 A `{x : Is01Cat A} : x = @is01cat_op A^op _ (@is01cat_op A _ x) := 1.
+Definition test4 A `{x : Is2Graph A} : x = @is2graph_op A^op _ (@is2graph_op A _ x) := 1.
+Definition test5 A `{x : Is1Cat A} : x = @is1cat_op A^op _ _ _ (@is1cat_op A _ _ _ x) := 1.
 
-(** Is1Cat is not definitionally involutive. *)
-Fail Definition test4 A `{x : Is1Cat A} : x = is1cat_op (A := A^op) := 1.
+(** * [core] only partially commutes with taking the opposite category. *)
+Definition core1 A `{HasEquivs A} : (core A)^op = core A^op :> Type := 1.
+Definition core2 A `{HasEquivs A} : isgraph_op (A:=core A) = isgraph_core (A:=A^op) := 1.
+Definition core3 A `{HasEquivs A} : is01cat_op (A:=core A) = is01cat_core (A:=A^op) := 1.
+Definition core4 A `{HasEquivs A} : is2graph_op (A:=core A) = is2graph_core (A:=A^op) := 1.
+
+(** This also passes, but we comment it out as it is slow.  When uncommented, to save time, we end with [Admitted.] instead of [Defined.] *)
+(*
+Definition core5 A `{HasEquivs A} : is1cat_op (A:=core A) = is1cat_core (A:=A^op).
+  Time reflexivity. (* ~6s *)
+Admitted.
+*)
diff --git a/theories/Algebra/AbSES/Core.v b/theories/Algebra/AbSES/Core.v
index 8b0f9dda33a..2601b0ac0b0 100644
--- a/theories/Algebra/AbSES/Core.v
+++ b/theories/Algebra/AbSES/Core.v
@@ -275,7 +275,7 @@ Global Instance is2graph_abses
 Global Instance is1cat_abses {A B : AbGroup@{u}}
   : Is1Cat (AbSES B A).
 Proof.
-  snrapply Build_Is1Cat.
+  snrapply Build_Is1Cat'.
   1: intros ? ?; apply is01cat_abses_path_data.
   1: intros ? ?; apply is0gpd_abses_path_data.
   3-5: cbn; reflexivity.
diff --git a/theories/Algebra/Rings/Module.v b/theories/Algebra/Rings/Module.v
index beba2495b49..d2b8b5d4ac3 100644
--- a/theories/Algebra/Rings/Module.v
+++ b/theories/Algebra/Rings/Module.v
@@ -269,7 +269,7 @@ Global Instance is2graph_leftmodule {R : Ring} : Is2Graph (LeftModule R)
 
 Global Instance is1cat_leftmodule {R : Ring} : Is1Cat (LeftModule R).
 Proof.
-  snrapply Build_Is1Cat.
+  snrapply Build_Is1Cat'.
   - intros M N; rapply is01cat_induced.
   - intros M N; rapply is0gpd_induced.
   - intros M N L h.
diff --git a/theories/Algebra/Universal/Homomorphism.v b/theories/Algebra/Universal/Homomorphism.v
index 4a05d4f462b..53e2e47189d 100644
--- a/theories/Algebra/Universal/Homomorphism.v
+++ b/theories/Algebra/Universal/Homomorphism.v
@@ -190,6 +190,7 @@ Global Instance is1cat_strong_algebra `{Funext} (σ : Signature)
 Proof.
   rapply Build_Is1Cat_Strong.
   - intros. apply assoc_homomorphism_compose.
+  - intros. symmetry; apply assoc_homomorphism_compose.
   - intros. apply left_id_homomorphism_compose.
   - intros. apply right_id_homomorphism_compose.
 Defined.
diff --git a/theories/Homotopy/SuccessorStructure.v b/theories/Homotopy/SuccessorStructure.v
index 49b8752b866..c0659af486e 100644
--- a/theories/Homotopy/SuccessorStructure.v
+++ b/theories/Homotopy/SuccessorStructure.v
@@ -217,7 +217,8 @@ Defined.
 
 Global Instance is1cat_ss : Is1Cat SuccStr.
 Proof.
-  srapply Build_Is1Cat.
+  snrapply Build_Is1Cat'.
+  1,2: exact _.
   - intros X Y Z g.
     snrapply Build_Is0Functor.
     intros f h p.
diff --git a/theories/Pointed/Core.v b/theories/Pointed/Core.v
index 488aeb2792a..6dfe6452a82 100644
--- a/theories/Pointed/Core.v
+++ b/theories/Pointed/Core.v
@@ -570,7 +570,8 @@ Defined.
 (** pType is a 1-coherent 1-category *)
 Global Instance is1cat_ptype : Is1Cat pType.
 Proof.
-  econstructor.
+  snrapply Build_Is1Cat'.
+  1, 2: exact _.
   - intros A B C h; rapply Build_Is0Functor.
     intros f g p; cbn.
     apply pmap_postwhisker; assumption.
@@ -602,7 +603,8 @@ Definition path_zero_morphism_pconst (A B : pType)
 (** pForall is a 1-category *)
 Global Instance is1cat_pforall (A : pType) (P : pFam A) : Is1Cat (pForall A P) | 10.
 Proof.
-  econstructor.
+  snrapply Build_Is1Cat'.
+  1, 2: exact _.
   - intros f g h p; rapply Build_Is0Functor.
     intros q r s. exact (phomotopy_postwhisker s p).
   - intros f g h p; rapply Build_Is0Functor.
diff --git a/theories/WildCat/Core.v b/theories/WildCat/Core.v
index 3d9ef05c3af..7d250535bf3 100644
--- a/theories/WildCat/Core.v
+++ b/theories/WildCat/Core.v
@@ -102,6 +102,8 @@ Class Is1Cat (A : Type) `{!IsGraph A, !Is2Graph A, !Is01Cat A} :=
   is0functor_precomp : forall (a b c : A) (f : a $-> b), Is0Functor (cat_precomp c f) ;
   cat_assoc : forall (a b c d : A) (f : a $-> b) (g : b $-> c) (h : c $-> d),
     (h $o g) $o f $== h $o (g $o f);
+  cat_assoc_opp : forall (a b c d : A) (f : a $-> b) (g : b $-> c) (h : c $-> d),
+    h $o (g $o f) $== (h $o g) $o f;
   cat_idl : forall (a b : A) (f : a $-> b), Id b $o f $== f;
   cat_idr : forall (a b : A) (f : a $-> b), f $o Id a $== f;
 }.
@@ -111,13 +113,23 @@ Global Existing Instance is0gpd_hom.
 Global Existing Instance is0functor_postcomp.
 Global Existing Instance is0functor_precomp.
 Arguments cat_assoc {_ _ _ _ _ _ _ _ _} f g h.
+Arguments cat_assoc_opp {_ _ _ _ _ _ _ _ _} f g h.
 Arguments cat_idl {_ _ _ _ _ _ _} f.
 Arguments cat_idr {_ _ _ _ _ _ _} f.
 
-Definition cat_assoc_opp {A : Type} `{Is1Cat A}
-           {a b c d : A} (f : a $-> b) (g : b $-> c) (h : c $-> d)
-  : h $o (g $o f) $== (h $o g) $o f
-  := (cat_assoc f g h)^$.
+(** An alternate constructor that doesn't require the proof of [cat_assoc_opp].  This can be used for defining examples of wild categories, but shouldn't be used for the general theory of wild categories. *)
+Definition Build_Is1Cat' (A : Type) `{!IsGraph A, !Is2Graph A, !Is01Cat A}
+  (is01cat_hom : forall a b : A, Is01Cat (a $-> b))
+  (is0gpd_hom : forall a b : A, Is0Gpd (a $-> b))
+  (is0functor_postcomp : forall (a b c : A) (g : b $-> c), Is0Functor (cat_postcomp a g))
+  (is0functor_precomp : forall (a b c : A) (f : a $-> b), Is0Functor (cat_precomp c f))
+  (cat_assoc : forall (a b c d : A) (f : a $-> b) (g : b $-> c) (h : c $-> d),
+      h $o g $o f $== h $o (g $o f))
+  (cat_idl : forall (a b : A) (f : a $-> b), Id b $o f $== f)
+  (cat_idr : forall (a b : A) (f : a $-> b), f $o Id a $== f)
+  : Is1Cat A
+  := Build_Is1Cat A _ _ _ is01cat_hom is0gpd_hom is0functor_postcomp is0functor_precomp
+      cat_assoc (fun a b c d f g h => (cat_assoc a b c d f g h)^$) cat_idl cat_idr.
 
 (** Whiskering and horizontal composition of 2-cells. *)
 
@@ -175,19 +187,18 @@ Class Is1Cat_Strong (A : Type)`{!IsGraph A, !Is2Graph A, !Is01Cat A} :=
   cat_assoc_strong : forall (a b c d : A)
     (f : a $-> b) (g : b $-> c) (h : c $-> d),
     (h $o g) $o f = h $o (g $o f) ;
+  cat_assoc_opp_strong : forall (a b c d : A)
+    (f : a $-> b) (g : b $-> c) (h : c $-> d),
+    h $o (g $o f) = (h $o g) $o f ;
   cat_idl_strong : forall (a b : A) (f : a $-> b), Id b $o f = f ;
   cat_idr_strong : forall (a b : A) (f : a $-> b), f $o Id a = f ;
 }.
 
 Arguments cat_assoc_strong {_ _ _ _ _ _ _ _ _} f g h.
+Arguments cat_assoc_opp_strong {_ _ _ _ _ _ _ _ _} f g h.
 Arguments cat_idl_strong {_ _ _ _ _ _ _} f.
 Arguments cat_idr_strong {_ _ _ _ _ _ _} f.
 
-Definition cat_assoc_opp_strong {A : Type} `{Is1Cat_Strong A}
-           {a b c d : A} (f : a $-> b) (g : b $-> c) (h : c $-> d)
-  : h $o (g $o f) = (h $o g) $o f
-  := (cat_assoc_strong f g h)^.
-
 Global Instance is1cat_is1cat_strong (A : Type) `{Is1Cat_Strong A}
   : Is1Cat A | 1000.
 Proof.
@@ -198,6 +209,7 @@ Proof.
   - apply is0functor_postcomp_strong.
   - apply is0functor_precomp_strong.
   - intros; apply GpdHom_path, cat_assoc_strong.
+  - intros; apply GpdHom_path, cat_assoc_opp_strong.
   - intros; apply GpdHom_path, cat_idl_strong.
   - intros; apply GpdHom_path, cat_idr_strong.
 Defined.
@@ -247,6 +259,7 @@ Global Instance is1cat_strong_hasmorext {A : Type} `{HasMorExt A}
 Proof.
   rapply Build_Is1Cat_Strong; hnf; intros; apply path_hom.
   + apply cat_assoc.
+  + apply cat_assoc_opp.
   + apply cat_idl.
   + apply cat_idr.
 Defined.
diff --git a/theories/WildCat/Displayed.v b/theories/WildCat/Displayed.v
index 566801eae04..4f04addf00d 100644
--- a/theories/WildCat/Displayed.v
+++ b/theories/WildCat/Displayed.v
@@ -106,6 +106,11 @@ Class IsD1Cat {A : Type} `{Is1Cat A}
                (f' : DHom f a' b') (g' : DHom g b' c') (h' : DHom h c' d'),
                DHom (cat_assoc f g h) ((h' $o' g') $o' f')
                (h' $o' (g' $o' f'));
+  dcat_assoc_opp : forall {a b c d : A} {f : a $-> b} {g : b $-> c} {h : c $-> d}
+               {a' : D a} {b' : D b} {c' : D c} {d' : D d}
+               (f' : DHom f a' b') (g' : DHom g b' c') (h' : DHom h c' d'),
+               DHom (cat_assoc_opp f g h) (h' $o' (g' $o' f'))
+               ((h' $o' g') $o' f');
   dcat_idl : forall {a b : A} {f : a $-> b} {a' : D a} {b' : D b}
              (f' : DHom f a' b'), DHom (cat_idl f) (DId b' $o' f') f';
   dcat_idr : forall {a b : A} {f : a $-> b} {a' : D a} {b' : D b}
@@ -117,13 +122,6 @@ Global Existing Instance isd0gpd_hom.
 Global Existing Instance isd0functor_postcomp.
 Global Existing Instance isd0functor_precomp.
 
-Definition dcat_assoc_opp {A : Type} {D : A -> Type} `{IsD1Cat A D}
-  {a b c d : A}  {f : a $-> b} {g : b $-> c} {h : c $-> d}
-  {a' : D a} {b' : D b} {c' : D c} {d' : D d}
-  (f' : DHom f a' b') (g' : DHom g b' c') (h' : DHom h c' d')
-  : DHom (cat_assoc_opp f g h) (h' $o' (g' $o' f')) ((h' $o' g') $o' f')
-  := (dcat_assoc f' g' h')^$'.
-
 Definition dcat_postwhisker {A : Type} {D : A -> Type} `{IsD1Cat A D}
   {a b c : A} {f g : a $-> b} {h : b $-> c} {p : f $== g}
   {a' : D a} {b' : D b} {c' : D c} {f' : DHom f a' b'} {g' : DHom g a' b'}
@@ -234,6 +232,8 @@ Proof.
     exact (p $@R f; p' $@R' f').
   - intros [a a'] [b b'] [c c'] [d d'] [f f'] [g g'] [h h'].
     exact (cat_assoc f g h; dcat_assoc f' g' h').
+  - intros [a a'] [b b'] [c c'] [d d'] [f f'] [g g'] [h h'].
+    exact (cat_assoc_opp f g h; dcat_assoc_opp f' g' h').
   - intros [a a'] [b b'] [f f'].
     exact (cat_idl f; dcat_idl f').
   - intros [a a'] [b b'] [f f'].
@@ -275,6 +275,11 @@ Class IsD1Cat_Strong {A : Type} `{Is1Cat_Strong A}
                       (f' : DHom f a' b') (g' : DHom g b' c') (h' : DHom h c' d'),
                       (transport (fun k => DHom k a' d') (cat_assoc_strong f g h)
                       ((h' $o' g') $o' f')) = h' $o' (g' $o' f');
+  dcat_assoc_opp_strong : forall {a b c d : A} {f : a $-> b} {g : b $-> c} {h : c $-> d}
+                      {a' : D a} {b' : D b} {c' : D c} {d' : D d}
+                      (f' : DHom f a' b') (g' : DHom g b' c') (h' : DHom h c' d'),
+                      (transport (fun k => DHom k a' d') (cat_assoc_opp_strong f g h)
+                      (h' $o' (g' $o' f'))) = (h' $o' g') $o' f';
   dcat_idl_strong : forall {a b : A} {f : a $-> b} {a' : D a} {b' : D b}
                     (f' : DHom f a' b'),
                     (transport (fun k => DHom k a' b') (cat_idl_strong f)
@@ -290,6 +295,7 @@ Global Existing Instance isd0gpd_hom_strong.
 Global Existing Instance isd0functor_postcomp_strong.
 Global Existing Instance isd0functor_precomp_strong.
 
+(* If in the future we make a [Build_Is1Cat_Strong'] that lets the user omit the second proof of associativity, this shows how it can be recovered from the original proof:
 Definition dcat_assoc_opp_strong {A : Type} {D : A -> Type} `{IsD1Cat_Strong A D}
   {a b c d : A}  {f : a $-> b} {g : b $-> c} {h : c $-> d}
   {a' : D a} {b' : D b} {c' : D c} {d' : D d}
@@ -300,6 +306,7 @@ Proof.
   apply (moveR_transport_V (fun k => DHom k a' d') (cat_assoc_strong f g h) _ _).
   exact ((dcat_assoc_strong f' g' h')^).
 Defined.
+*)
 
 Global Instance isd1cat_isd1catstrong {A : Type} (D : A -> Type)
   `{IsD1Cat_Strong A D} : IsD1Cat D.
@@ -307,6 +314,8 @@ Proof.
   srapply Build_IsD1Cat.
   - intros a b c d f g h a' b' c' d' f' g' h'.
     exact (DHom_path (cat_assoc_strong f g h) (dcat_assoc_strong f' g' h')).
+  - intros a b c d f g h a' b' c' d' f' g' h'.
+    exact (DHom_path (cat_assoc_opp_strong f g h) (dcat_assoc_opp_strong f' g' h')).
   - intros a b f a' b' f'.
     exact (DHom_path (cat_idl_strong f) (dcat_idl_strong f')).
   - intros a b f a' b' f'.
@@ -321,6 +330,9 @@ Proof.
   - intros aa' bb' cc' dd' [f f'] [g g'] [h h'].
     exact (path_sigma' _
             (cat_assoc_strong f g h) (dcat_assoc_strong f' g' h')).
+  - intros aa' bb' cc' dd' [f f'] [g g'] [h h'].
+    exact (path_sigma' _
+            (cat_assoc_opp_strong f g h) (dcat_assoc_opp_strong f' g' h')).
   - intros aa' bb' [f f'].
     exact (path_sigma' _ (cat_idl_strong f) (dcat_idl_strong f')).
   - intros aa' bb' [f f'].
@@ -506,6 +518,9 @@ Proof.
   - intros ab1 ab2 ab3 ab4 fg1 fg2 fg3.
     intros ab1' ab2' ab3' ab4' [f1' g1'] [f2' g2'] [f3' g3'].
     exact (dcat_assoc f1' f2' f3', dcat_assoc g1' g2' g3').
+  - intros ab1 ab2 ab3 ab4 fg1 fg2 fg3.
+    intros ab1' ab2' ab3' ab4' [f1' g1'] [f2' g2'] [f3' g3'].
+    exact (dcat_assoc_opp f1' f2' f3', dcat_assoc_opp g1' g2' g3').
   - intros ab1 ab2 fg ab1' ab2' [f' g'].
     exact (dcat_idl f', dcat_idl g').
   - intros ab1 ab2 fg ab1' ab2' [f' g'].
diff --git a/theories/WildCat/DisplayedEquiv.v b/theories/WildCat/DisplayedEquiv.v
index 3cd3cf2245f..0492792e574 100644
--- a/theories/WildCat/DisplayedEquiv.v
+++ b/theories/WildCat/DisplayedEquiv.v
@@ -160,7 +160,7 @@ Defined.
 Global Instance dcatie_id {A} {D : A -> Type} `{DHasEquivs A D}
   {a : A} (a' : D a)
   : DCatIsEquiv (DId a')
-  := dcatie_adjointify (DId a') (DId a') (dcat_idl (DId a')) (dcat_idl (DId a')).
+  := dcatie_adjointify (DId a') (DId a') (dcat_idl (DId a')) (dcat_idr (DId a')).
 
 Definition did_cate {A} {D : A -> Type} `{DHasEquivs A D}
   {a : A} (a' : D a)
@@ -205,10 +205,10 @@ Proof.
     refine (_ $@L' (dcate_isretr _ $@R' _) $@' _).
     refine (_ $@L' dcat_idl _ $@' _).
     apply dcate_isretr.
-  - refine (dcat_assoc _ _ _ $@' _).
-    refine (_ $@L' dcat_assoc_opp _ _ _ $@' _).
-    refine (_ $@L' (dcate_issect _ $@R' _) $@' _).
-    refine (_ $@L' dcat_idl _ $@' _).
+  - refine (dcat_assoc_opp _ _ _ $@' _).
+    refine (dcat_assoc _ _ _ $@R' _ $@' _).
+    refine (((_ $@L' dcate_issect _) $@R' _) $@' _).
+    refine ((dcat_idr _ $@R' _) $@' _).
     apply dcate_issect.
 Defined.
 
diff --git a/theories/WildCat/Equiv.v b/theories/WildCat/Equiv.v
index 26ccff63cdf..02bbaa87b6c 100644
--- a/theories/WildCat/Equiv.v
+++ b/theories/WildCat/Equiv.v
@@ -137,7 +137,7 @@ Defined.
 (** The identity morphism is an equivalence *)
 Global Instance catie_id {A} `{HasEquivs A} (a : A)
   : CatIsEquiv (Id a)
-  := catie_adjointify (Id a) (Id a) (cat_idl (Id a)) (cat_idl (Id a)).
+  := catie_adjointify (Id a) (Id a) (cat_idl (Id a)) (cat_idr (Id a)).
 
 Definition id_cate {A} `{HasEquivs A} (a : A)
   : a $<~> a
@@ -177,10 +177,10 @@ Proof.
     refine ((_ $@L (cate_isretr _ $@R _)) $@ _).
     refine ((_ $@L cat_idl _) $@ _).
     apply cate_isretr.
-  - refine (cat_assoc _ _ _ $@ _).
-    refine ((_ $@L cat_assoc_opp _ _ _) $@ _).
-    refine ((_ $@L (cate_issect _ $@R _)) $@ _).
-    refine ((_ $@L cat_idl _) $@ _).
+  - refine (cat_assoc_opp _ _ _ $@ _).
+    refine ((cat_assoc _ _ _ $@R _) $@ _).
+    refine (((_ $@L cate_issect _) $@R _) $@ _).
+    refine ((cat_idr _ $@R _) $@ _).
     apply cate_issect.
 Defined.
 
@@ -226,6 +226,16 @@ Proof.
   - refine (_ $@L compose_cate_funinv g f).
 Defined.
 
+Definition compose_cate_assoc_opp {A} `{HasEquivs A}
+           {a b c d : A} (f : a $<~> b) (g : b $<~> c) (h : c $<~> d)
+  : cate_fun (h $oE (g $oE f)) $== cate_fun ((h $oE g) $oE f).
+Proof.
+  refine (compose_cate_fun h _ $@ _ $@ cat_assoc_opp f g h $@ _ $@
+                           compose_cate_funinv _ f).
+  - refine (_ $@L compose_cate_fun g f).
+  - refine (compose_cate_funinv h g $@R _).
+Defined.
+
 Definition compose_cate_idl {A} `{HasEquivs A}
            {a b : A} (f : a $<~> b)
   : cate_fun (id_cate b $oE f) $== cate_fun f.
@@ -559,6 +569,7 @@ Global Instance is1cat_core {A : Type} `{HasEquivs A}
 Proof.
   rapply Build_Is1Cat.
   - intros; apply compose_cate_assoc.
+  - intros; apply compose_cate_assoc_opp.
   - intros; apply compose_cate_idl.
   - intros; apply compose_cate_idr.
 Defined.
diff --git a/theories/WildCat/Forall.v b/theories/WildCat/Forall.v
index cd000c3ae6d..25a76f84eb2 100644
--- a/theories/WildCat/Forall.v
+++ b/theories/WildCat/Forall.v
@@ -52,6 +52,7 @@ Proof.
     intros f g p a.
     exact (p a $@R h a).
   + intros w x y z f g h a; apply cat_assoc.
+  + intros w x y z f g h a; apply cat_assoc_opp.
   + intros x y f a; apply cat_idl.
   + intros x y f a; apply cat_idr.
 Defined.
diff --git a/theories/WildCat/FunctorCat.v b/theories/WildCat/FunctorCat.v
index 3ea393ef972..7b0a550de5f 100644
--- a/theories/WildCat/FunctorCat.v
+++ b/theories/WildCat/FunctorCat.v
@@ -72,6 +72,8 @@ Proof.
     exact (f a $@R alpha a).
   - intros [F ?] [G ?] [K ?] [L ?] [alpha ?] [gamma ?] [phi ?] a; cbn.
     srapply cat_assoc.
+  - intros [F ?] [G ?] [K ?] [L ?] [alpha ?] [gamma ?] [phi ?] a; cbn.
+    srapply cat_assoc_opp.
   - intros [F ?] [G ?] [alpha ?] a; cbn.
     srapply cat_idl.
   - intros [F ?] [G ?] [alpha ?] a; cbn.
diff --git a/theories/WildCat/Induced.v b/theories/WildCat/Induced.v
index 7635d1ece14..0e9dd18c269 100644
--- a/theories/WildCat/Induced.v
+++ b/theories/WildCat/Induced.v
@@ -57,6 +57,7 @@ Section Induced_category.
     + rapply is0functor_postcomp.
     + rapply is0functor_precomp.
     + rapply cat_assoc.
+    + rapply cat_assoc_opp.
     + rapply cat_idl.
     + rapply cat_idr.
   Defined.
diff --git a/theories/WildCat/Opposite.v b/theories/WildCat/Opposite.v
index a862bdeca1c..1e7e8cf9716 100644
--- a/theories/WildCat/Opposite.v
+++ b/theories/WildCat/Opposite.v
@@ -52,6 +52,7 @@ Proof.
     cbn in *.
     exact (h $@L p).
   - intros a b c d f g h; exact (cat_assoc_opp h g f).
+  - intros a b c d f g h; exact (cat_assoc h g f).
   - intros a b f; exact (cat_idr f).
   - intros a b f; exact (cat_idl f).
 Defined.
@@ -59,8 +60,11 @@ Defined.
 Global Instance is1cat_strong_op A `{Is1Cat_Strong A}
   : Is1Cat_Strong (A ^op).
 Proof.
-  srapply Build_Is1Cat_Strong; unfold op in *; cbn in *.
+  snrapply Build_Is1Cat_Strong.
+  1-4: exact _.
+  all: cbn.
   - intros a b c d f g h; exact (cat_assoc_opp_strong h g f).
+  - intros a b c d f g h; exact (cat_assoc_strong h g f).
   - intros a b f.
     apply cat_idr_strong.
   - intros a b f.
@@ -100,7 +104,7 @@ Global Instance is1functor_op A B (F : A -> B)
   `{Is1Cat A, Is1Cat B, !Is0Functor F, !Is1Functor F}
   : Is1Functor (F : A^op -> B^op).
 Proof.
-  apply Build_Is1Functor; unfold op in *; cbn in *.
+  apply Build_Is1Functor; cbn.
   - intros a b; rapply fmap2.
   - exact (fmap_id F).
   - intros a b c f g; exact (fmap_comp F g f).
@@ -112,16 +116,11 @@ Global Instance is0functor_op' A B (F : A^op -> B^op)
   : Is0Functor (F : A -> B)
   := is0functor_op A^op B^op F.
 
-(** [Is1Cat] structures are not definitionally involutive, so we prove the reverse direction separately. *)
+(** [Is1Cat] structures are also definitionally involutive. *)
 Global Instance is1functor_op' A B (F : A^op -> B^op)
   `{Is1Cat A, Is1Cat B, !Is0Functor (F : A^op -> B^op), Fop2 : !Is1Functor (F : A^op -> B^op)}
-  : Is1Functor (F : A -> B).
-Proof.
-  apply Build_Is1Functor; unfold op in *; cbn.
-  - intros a b; exact (@fmap2 A^op B^op _ _ _ _ _ _ _ _ F _ Fop2 b a).
-  - exact (@fmap_id A^op B^op _ _ _ _ _ _ _ _ F _ Fop2).
-  - intros a b c f g; exact (@fmap_comp A^op B^op _ _ _ _ _ _ _ _ F _ Fop2 _ _ _ g f).
-Defined.
+  : Is1Functor (F : A -> B)
+  := is1functor_op A^op B^op F.
 
 (** Bundled opposite functors *)
 Definition fun01_op (A B : Type) `{IsGraph A} `{IsGraph B}
@@ -150,9 +149,8 @@ Global Instance is1nat_op A B `{Is01Cat A} `{Is1Cat B}
        (alpha : F $=> G) `{!Is1Natural F G alpha}
   : Is1Natural (G : A^op -> B^op) (F : A^op -> B^op) (transformation_op F G alpha).
 Proof.
-  unfold op in *.
+  unfold op.
   unfold transformation_op.
-  cbn.
   intros a b f.
   srapply isnat_tr.
 Defined.
@@ -160,7 +158,7 @@ Defined.
 (** Opposite categories preserve having equivalences. *)
 Global Instance hasequivs_op {A} `{HasEquivs A} : HasEquivs A^op.
 Proof.
-  srapply Build_HasEquivs; intros a b; unfold op in *; cbn.
+  snrapply Build_HasEquivs; intros a b; unfold op in a, b; cbn.
   - exact (b $<~> a).
   - apply CatIsEquiv.
   - apply cate_fun'.
@@ -174,7 +172,7 @@ Proof.
     exact (catie_adjointify f g t s).
 Defined.
 
-Global Instance isequivs_op {A : Type} `{HasEquivs A}
+Global Instance isequiv_op {A : Type} `{HasEquivs A}
        {a b : A} (f : a $-> b) {ief : CatIsEquiv f}
   : @CatIsEquiv A^op _ _ _ _ _ b a f.
 Proof.
@@ -195,8 +193,7 @@ Lemma natequiv_op {A B : Type} `{Is01Cat A} `{HasEquivs B}
 Proof.
   intros [a n].
   snrapply Build_NatEquiv.
-  { intro x.
-    exact (a x). }
+  1: exact a.
   rapply is1nat_op.
 Defined.
 
diff --git a/theories/WildCat/Paths.v b/theories/WildCat/Paths.v
index 63593ac807f..ddab9ab2db2 100644
--- a/theories/WildCat/Paths.v
+++ b/theories/WildCat/Paths.v
@@ -40,7 +40,9 @@ Proof.
     intros q r h.
     exact (whiskerL p h).
   - intros w x y z p q r.
-    exact (concat_p_pp p q r). 
+    exact (concat_p_pp p q r).
+  - intros w x y z p q r.
+    exact (concat_pp_p p q r).
   - intros x y p.
     exact (concat_p1 p).
   - intros x y p.
diff --git a/theories/WildCat/Prod.v b/theories/WildCat/Prod.v
index 4b94a24a9b0..dfa66fbb4e8 100644
--- a/theories/WildCat/Prod.v
+++ b/theories/WildCat/Prod.v
@@ -40,7 +40,7 @@ Defined.
 Global Instance is1cat_prod A B `{Is1Cat A} `{Is1Cat B}
   : Is1Cat (A * B).
 Proof.
-  srapply (Build_Is1Cat).
+  srapply Build_Is1Cat.
   - intros [x1 x2] [y1 y2] [z1 z2] [h1 h2].
     srapply Build_Is0Functor.
     intros [f1 f2] [g1 g2] [p1 p2]; cbn in *.
@@ -52,6 +52,9 @@ Proof.
   - intros [a1 a2] [b1 b2] [c1 c2] [d1 d2] [f1 f2] [g1 g2] [h1 h2].
     cbn in *.
     exact(cat_assoc f1 g1 h1, cat_assoc f2 g2 h2).
+  - intros [a1 a2] [b1 b2] [c1 c2] [d1 d2] [f1 f2] [g1 g2] [h1 h2].
+    cbn in *.
+    exact(cat_assoc_opp f1 g1 h1, cat_assoc_opp f2 g2 h2).
   - intros [a1 a2] [b1 b2] [f1 f2].
     cbn in *.
     exact (cat_idl _, cat_idl _).
diff --git a/theories/WildCat/Sum.v b/theories/WildCat/Sum.v
index 32331dcf618..96564d6ea7f 100644
--- a/theories/WildCat/Sum.v
+++ b/theories/WildCat/Sum.v
@@ -39,25 +39,47 @@ Global Instance is1cat_sum A B `{ Is1Cat A } `{ Is1Cat B}
 Proof.
   snrapply Build_Is1Cat.
   - intros x y.
-    srapply Build_Is01Cat;
-    destruct x as [a1 | b1], y as [a2 | b2];
-    try contradiction; cbn;
-    (apply Id || intros a b c; apply cat_comp).
+    srapply Build_Is01Cat; destruct x as [a1 | b1], y as [a2 | b2].
+    2,3,6,7: contradiction.
+    all: cbn.
+    1,2: exact Id.
+    1,2: intros a b c; apply cat_comp.
   - intros x y; srapply Build_Is0Gpd.
-    destruct x as [a1 | b1], y as [a2 | b2];
-    try contradiction; cbn; intros f g; apply gpd_rev.
+    destruct x as [a1 | b1], y as [a2 | b2].
+    2,3: contradiction.
+    all: cbn; intros f g; apply gpd_rev.
   - intros x y z h; srapply Build_Is0Functor.
     intros f g p.
-    destruct x as [a1 | b1], y as [a2 | b2], z as [a3 | b3];
-    try contradiction; cbn in *; change (f $== g) in p; exact (h $@L p).
+    destruct x as [a1 | b1], y as [a2 | b2].
+    2,3: contradiction.
+    all: destruct z as [a3 | b3].
+    2,3: contradiction.
+    all: cbn in *; change (f $== g) in p; exact (h $@L p).
   - intros x y z h; srapply Build_Is0Functor.
     intros f g p.
-    destruct x as [a1 | b1], y as [a2 | b2], z as [a3 | b3];
-    try contradiction; cbn in *; change (f $== g) in p; exact (p $@R h).
-  - intros [a1 | b1] [a2 | b2] [a3 | b3] [a4 | b4] f g h;
-    try contradiction; cbn; apply cat_assoc.
-  - intros [a1 | b1] [a2 | b2] f; try contradiction;
-    cbn; apply cat_idl.
-  - intros [a1 | b1] [a2 | b2] f; try contradiction;
-    cbn; apply cat_idr.
+    destruct x as [a1 | b1], y as [a2 | b2].
+    2,3: contradiction.
+    all: destruct z as [a3 | b3].
+    2,3: contradiction.
+    all: cbn in *; change (f $== g) in p; exact (p $@R h).
+  - intros [a1 | b1] [a2 | b2].
+    2,3: contradiction.
+    all: intros [a3 | b3].
+    2,3: contradiction.
+    all: intros [a4 | b4].
+    2-3: contradiction.
+    all: intros f g h; cbn; apply cat_assoc.
+  - intros [a1 | b1] [a2 | b2].
+    2,3: contradiction.
+    all: intros [a3 | b3].
+    2,3: contradiction.
+    all: intros [a4 | b4].
+    2-3: contradiction.
+    all: intros f g h; cbn; apply cat_assoc_opp.
+  - intros [a1 | b1] [a2 | b2] f.
+    2, 3: contradiction.
+    all: cbn; apply cat_idl.
+  - intros [a1 | b1] [a2 | b2] f.
+    2, 3: contradiction.
+    all: cbn; apply cat_idr.
 Defined.
diff --git a/theories/WildCat/Universe.v b/theories/WildCat/Universe.v
index c968aa74c75..4de5e402f5c 100644
--- a/theories/WildCat/Universe.v
+++ b/theories/WildCat/Universe.v
@@ -120,6 +120,7 @@ Proof.
   - intros g h p x.
     exact (1 @@ p x).
   - intros ? ? ? ? ? ? ? ?; apply concat_p_pp.
+  - intros ? ? ? ? ? ? ? ?; apply concat_pp_p.
   - intros ? ? ? ?. apply concat_p1.
   - intros ? ? ? ?. apply concat_1p.
 Defined.
diff --git a/theories/WildCat/ZeroGroupoid.v b/theories/WildCat/ZeroGroupoid.v
index 62290fbfef3..ec60178e96a 100644
--- a/theories/WildCat/ZeroGroupoid.v
+++ b/theories/WildCat/ZeroGroupoid.v
@@ -72,6 +72,7 @@ Proof.
     cbn.
     exact (p (f x)).
   - reflexivity. (* Associativity. *)
+  - reflexivity. (* Associativity in opposite direction. *)
   - reflexivity. (* Left identity. *)
   - reflexivity. (* Right identity. *)
 Defined.