Skip to content

Instantly share code, notes, and snippets.

@louisswarren

louisswarren/closure.agda

Last active September 23, 2019 02:53
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save louisswarren/d47bb47c152becbf6b1337fc46914756 to your computer and use it in GitHub Desktop.
Save louisswarren/d47bb47c152becbf6b1337fc46914756 to your computer and use it in GitHub Desktop.
Download ZIP
Closure (hull) operators in agda
Raw
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) → ρ (ρ α) ≈ (ρ α)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment