@@ -67,6 +67,13 @@ module LAoP.Relation.Internal
6767 ker,
6868 img,
6969
70+ -- * Taxonomy of binary relations
71+ entire,
72+ injective,
73+ surjective,
74+ simple,
75+ bijective,
76+
7077 -- * (Endo-)Relational properties
7178 reflexive,
7279 coreflexive,
@@ -325,6 +332,15 @@ entire = reflexive . ker
325332surjective :: (KnownNat (I.Count (I.Normalize b)), I.FromLists Boolean (I.Normalize b) (I.Normalize b)) => Relation a b -> Bool
326333surjective = reflexive . img
327334
335+-- | A 'Relation' @r@ is bijective iff @'injective' r && 'surjective' r@
336+bijective ::
337+ ( KnownNat (I.Count (I.Normalize b)),
338+ KnownNat (I.Count (I.Normalize a)),
339+ I.FromLists Boolean (I.Normalize b) (I.Normalize b),
340+ I.FromLists Boolean (I.Normalize a) (I.Normalize a)
341+ ) => Relation a b -> Bool
342+bijective r = injective r && surjective r
343+
328344-- | A 'Relation' @r@ is transitive iff @(r `'comp'` r) `'sse'` r@
329345transitive :: Relation a a -> Bool
330346transitive r = (r `comp` r) `sse` r