diff --git a/theories/Categories/FunctorCategory/Morphisms.v b/theories/Categories/FunctorCategory/Morphisms.v
index e9999aede30..be2cba55ba1 100644
--- a/theories/Categories/FunctorCategory/Morphisms.v
+++ b/theories/Categories/FunctorCategory/Morphisms.v
@@ -110,7 +110,7 @@ Section idtoiso.
   Lemma eta_idtoiso
         (F G : object (C -> D))
         (T : F = G)
-  : Morphisms.idtoiso _ T = idtoiso T.
+  : Category.Morphisms.idtoiso _ T = idtoiso T.
   Proof.
     case T.
     expand; f_ap.