Closure (hull) operators in agda

closure.agda

open import Agda.Primitive

Pred : ∀{a} → Set a → Set _
Pred A = A → Set

_∈_ : ∀{a} {A : Set a} → A → Pred A → Set
x ∈ α = α x

_⊂_ : ∀{a} {A : Set a} → Pred A → Pred A → Set a
α ⊂ β = ∀ x → x ∈ α → x ∈ β

record _≈_ {a} {A : Set a} (α β : Pred A) : Set a where
  field
    ≈⊂ : α ⊂ β
    ≈⊃ : β ⊂ α

record Closure {a} {A : Set a} (ρ : Pred A → Pred A) : Set (lsuc a) where
  field
    ext : (α   : Pred A) → α ⊂ (ρ α)
    inc : (α β : Pred A) → α ⊂ β → (ρ α) ⊂ (ρ β)
    ide : (α   : Pred A) → ρ (ρ α) ≈ (ρ α)