From b1ac973d9a53b6853e5c6e82c780e1240a57493c Mon Sep 17 00:00:00 2001 From: akaiDing <tingtind@umich.edu> Date: Tue, 14 Nov 2023 16:30:55 -0500 Subject: [PATCH] update cubical library path --- .../Semantics/Concrete/DoublePoset/LockStepErrorBisim.agda | 2 +- formalizations/guarded-cubical/Semantics/Monotone/Base.agda | 2 +- formalizations/guarded-cubical/Semantics/WeakBisimilarity.agda | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/formalizations/guarded-cubical/Semantics/Concrete/DoublePoset/LockStepErrorBisim.agda b/formalizations/guarded-cubical/Semantics/Concrete/DoublePoset/LockStepErrorBisim.agda index afe5e15..92240c2 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 92d2665..36bcab6 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 c0cc371..8511f42 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) -- GitLab