From 1f718c9dbe48934edf115aef285c5aeaa2dfb20d Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown@cl.cam.ac.uk>
Date: Fri, 7 Jan 2022 13:36:42 +0000
Subject: Add some required algebraic types.

---
 src/Helium/Algebra/Core.agda | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)
 create mode 100644 src/Helium/Algebra/Core.agda

(limited to 'src/Helium/Algebra/Core.agda')

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
-- 
cgit v1.2.3