We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 2e629e0 commit bad2ee9Copy full SHA for bad2ee9
src/Relation/Binary/Domain/Definitions.agda
@@ -21,7 +21,6 @@ private
21
22
------------------------------------------------------------------------
23
-- Directed families
24
-------------------------------------------------------------------------
25
26
IsSemidirectedFamily : (P : Poset c ℓ₁ ℓ₂) → ∀ {Ix : Set c} → (s : Ix → Poset.Carrier P) → Set _
27
IsSemidirectedFamily P {Ix} s = ∀ i j → ∃[ k ] (Poset._≤_ P (s i) (s k) × Poset._≤_ P (s j) (s k))
src/Relation/Binary/Properties/Domain.agda
0 commit comments