diff --git a/formalizations/guarded-cubical/Common/Poset/Constructions.agda b/formalizations/guarded-cubical/Common/Poset/Constructions.agda
index 3aae364eb5cf83d585100af1c0744136a7bf945b..ca4b0be4c101e09caae635883f2feb70186f1ccb 100644
--- a/formalizations/guarded-cubical/Common/Poset/Constructions.agda
+++ b/formalizations/guarded-cubical/Common/Poset/Constructions.agda
@@ -8,7 +8,7 @@ module Common.Poset.Constructions where
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Structure
 open import Cubical.Relation.Binary
-open import Cubical.Relation.Binary.Poset
+open import Cubical.Relation.Binary.Order.Poset
 open import Cubical.Foundations.HLevels
 open import Cubical.Data.Bool
 open import Cubical.Data.Nat renaming (â„• to Nat)
diff --git a/formalizations/guarded-cubical/Common/Poset/MonotoneRelation.agda b/formalizations/guarded-cubical/Common/Poset/MonotoneRelation.agda
index 17693fe45d77adfa1c078c9c75740e8db4313929..3c628db14eae87d9869ff7bf090075c6e48630cf 100644
--- a/formalizations/guarded-cubical/Common/Poset/MonotoneRelation.agda
+++ b/formalizations/guarded-cubical/Common/Poset/MonotoneRelation.agda
@@ -10,7 +10,7 @@ open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Function
 
 open import Cubical.Relation.Binary
-open import Cubical.Relation.Binary.Poset
+open import Cubical.Relation.Binary.Order.Poset
 open import Cubical.Foundations.Structure
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.HLevels
diff --git a/formalizations/guarded-cubical/Semantics/LockStepErrorOrdering.agda b/formalizations/guarded-cubical/Semantics/LockStepErrorOrdering.agda
index 99c31f0bb6167c506245ea70d6f957c8fb787b97..c37daff13703f9fa460e4de8c9dc593567adeb79 100644
--- a/formalizations/guarded-cubical/Semantics/LockStepErrorOrdering.agda
+++ b/formalizations/guarded-cubical/Semantics/LockStepErrorOrdering.agda
@@ -8,7 +8,7 @@ open import Common.Later
 module Semantics.LockStepErrorOrdering (k : Clock) where
 
 open import Cubical.Relation.Binary
-open import Cubical.Relation.Binary.Poset
+open import Cubical.Relation.Binary.Order.Poset
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Function
diff --git a/formalizations/guarded-cubical/Semantics/PredomainInternalHom.agda b/formalizations/guarded-cubical/Semantics/PredomainInternalHom.agda
index e41411c7821ea0f3e3672121b02633ea08090c31..b7e0d5caa2bc73e0406a77b055156429350e0793 100644
--- a/formalizations/guarded-cubical/Semantics/PredomainInternalHom.agda
+++ b/formalizations/guarded-cubical/Semantics/PredomainInternalHom.agda
@@ -7,7 +7,7 @@ module Semantics.PredomainInternalHom where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Structure
-open import Cubical.Relation.Binary.Poset
+open import Cubical.Relation.Binary.Order.Poset
 
 
 open import Semantics.Predomains
diff --git a/formalizations/guarded-cubical/Semantics/Predomains.agda b/formalizations/guarded-cubical/Semantics/Predomains.agda
index 77de44bbf7604e1443405548b831051d47b603d8..dbc948bb721d0bef2b54e0a835b781c862120228 100644
--- a/formalizations/guarded-cubical/Semantics/Predomains.agda
+++ b/formalizations/guarded-cubical/Semantics/Predomains.agda
@@ -8,7 +8,7 @@ module Semantics.Predomains where
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Structure
 open import Cubical.Relation.Binary
-open import Cubical.Relation.Binary.Poset
+open import Cubical.Relation.Binary.Order.Poset
 open import Cubical.Foundations.HLevels
 open import Cubical.Data.Bool
 open import Cubical.Data.Nat renaming (â„• to Nat)