diff options
Diffstat (limited to 'src/Helium/Algebra/Core.agda')
| -rw-r--r-- | src/Helium/Algebra/Core.agda | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/src/Helium/Algebra/Core.agda b/src/Helium/Algebra/Core.agda new file mode 100644 index 0000000..afe7053 --- /dev/null +++ b/src/Helium/Algebra/Core.agda @@ -0,0 +1,19 @@ +------------------------------------------------------------------------ +-- Agda Helium +-- +-- More core algebraic definitions +------------------------------------------------------------------------ + +{-# OPTIONS --safe --without-K #-} + +module Helium.Algebra.Core where + +open import Level using (_⊔_) +open import Relation.Binary.Core using (Rel) +open import Relation.Nullary using (¬_) + +AlmostOp₁ : ∀ {a ℓ} {A : Set a} → Rel A ℓ → A → Set (a ⊔ ℓ) +AlmostOp₁ {A = A} _≈_ ε = ∀ {x} → ¬ x ≈ ε → A + +AlmostOp₂ : ∀ {a ℓ} {A : Set a} → Rel A ℓ → A → Set (a ⊔ ℓ) +AlmostOp₂ {A = A} _≈_ ε = ∀ (x : A) {y} → ¬ y ≈ ε → A |