blob: afe70533a48b3d40be81add3b210b7befb4f758c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
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
|
