diff --git a/formalizations/guarded-cubical/Common/Poset/Convenience.agda b/formalizations/guarded-cubical/Common/Poset/Convenience.agda
index 2665387348205efc3ac03bff6ff82b767f54bd86..82312c6a1033a926d1dd0795aa25050fe11c7220 100644
--- a/formalizations/guarded-cubical/Common/Poset/Convenience.agda
+++ b/formalizations/guarded-cubical/Common/Poset/Convenience.agda
@@ -3,7 +3,7 @@
 module Common.Poset.Convenience where
 
 open import Cubical.Foundations.Prelude
-open import Cubical.Relation.Binary.Poset
+open import Cubical.Relation.Binary.Order.Poset
 open import Cubical.Foundations.Structure
 open import Cubical.Foundations.HLevels
 open import Cubical.Relation.Binary.Base
diff --git a/formalizations/guarded-cubical/Common/Poset/Monotone.agda b/formalizations/guarded-cubical/Common/Poset/Monotone.agda
index 2138df961401c6e9c2c61196dec4ea57fceb6e91..c7ada3e735a0175d5bbab4e5f435ee0a98ba0942 100644
--- a/formalizations/guarded-cubical/Common/Poset/Monotone.agda
+++ b/formalizations/guarded-cubical/Common/Poset/Monotone.agda
@@ -18,7 +18,7 @@ open import Cubical.Reflection.RecordEquiv
 open import Cubical.Data.Sigma
 
 -- open import Common.Preorder.Base
-open import Cubical.Relation.Binary.Poset
+open import Cubical.Relation.Binary.Order.Poset
 open import Common.Poset.Convenience
 
 
diff --git a/formalizations/guarded-cubical/Semantics/Concrete/DoublePoset/Base.agda b/formalizations/guarded-cubical/Semantics/Concrete/DoublePoset/Base.agda
index 59e4a30ae0a1c9fb866240e8b0bd8268cff82fb3..4d0d597e30239240c2ac43785eb825bda4bd3257 100644
--- a/formalizations/guarded-cubical/Semantics/Concrete/DoublePoset/Base.agda
+++ b/formalizations/guarded-cubical/Semantics/Concrete/DoublePoset/Base.agda
@@ -3,7 +3,7 @@ module Semantics.Concrete.DoublePoset.Base where
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Structure
 
-open import Cubical.Relation.Binary.Poset
+open import Cubical.Relation.Binary.Order.Poset.Base
 open import Cubical.Relation.Binary.Base
 
 open import Common.Common
diff --git a/formalizations/guarded-cubical/Semantics/Concrete/DoublePoset/Morphism.agda b/formalizations/guarded-cubical/Semantics/Concrete/DoublePoset/Morphism.agda
index e0d0c6209b7eb2e39dde5b81096b49960ce44b92..a55007446b95248780a33b148fd9d9ec5b23fcbb 100644
--- a/formalizations/guarded-cubical/Semantics/Concrete/DoublePoset/Morphism.agda
+++ b/formalizations/guarded-cubical/Semantics/Concrete/DoublePoset/Morphism.agda
@@ -19,7 +19,7 @@ open import Cubical.Data.Sigma
 
 open import Common.Common
 -- open import Common.Preorder.Base
-open import Cubical.Relation.Binary.Poset
+open import Cubical.Relation.Binary.Order.Poset
 open import Common.Poset.Convenience
 
 open import Semantics.Concrete.DoublePoset.Base