Add some required algebraic types.

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