diff --git a/libs/agda-stdlib b/libs/agda-stdlib
index 5c12b38..ac331fc 160000
--- a/libs/agda-stdlib
+++ b/libs/agda-stdlib
@@ -1 +1 @@
-Subproject commit 5c12b38a3a6ecb4d7699dcbe828fb1664151c3bb
+Subproject commit ac331fc38ca05f85dfebc57eb1259ba2ea0e50d5
diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index 24ba6aa..cbea4fa 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -112,7 +112,7 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
     --
     -- [HoTT §9.1.4]
     idToIso : (A B : Object) → A ≡ B → A ≊ B
-    idToIso A B eq = subst eq (idIso A)
+    idToIso A B eq = subst {P = λ X → A ≊ X} eq (idIso A)
 
     Univalent : Set (ℓa ⊔ ℓb)
     Univalent = {A B : Object} → isEquiv (A ≡ B) (A ≊ B) (idToIso A B)