5 files changed, 242 insertions, 0 deletions
diff --git a/src/Relation/Unary/Closure/Base.agda b/src/Relation/Unary/Closure/Base.agda
new file mode 100644
index 0000000..0457d92
--- /dev/null
+++ b/src/Relation/Unary/Closure/Base.agda
@@ -0,0 +1,61 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Closures of a unary relation with respect to a binary one.
+------------------------------------------------------------------------
+
+open import Relation.Binary
+
+module Relation.Unary.Closure.Base {a b} {A : Set a} (R : Rel A b) where
+
+open import Level
+open import Relation.Unary using (Pred)
+
+------------------------------------------------------------------------
+-- Definitions
+
+-- We start with the definition of □ ("box") which is named after the box
+-- modality in modal logic. `□ T x` states that all the elements one step
+-- away from `x` with respect to the relation R satisfy `T`.
+
+□ : ∀ {t} → Pred A t → Pred A (a ⊔ b ⊔ t)
+□ T x = ∀ {y} → R x y → T y
+
+-- Use cases of □ include:
+-- * The definition of the accessibility predicate corresponding to R:
+--   data Acc (x : A) : Set (a ⊔ b) where
+--     step : □ Acc x → Acc x
+
+-- * The characterization of stability under weakening: picking R to be
+--   `Data.List.Relation.Sublist.Inductive`, `∀ {Γ} → Tm Γ → □ T Γ`
+--   corresponds to the fact that we have a notion of weakening for `Tm`.
+
+-- Closed: whenever we have a value in one context, we can get one in any
+-- related context.
+
+record Closed {t} (T : Pred A t) : Set (a ⊔ b ⊔ t) where
+  field next : ∀ {x} → T x → □ T x
+
+
+------------------------------------------------------------------------
+-- Properties
+
+module _ {t} {T : Pred A t} where
+
+  reindex : Transitive R → ∀ {x y} → R x y → □ T x → □ T y
+  reindex trans x∼y □Tx y∼z = □Tx (trans x∼y y∼z)
+
+  -- Provided that R is reflexive and Transitive, □ is a comonad
+  map : ∀ {u} {U : Pred A u} {x} → (∀ {x} → T x → U x) → □ T x → □ U x
+  map f □Tx x~y = f (□Tx x~y)
+
+  extract : Reflexive R → ∀ {x} → □ T x → T x
+  extract refl □Tx = □Tx refl
+
+  duplicate : Transitive R → ∀ {x} → □ T x → □ (□ T) x
+  duplicate trans □Tx x∼y y∼z = □Tx (trans x∼y y∼z)
+
+-- Provided that R is transitive, □ is the Closure operator
+-- i.e. for any `T`, `□ T` is closed.
+□-closed : Transitive R → ∀ {t} {T : Pred A t} → Closed (□ T)
+□-closed trans = record { next = duplicate trans }
diff --git a/src/Relation/Unary/Closure/Preorder.agda b/src/Relation/Unary/Closure/Preorder.agda
new file mode 100644
index 0000000..2d16751
--- /dev/null
+++ b/src/Relation/Unary/Closure/Preorder.agda
@@ -0,0 +1,30 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Closure of a unary relation with respect to a preorder
+------------------------------------------------------------------------
+
+open import Relation.Binary
+
+module Relation.Unary.Closure.Preorder {a r e} (P : Preorder a e r) where
+
+open Preorder P
+open import Relation.Unary using (Pred)
+
+-- Specialising the results proven generically in `Base`.
+import Relation.Unary.Closure.Base _∼_ as Base
+open Base public using (□; map; Closed)
+
+module _ {t} {T : Pred Carrier t} where
+
+  reindex : ∀ {x y} → x ∼ y → □ T x → □ T y
+  reindex = Base.reindex trans
+
+  extract : ∀ {x} → □ T x → T x
+  extract = Base.extract refl
+
+  duplicate : ∀ {x} → □ T x → □ (□ T) x
+  duplicate = Base.duplicate trans
+
+□-closed : ∀ {t} {T : Pred Carrier t} → Closed (□ T)
+□-closed = Base.□-closed trans
diff --git a/src/Relation/Unary/Closure/StrictPartialOrder.agda b/src/Relation/Unary/Closure/StrictPartialOrder.agda
new file mode 100644
index 0000000..bce595f
--- /dev/null
+++ b/src/Relation/Unary/Closure/StrictPartialOrder.agda
@@ -0,0 +1,28 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Closures of a unary relation with respect to a strict partial order
+------------------------------------------------------------------------
+
+open import Relation.Binary
+
+module Relation.Unary.Closure.StrictPartialOrder
+       {a r e} (P : StrictPartialOrder a e r) where
+
+open StrictPartialOrder P renaming (_<_ to _∼_)
+open import Relation.Unary using (Pred)
+
+-- Specialising the results proven generically in `Base`.
+import Relation.Unary.Closure.Base _∼_ as Base
+open Base public using (□; map; Closed)
+
+module _ {t} {T : Pred Carrier t} where
+
+  reindex : ∀ {x y} → x ∼ y → □ T x → □ T y
+  reindex = Base.reindex trans
+
+  duplicate : ∀ {x} → □ T x → □ (□ T) x
+  duplicate = Base.duplicate trans
+
+□-closed : ∀ {t} {T : Pred Carrier t} → Closed (□ T)
+□-closed = Base.□-closed trans
diff --git a/src/Relation/Unary/Indexed.agda b/src/Relation/Unary/Indexed.agda
new file mode 100644
index 0000000..26f06cf
--- /dev/null
+++ b/src/Relation/Unary/Indexed.agda
@@ -0,0 +1,22 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Indexed unary relations
+------------------------------------------------------------------------
+
+module Relation.Unary.Indexed  where
+
+open import Data.Product using (∃; _×_)
+open import Level
+open import Relation.Nullary using (¬_)
+
+IPred : ∀ {i a} {I : Set i} → (I → Set a) → (ℓ : Level) → Set _
+IPred A ℓ = ∀ {i} → A i → Set ℓ
+
+module _ {i a} {I : Set i} {A : I → Set a} where
+
+  _∈_ : ∀ {ℓ} → (∀ i → A i) → IPred A ℓ → Set _
+  x ∈ P = ∀ i → P (x i)
+
+  _∉_ : ∀ {ℓ} → (∀ i → A i) → IPred A ℓ → Set _
+  t ∉ P = ¬ (t ∈ P)
diff --git a/src/Relation/Unary/Properties.agda b/src/Relation/Unary/Properties.agda
new file mode 100644
index 0000000..f2f1076
--- /dev/null
+++ b/src/Relation/Unary/Properties.agda
@@ -0,0 +1,101 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of constructions over unary relations
+------------------------------------------------------------------------
+
+module Relation.Unary.Properties where
+
+open import Data.Product using (_×_; _,_; swap; proj₁)
+open import Data.Sum.Base using (inj₁; inj₂)
+open import Data.Unit using (tt)
+open import Relation.Binary.Core hiding (Decidable)
+open import Relation.Unary
+open import Relation.Nullary using (yes; no)
+open import Relation.Nullary.Product using (_×-dec_)
+open import Relation.Nullary.Sum using (_⊎-dec_)
+open import Relation.Nullary.Negation using (¬?)
+open import Function using (_$_; _∘_)
+
+----------------------------------------------------------------------
+-- The empty set
+
+module _ {a} {A : Set a} where
+
+  ∅? : Decidable {A = A} ∅
+  ∅? _ = no λ()
+
+  ∅-Empty : Empty {A = A} ∅
+  ∅-Empty x ()
+
+  ∁∅-Universal : Universal {A = A} (∁ ∅)
+  ∁∅-Universal = λ x x∈∅ → x∈∅
+
+----------------------------------------------------------------------
+-- The universe
+
+module _ {a} {A : Set a} where
+
+  U? : Decidable {A = A} U
+  U? _ = yes tt
+
+  U-Universal : Universal {A = A} U
+  U-Universal = λ _ → _
+
+  ∁U-Empty : Empty {A = A} (∁ U)
+  ∁U-Empty = λ x x∈∁U → x∈∁U _
+
+----------------------------------------------------------------------
+-- Subset properties
+
+module _ {a ℓ} {A : Set a} where
+
+  ∅-⊆ : (P : Pred A ℓ) → ∅ ⊆ P
+  ∅-⊆ P ()
+
+  ⊆-U : (P : Pred A ℓ) → P ⊆ U
+  ⊆-U P _ = _
+
+  ⊆-refl : Reflexive (_⊆_ {A = A} {ℓ})
+  ⊆-refl x∈P = x∈P
+
+  ⊆-trans : Transitive (_⊆_ {A = A} {ℓ})
+  ⊆-trans P⊆Q Q⊆R x∈P = Q⊆R (P⊆Q x∈P)
+
+  ⊂-asym : Asymmetric (_⊂_ {A = A} {ℓ})
+  ⊂-asym (_ , Q⊈P) = Q⊈P ∘ proj₁
+
+----------------------------------------------------------------------
+-- Decidability properties
+
+module _ {a} {A : Set a} where
+
+  ∁? : ∀ {ℓ} {P : Pred A ℓ} → Decidable P → Decidable (∁ P)
+  ∁? P? x = ¬? (P? x)
+
+  _∪?_ : ∀ {ℓ₁ ℓ₂} {P : Pred A ℓ₁} {Q : Pred A ℓ₂} →
+         Decidable P → Decidable Q → Decidable (P ∪ Q)
+  _∪?_ P? Q? x = (P? x) ⊎-dec (Q? x)
+
+  _∩?_ : ∀ {ℓ₁ ℓ₂} {P : Pred A ℓ₁} {Q : Pred A ℓ₂} →
+         Decidable P → Decidable Q → Decidable (P ∩ Q)
+  _∩?_ P? Q? x = (P? x) ×-dec (Q? x)
+
+module _ {a b} {A : Set a} {B : Set b} where
+
+  _×?_ : ∀ {ℓ₁ ℓ₂} {P : Pred A ℓ₁} {Q : Pred B ℓ₂} →
+         Decidable P → Decidable Q → Decidable (P ⟨×⟩ Q)
+  _×?_ P? Q? (a , b) = (P? a) ×-dec (Q? b)
+
+  _⊙?_ : ∀ {ℓ₁ ℓ₂} {P : Pred A ℓ₁} {Q : Pred B ℓ₂} →
+         Decidable P → Decidable Q → Decidable (P ⟨⊙⟩ Q)
+  _⊙?_ P? Q? (a , b) = (P? a) ⊎-dec (Q? b)
+
+  _⊎?_ : ∀ {ℓ} {P : Pred A ℓ} {Q : Pred B ℓ} →
+         Decidable P → Decidable Q → Decidable (P ⟨⊎⟩ Q)
+  _⊎?_ P? Q? (inj₁ a) = P? a
+  _⊎?_ P? Q? (inj₂ b) = Q? b
+
+  _~? : ∀ {ℓ} {P : Pred (A × B) ℓ} →
+        Decidable P → Decidable (P ~)
+  _~? P? = P? ∘ swap