Update theories/Homotopy/ClassifyingSpace.v

Co-authored-by: Dan Christensen <[email protected]>

theories/Homotopy/ClassifyingSpace.v

@@ -581,8 +581,7 @@ Proof.
     rapply pequiv_pclassifyingspace_pi1. }
   snrapply Build_NatEquiv.
   1: intro; exact pequiv_ptr_rec.
-  rapply (@is1natural_prewhisker _ _ _
-            (opyon (pTr 1 X)) (opyon X) B _ _ _ _ _ _ _ _ _ _ (opyoneda _ _ _)).
+  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. *)