From 95a8e82d407167998c90a11e7438ec25010794ca Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Tue, 30 Oct 2018 14:28:09 +0100
Subject: [PATCH] Update agda-stdlib to newer version

---
 libs/agda-stdlib      | 2 +-
 src/Cat/Category.agda | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

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)