Skip to content

Instantly share code, notes, and snippets.

@louisswarren louisswarren/closure.agda
Last active Sep 23, 2019

Embed
What would you like to do?
Closure (hull) operators in 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
You can’t perform that action at this time.