Merge pull request #1740 from herbelin/master+qualifying-idtoiso

Qualifying idtoiso into Category.Morphisms.idtoiso
HoTT · Aug 7, 2023 · c89dc10 · c89dc10
2 parents cca97be + 297229e
commit c89dc10
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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.