diff --git a/theories/Homotopy/ClassifyingSpace.v b/theories/Homotopy/ClassifyingSpace.v
index 20b8ffc532..d4cf92a1b3 100644
--- a/theories/Homotopy/ClassifyingSpace.v
+++ b/theories/Homotopy/ClassifyingSpace.v
@@ -581,7 +581,7 @@ Proof.
     rapply pequiv_pclassifyingspace_pi1. }
   snrapply Build_NatEquiv.
   1: intro; exact pequiv_ptr_rec.
-  rapply is1natural_prewhisker.
+  rapply (is1natural_prewhisker (G:=opyon X) B (opyoneda _ _ _)).
 Defined.
 
 (** The classifying space functor and the fundamental group functor form an adjunction (pType needs to be restricted to the subcategory of 0-connected pTypes). Note that the full adjunction should also be natural in X, but this was not needed yet. *)
diff --git a/theories/WildCat/Adjoint.v b/theories/WildCat/Adjoint.v
index 9e44791f87..5e2800f613 100644
--- a/theories/WildCat/Adjoint.v
+++ b/theories/WildCat/Adjoint.v
@@ -376,7 +376,7 @@ Proof.
     exact (natequiv_prewhisker (A:=A^op) (B:=B^op)
       (natequiv_adjunction_l adj2 y) F). }
   intros x.
-  rapply is1natural_comp.
+  nrapply is1natural_comp.
   + rapply (is1natural_prewhisker G' (natequiv_adjunction_r adj1 x)).
   + rapply is1natural_equiv_adjunction_r.
 Defined.
@@ -393,7 +393,7 @@ Proof.
     refine (natequiv_compose (natequiv_adjunction_l adj _) _).
     rapply (natequiv_postwhisker _ (natequiv_op e)). }
   intros x.
-  rapply is1natural_comp.
+  nrapply is1natural_comp; typeclasses eauto.
 Defined.
 
 (** Replace the right functor in an adjunction by a naturally equivalent one. *)
@@ -408,8 +408,7 @@ Proof.
     refine (natequiv_compose _ (natequiv_adjunction_r adj _)).
     rapply (natequiv_postwhisker _ e). }
   intros y.
-  rapply is1natural_comp.
+  nrapply is1natural_comp.
   2: exact _.
   rapply is1natural_yoneda.
 Defined.
-
diff --git a/theories/WildCat/NatTrans.v b/theories/WildCat/NatTrans.v
index ce2871fa1e..eb47b3c164 100644
--- a/theories/WildCat/NatTrans.v
+++ b/theories/WildCat/NatTrans.v
@@ -66,7 +66,7 @@ Arguments Is1Natural {A B} {isgraph_A}
   F {is0functor_F} G {is0functor_G} alpha : rename.
 Arguments isnat {_ _ _ _ _ _ _ _ _ _ _} alpha {alnat _ _} f : rename.
 Arguments isnat_tr {_ _ _ _ _ _ _ _ _ _ _} alpha {alnat _ _} f : rename.
-
+Hint Mode Is1Natural - - - - - - - - - - - ! : typeclass_instances.
 (** We coerce naturality proofs to their naturality square as the [isnat] projection can be unwieldy in certain situations where the transformation is difficult to write down. This allows for the naturality proof to be used directly. *)
 Coercion isnat : Is1Natural >-> Funclass.