From 62aa5c1de5c58a3ed805a8fa690353db71bb3528 Mon Sep 17 00:00:00 2001 From: Jacques Date: Wed, 19 Feb 2025 12:31:49 -0500 Subject: [PATCH] Apartness & Construct --- src/Algebra/Apartness/Bundles.agda | 2 +- src/Algebra/Construct/Add/Identity.agda | 17 +++++++++-------- src/Algebra/Construct/NaturalChoice/Base.agda | 2 +- 3 files changed, 11 insertions(+), 10 deletions(-) diff --git a/src/Algebra/Apartness/Bundles.agda b/src/Algebra/Apartness/Bundles.agda index 9a55794051..ba9c715ff4 100644 --- a/src/Algebra/Apartness/Bundles.agda +++ b/src/Algebra/Apartness/Bundles.agda @@ -13,7 +13,7 @@ open import Relation.Binary.Core using (Rel) open import Relation.Binary.Bundles using (ApartnessRelation) open import Algebra.Core using (Op₁; Op₂) open import Algebra.Bundles using (CommutativeRing) -open import Algebra.Apartness.Structures +open import Algebra.Apartness.Structures using (IsHeytingCommutativeRing; IsHeytingField) record HeytingCommutativeRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infix 8 -_ diff --git a/src/Algebra/Construct/Add/Identity.agda b/src/Algebra/Construct/Add/Identity.agda index dc82a1c67b..6aacaebf9b 100644 --- a/src/Algebra/Construct/Add/Identity.agda +++ b/src/Algebra/Construct/Add/Identity.agda @@ -9,17 +9,18 @@ module Algebra.Construct.Add.Identity where -open import Algebra.Bundles +open import Algebra.Bundles using (Semigroup; Monoid) open import Algebra.Core using (Op₂) -open import Algebra.Definitions -open import Algebra.Structures -open import Relation.Binary.Construct.Add.Point.Equality renaming (_≈∙_ to lift≈) +open import Algebra.Definitions using (Congruent₂; Associative; LeftIdentity; RightIdentity; Identity) +open import Algebra.Structures using (IsMagma; IsSemigroup; IsMonoid) open import Data.Product.Base using (_,_) open import Level using (Level; _⊔_) -open import Relation.Binary.Core -open import Relation.Binary.Definitions -open import Relation.Binary.Structures -open import Relation.Nullary.Construct.Add.Point +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Definitions using (Reflexive) +open import Relation.Binary.Structures using (IsEquivalence) +open import Relation.Nullary.Construct.Add.Point using (Pointed; [_]; ∙) +open import Relation.Binary.Construct.Add.Point.Equality renaming (_≈∙_ to lift≈) + private variable diff --git a/src/Algebra/Construct/NaturalChoice/Base.agda b/src/Algebra/Construct/NaturalChoice/Base.agda index 6b4d4d13b7..9ba6b08a66 100644 --- a/src/Algebra/Construct/NaturalChoice/Base.agda +++ b/src/Algebra/Construct/NaturalChoice/Base.agda @@ -7,7 +7,7 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Algebra.Core +open import Algebra.Core using (Op₂) open import Level as L hiding (_⊔_) open import Function.Base using (flip) open import Relation.Binary.Bundles using (TotalPreorder)