diff --git a/libs/agda-stdlib b/libs/agda-stdlib
index fbd8ba7..4493cf2 160000
--- a/libs/agda-stdlib
+++ b/libs/agda-stdlib
@@ -1 +1 @@
-Subproject commit fbd8ba7ea84c4b643fd08797b4031b18a59f561d
+Subproject commit 4493cf249a1648be2ad365fe94ece337bfbcb5d9
diff --git a/libs/cubical b/libs/cubical
index 5b35333..4e5d43a 160000
--- a/libs/cubical
+++ b/libs/cubical
@@ -1 +1 @@
-Subproject commit 5b35333dbbd8fa523e478c1cfe60657321ca38fe
+Subproject commit 4e5d43a9c75286b3a8750567d75a930674d7720d
diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index 1561aab..749ba42 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -137,11 +137,10 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
       Univalent[Contr] : Set _
       Univalent[Contr] = ∀ A → isContr (Σ[ X ∈ Object ] A ≊ X)
 
-      -- From: Thierry Coquand <Thierry.Coquand@cse.gu.se>
-      -- Date: Wed, Mar 21, 2018 at 3:12 PM
-      --
-      -- This is not so straight-forward so you can assume it
-      postulate from[Contr] : Univalent[Contr] → Univalent
+      from[Contr] : Univalent[Contr] → Univalent
+      from[Contr] = ContrToUniv.lemma _ _
+        where
+        open import Cubical.Fiberwise
 
     univalenceFrom≃ : Univalent≃ → Univalent
     univalenceFrom≃ = from[Contr] ∘ step