diff --git a/formalizations/guarded-cubical/Semantics/Concrete/DoublePoset/LockStepErrorBisim.agda b/formalizations/guarded-cubical/Semantics/Concrete/DoublePoset/LockStepErrorBisim.agda
index afe5e15a747d768ebc36ac298695a3f6a42b762f..92240c20ca46c0686d770ab886b4bfceaaca68f0 100644
--- a/formalizations/guarded-cubical/Semantics/Concrete/DoublePoset/LockStepErrorBisim.agda
+++ b/formalizations/guarded-cubical/Semantics/Concrete/DoublePoset/LockStepErrorBisim.agda
@@ -27,7 +27,7 @@ open import Cubical.Foundations.Equiv
 
 open import Cubical.Relation.Nullary
 open import Cubical.Relation.Binary.Base
-open import Cubical.Relation.Binary.Poset
+open import Cubical.Relation.Binary.Order.Poset
 
 open import Cubical.Data.Unit.Properties
 
diff --git a/formalizations/guarded-cubical/Semantics/Monotone/Base.agda b/formalizations/guarded-cubical/Semantics/Monotone/Base.agda
index 92d2665af450d89fc446ed8e4e8bcbd7aa0ca5b1..36bcab625d2aa146d19f9f84750cacea4d65f0b9 100644
--- a/formalizations/guarded-cubical/Semantics/Monotone/Base.agda
+++ b/formalizations/guarded-cubical/Semantics/Monotone/Base.agda
@@ -6,7 +6,7 @@
 
 module Semantics.Monotone.Base where
 
-open import Cubical.Relation.Binary.Poset
+open import Cubical.Relation.Binary.Order.Poset
 open import Cubical.Data.Sigma
 open import Cubical.Foundations.Structure
 
diff --git a/formalizations/guarded-cubical/Semantics/WeakBisimilarity.agda b/formalizations/guarded-cubical/Semantics/WeakBisimilarity.agda
index c0cc371638d96017696da51d57fb7fad643d8df6..8511f42a9433e344ccfa830538fc96938f514218 100644
--- a/formalizations/guarded-cubical/Semantics/WeakBisimilarity.agda
+++ b/formalizations/guarded-cubical/Semantics/WeakBisimilarity.agda
@@ -17,7 +17,7 @@ open import Cubical.Data.Sum
 open import Cubical.Data.Empty as ⊥
 
 open import Cubical.Relation.Binary
-open import Cubical.Relation.Binary.Poset
+open import Cubical.Relation.Binary.Order.Poset
 
 open import Cubical.HITs.PropositionalTruncation renaming (elim to PTelim)