From 5b0250dcd45d78e97f79827563952d2f1af6588c Mon Sep 17 00:00:00 2001 From: Eric Giovannini <ecg19@seas.upenn.edu> Date: Tue, 14 Nov 2023 16:13:57 -0500 Subject: [PATCH] update to agda 2.6.4 and cubical-0.6 --- formalizations/guarded-cubical/Common/Poset/Convenience.agda | 2 +- formalizations/guarded-cubical/Common/Poset/Monotone.agda | 2 +- .../guarded-cubical/Semantics/Concrete/DoublePoset/Base.agda | 2 +- .../Semantics/Concrete/DoublePoset/Morphism.agda | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/formalizations/guarded-cubical/Common/Poset/Convenience.agda b/formalizations/guarded-cubical/Common/Poset/Convenience.agda index 2665387..82312c6 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 2138df9..c7ada3e 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 59e4a30..4d0d597 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 e0d0c62..a550074 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 -- GitLab