@@ -70,6 +70,8 @@ module LAoP.Relation.Internal
7070 intersection,
7171 union,
7272 sse,
73+ implies,
74+ iff,
7375 ker,
7476 img,
7577
@@ -103,6 +105,10 @@ module LAoP.Relation.Internal
103105 -- ** Bifunctor
104106 (-|-),
105107
108+ -- * Relational "currying"
109+ trans,
110+ untrans,
111+
106112 -- * (Endo-)Relational properties
107113 reflexive,
108114 coreflexive,
@@ -330,6 +336,14 @@ conv (R a) = R (I.tr a)
330336sse :: Relation a b -> Relation a b -> Bool
331337sse a b = a <= b
332338
339+-- | Relational implication (the same as @'sse'@)
340+implies :: Relation a b -> Relation a b -> Bool
341+implies = sse
342+
343+-- | Relational bi-implication
344+iff :: Relation a b -> Relation a b -> Bool
345+iff r s = (r `implies` s) && (s `implies` r)
346+
333347-- | Relational intersection
334348--
335349-- Lifts pointwise conjunction.
@@ -605,6 +619,45 @@ infixl 5 -|-
605619 => Relation a b -> Relation c d -> Relation (Either a c) (Either b d)
606620(-|-) (R a) (R b) = R ((I.-|-) a b)
607621
622+-- Relational "Currying"
623+
624+-- | Relational 'trans'
625+trans ::
626+ ( KnownNat (I.Count (I.Normalize (a, b))),
627+ KnownNat (I.Count (I.Normalize a)),
628+ KnownNat (I.Count (I.Normalize (c, b))),
629+ KnownNat (I.Count (I.Normalize b)),
630+ KnownNat (I.Count (I.Normalize c)),
631+ I.FromLists Boolean (I.Normalize (c, b)) (I.FromNat (I.Count c)),
632+ I.FromLists Boolean (I.Normalize (c, b)) (I.FromNat (I.Count b)),
633+ I.FromLists Boolean (I.Normalize (a, b)) (I.FromNat (I.Count b)),
634+ I.FromLists Boolean (I.Normalize (a, b)) (I.FromNat (I.Count a)),
635+ I.Normalize (a, b) ~ I.Normalize (I.Normalize (a, b)),
636+ I.Normalize (c, b) ~ I.Normalize (I.Normalize (c, b)),
637+ I.Normalize (I.Normalize a, I.Normalize b) ~ I.FromNat (I.Count (I.Normalize (a, b))),
638+ I.Normalize (I.Normalize c, I.Normalize b) ~ I.FromNat (I.Count (I.Normalize (c, b)))
639+ )
640+ => Relation (a, b) c -> Relation a (c, b)
641+trans r = splitR r p2 `comp` conv p1
642+
643+-- | Relational 'untrans'
644+untrans ::
645+ ( KnownNat (I.Count (I.Normalize (a, b))),
646+ KnownNat (I.Count (I.Normalize a)),
647+ KnownNat (I.Count (I.Normalize (c, b))),
648+ KnownNat (I.Count (I.Normalize b)),
649+ KnownNat (I.Count (I.Normalize c)),
650+ I.FromLists Boolean (I.Normalize (c, b)) (I.FromNat (I.Count c)),
651+ I.FromLists Boolean (I.Normalize (c, b)) (I.FromNat (I.Count b)),
652+ I.FromLists Boolean (I.Normalize (a, b)) (I.FromNat (I.Count b)),
653+ I.FromLists Boolean (I.Normalize (a, b)) (I.FromNat (I.Count a)),
654+ I.Normalize (a, b) ~ I.Normalize (I.Normalize (a, b)),
655+ I.Normalize (c, b) ~ I.Normalize (I.Normalize (c, b)),
656+ I.Normalize (I.Normalize a, I.Normalize b) ~ I.FromNat (I.Count (I.Normalize (a, b))),
657+ I.Normalize (I.Normalize c, I.Normalize b) ~ I.FromNat (I.Count (I.Normalize (c, b)))
658+ )
659+ => Relation a (c, b) -> Relation (a, b) c
660+untrans s = p1 `comp` conv (splitR (conv s) p2)
608661
609662-- Relation pretty print
610663