{-# OPTIONS --universe-polymorphism #-}
module Relation.Binary.Core where
open import Data.Product
open import Data.Sum
open import Function
open import Level
open import Relation.Nullary
REL : ∀ {a b} → Set a → Set b → (ℓ : Level) → Set (a ⊔ b ⊔ suc ℓ)
REL A B ℓ = A → B → Set ℓ
Rel : ∀ {a} → Set a → (ℓ : Level) → Set (a ⊔ suc ℓ)
Rel A ℓ = REL A A ℓ
infixr 4 _⇒_ _=[_]⇒_
_⇒_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b} →
REL A B ℓ₁ → REL A B ℓ₂ → Set _
P ⇒ Q = ∀ {i j} → P i j → Q i j
_=[_]⇒_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b} →
Rel A ℓ₁ → (A → B) → Rel B ℓ₂ → Set _
P =[ f ]⇒ Q = P ⇒ (Q on f)
_Preserves_⟶_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b} →
(A → B) → Rel A ℓ₁ → Rel B ℓ₂ → Set _
f Preserves P ⟶ Q = P =[ f ]⇒ Q
_Preserves₂_⟶_⟶_ :
∀ {a b c ℓ₁ ℓ₂ ℓ₃} {A : Set a} {B : Set b} {C : Set c} →
(A → B → C) → Rel A ℓ₁ → Rel B ℓ₂ → Rel C ℓ₃ → Set _
_+_ Preserves₂ P ⟶ Q ⟶ R =
∀ {x y u v} → P x y → Q u v → R (x + u) (y + v)
Reflexive : ∀ {a ℓ} {A : Set a} → Rel A ℓ → Set _
Reflexive _∼_ = ∀ {x} → x ∼ x
Irreflexive : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b} →
REL A B ℓ₁ → REL A B ℓ₂ → Set _
Irreflexive _≈_ _<_ = ∀ {x y} → x ≈ y → ¬ (x < y)
Sym : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b} →
REL A B ℓ₁ → REL B A ℓ₂ → Set _
Sym P Q = P ⇒ flip Q
Symmetric : ∀ {a ℓ} {A : Set a} → Rel A ℓ → Set _
Symmetric _∼_ = Sym _∼_ _∼_
Trans : ∀ {a b c ℓ₁ ℓ₂ ℓ₃} {A : Set a} {B : Set b} {C : Set c} →
REL A B ℓ₁ → REL B C ℓ₂ → REL A C ℓ₃ → Set _
Trans P Q R = ∀ {i j k} → P i j → Q j k → R i k
TransFlip : ∀ {a b c ℓ₁ ℓ₂ ℓ₃} {A : Set a} {B : Set b} {C : Set c} →
REL A B ℓ₁ → REL B C ℓ₂ → REL A C ℓ₃ → Set _
TransFlip P Q R = ∀ {i j k} → Q j k → P i j → R i k
Transitive : ∀ {a ℓ} {A : Set a} → Rel A ℓ → Set _
Transitive _∼_ = Trans _∼_ _∼_ _∼_
Antisymmetric : ∀ {a ℓ₁ ℓ₂} {A : Set a} → Rel A ℓ₁ → Rel A ℓ₂ → Set _
Antisymmetric _≈_ _≤_ = ∀ {x y} → x ≤ y → y ≤ x → x ≈ y
Asymmetric : ∀ {a ℓ} {A : Set a} → Rel A ℓ → Set _
Asymmetric _<_ = ∀ {x y} → x < y → ¬ (y < x)
_Respects_ : ∀ {a ℓ₁ ℓ₂} {A : Set a} → (A → Set ℓ₁) → Rel A ℓ₂ → Set _
P Respects _∼_ = ∀ {x y} → x ∼ y → P x → P y
_Respects₂_ : ∀ {a ℓ₁ ℓ₂} {A : Set a} → Rel A ℓ₁ → Rel A ℓ₂ → Set _
P Respects₂ _∼_ =
(∀ {x} → P x Respects _∼_) ×
(∀ {y} → flip P y Respects _∼_)
Substitutive : ∀ {a ℓ₁} {A : Set a} → Rel A ℓ₁ → (ℓ₂ : Level) → Set _
Substitutive {A = A} _∼_ p = (P : A → Set p) → P Respects _∼_
Decidable : ∀ {a b ℓ} {A : Set a} {B : Set b} → REL A B ℓ → Set _
Decidable _∼_ = ∀ x y → Dec (x ∼ y)
Total : ∀ {a ℓ} {A : Set a} → Rel A ℓ → Set _
Total _∼_ = ∀ x y → (x ∼ y) ⊎ (y ∼ x)
data Tri {a b c} (A : Set a) (B : Set b) (C : Set c) :
Set (a ⊔ b ⊔ c) where
tri< : ( a : A) (¬b : ¬ B) (¬c : ¬ C) → Tri A B C
tri≈ : (¬a : ¬ A) ( b : B) (¬c : ¬ C) → Tri A B C
tri> : (¬a : ¬ A) (¬b : ¬ B) ( c : C) → Tri A B C
Trichotomous : ∀ {a ℓ₁ ℓ₂} {A : Set a} → Rel A ℓ₁ → Rel A ℓ₂ → Set _
Trichotomous _≈_ _<_ = ∀ x y → Tri (x < y) (x ≈ y) (x > y)
where _>_ = flip _<_
record NonEmpty {a b ℓ} {A : Set a} {B : Set b}
(T : REL A B ℓ) : Set (a ⊔ b ⊔ ℓ) where
constructor nonEmpty
field
{x} : A
{y} : B
proof : T x y
private
module Dummy where
infix 4 _≡_ _≢_
data _≡_ {a} {A : Set a} (x : A) : A → Set where
refl : x ≡ x
{-# BUILTIN EQUALITY _≡_ #-}
{-# BUILTIN REFL refl #-}
_≢_ : ∀ {a} {A : Set a} → A → A → Set
x ≢ y = ¬ x ≡ y
record IsEquivalence {a ℓ} {A : Set a}
(_≈_ : Rel A ℓ) : Set (a ⊔ ℓ) where
field
refl : Reflexive _≈_
sym : Symmetric _≈_
trans : Transitive _≈_
reflexive : Dummy._≡_ ⇒ _≈_
reflexive Dummy.refl = refl
open Dummy public