From a0c7a288a9bb1688acb625bdf0937518faf6699d Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Fri, 5 Jun 2026 21:05:36 +0200 Subject: [PATCH] Add definitions for function-like relations --- src/Relation/Binary/Definitions.agda | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/src/Relation/Binary/Definitions.agda b/src/Relation/Binary/Definitions.agda index 80b9e5ff44..1e878f07f4 100644 --- a/src/Relation/Binary/Definitions.agda +++ b/src/Relation/Binary/Definitions.agda @@ -262,3 +262,23 @@ record NonEmpty {A : Set a} {B : Set b} {x} : A {y} : B proof : T x y + +-- LeftUnique - the relation is injective, +-- i.e. every element of the codomain has at most one preimage. +LeftUnique : Rel A ℓ₁ → Rel B ℓ₂ → REL A B ℓ → Set _ +LeftUnique _≈₁_ _≈₂_ _↦_ = ∀ {x y u v} → x ↦ u → y ↦ v → u ≈₂ v → x ≈₁ y + +-- RightUnique - the relation is a (partial) function, +-- i.e. every element of the domain has at most one image. +RightUnique : Rel A ℓ₁ → Rel B ℓ₂ → REL A B ℓ → Set _ +RightUnique _≈₁_ _≈₂_ _↦_ = ∀ {x y u v} → x ↦ u → y ↦ v → x ≈₁ y → u ≈₂ v + +-- LeftTotal - the relation is total (as in a total function), +-- i.e. every element of the domain has at least one image. +LeftTotal : Rel A ℓ₁ → REL A B ℓ → Set _ +LeftTotal _≈_ _↦_ = ∀ x → ∃[ u ] x ↦ u + +-- RightTotal - the relation is surjective, +-- i.e. every element of the codomain has at least one preimage. +RightTotal : Rel B ℓ₂ → REL A B ℓ → Set _ +RightTotal _≈_ _↦_ = ∀ u → ∃[ x ] x ↦ u