From 35b3a76738f96c737c6cbf354b01dbc5612fd168 Mon Sep 17 00:00:00 2001 From: Jesin Date: Thu, 16 Nov 2023 00:47:03 -0500 Subject: [PATCH] fix Connex comment Connex allows both relations to hold, so the old comment was wrong. --- src/Relation/Binary/Definitions.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Relation/Binary/Definitions.agda b/src/Relation/Binary/Definitions.agda index 547d4e7b48..887cb7c4a6 100644 --- a/src/Relation/Binary/Definitions.agda +++ b/src/Relation/Binary/Definitions.agda @@ -99,7 +99,7 @@ Asymmetric _<_ = ∀ {x y} → x < y → ¬ (y < x) Dense : Rel A ℓ → Set _ Dense _<_ = ∀ {x y} → x < y → ∃[ z ] x < z × z < y --- Generalised connex - exactly one of the two relations holds. +-- Generalised connex - at least one of the two relations holds. Connex : REL A B ℓ₁ → REL B A ℓ₂ → Set _ Connex P Q = ∀ x y → P x y ⊎ Q y x