@@ -382,8 +382,8 @@ belongs = toRel (flip elemR)
382382-- Also known as ⊥ (Bottom) Relation or empty Relation.
383383--
384384-- @
385−-- r `'comp'` ⊥ == ⊥ `'comp'` r == ⊥
386−-- ⊥ `'sse'` R && R `'sse'` T == True
385+-- r ``comp`` ⊥ == ⊥ ``comp`` r == ⊥
386+-- ⊥ ``sse`` R && R ``sse`` T == True
387387-- @
388388zeros ::
389389 (I.FromLists Boolean (I.Normalize a) (I.Normalize b), KnownNat (I.Count (I.Normalize a)), KnownNat (I.Count (I.Normalize b))) =>
@@ -398,7 +398,7 @@ zeros = relationBuilder (const (nat 0))
398398-- Also known as T (Top) Relation or universal Relation.
399399--
400400-- @
401−-- ⊥ `'sse'` R && R `'sse'` T == True
401+-- ⊥ ``sse`` R && R ``sse`` T == True
402402-- @
403403ones ::
404404 (I.FromLists Boolean (I.Normalize a) (I.Normalize b), KnownNat (I.Count (I.Normalize a)), KnownNat (I.Count (I.Normalize b))) =>
@@ -428,7 +428,7 @@ point = fromF' . const
428428-- | Identity matrix
429429--
430430-- @
431−-- 'identity' `'comp'` r == r == r `'comp'` 'identity'
431+-- 'identity' ``comp`` r == r == r ``comp`` 'identity'
432432-- @
433433identity ::
434434 (I.FromLists Boolean (I.Normalize a) (I.Normalize a), KnownNat (I.Count (I.Normalize a))) =>
@@ -438,7 +438,7 @@ identity = relationBuilder (bool (nat 0) (nat 1) . uncurry (==))
438438-- | Relational composition
439439--
440440-- @
441−-- r `'comp'` (s `'comp'` p) = (r `'comp'` s) `'comp'` p
441+-- r ``comp`` (s ``comp`` p) = (r ``comp`` s) ``comp`` p
442442-- @
443443comp :: Relation b c -> Relation a b -> Relation a c
444444comp (R a) (R b) = R (I.compRel a b)
@@ -469,7 +469,7 @@ divS (R x) (R y) = R (I.divS x y)
469469
470470-- | Relational shrinking.
471471--
472−-- @r `'shrunkBy'` s@ is the largest part of @r@ such that,
472+-- @r ``shrunkBy`` s@ is the largest part of @r@ such that,
473473-- if it yields an output for an input @x@, it must be a maximum,
474474-- with respect to @s@, among all possible outputs of @x@ by @r@.
475475shrunkBy :: Relation b a -> Relation a a -> Relation b a
@@ -477,13 +477,13 @@ shrunkBy r s = r `intersection` divR s (conv r)
477477
478478-- | Relational overriding.
479479--
480−-- @r `'overriddenBy'` s@ yields the relation which contains the
480+-- @r ``overriddenBy`` s@ yields the relation which contains the
481481-- whole of @s@ and that part of @r@ where @s@ is undefined.
482482--
483483-- @
484−-- 'zeros' `'overriddenBy'` s == s
485−-- r `'overriddenBy'` 'zeros' == r
486−-- r `'overriddenBy'` r == r
484+-- 'zeros' ``overriddenBy`` s == s
485+-- r ``overriddenBy`` 'zeros' == r
486+-- r ``overriddenBy`` r == r
487487-- @
488488overriddenBy ::
489489 ( I.FromLists Boolean (I.Normalize b) (I.Normalize b),
@@ -494,7 +494,7 @@ overriddenBy r s = s `union` r `intersection` divR zeros (conv s)
494494-- | Relational application.
495495--
496496-- If @a@ and @b@ are related by 'Relation' @r@
497−-- then @'pointAp' a b r == 'one' ('Nat' 1)@
497+-- then @'pointAp' a b r == 'one' ('nat' 1)@
498498pointAp ::
499499 ( Bounded a,
500500 Bounded b,
@@ -553,8 +553,8 @@ iff r s = r == s
553553-- Lifts pointwise conjunction.
554554--
555555-- @
556−-- (r `'intersection'` s) `'intersection'` t == r `'intersection' (s `'intersection'` t)
557−-- x `'sse'` r `'intersection'` s == x `'intersection'` r && x `'intersection'` s
556+-- (r ``intersection`` s) ``intersection`` t == r ``intersection`` (s ``intersection`` t)
557+-- x ``sse`` r ``intersection`` s == x ``intersection`` r && x ``intersection`` s
558558-- @
559559intersection :: Relation a b -> Relation a b -> Relation a b
560560intersection a b = a * b
@@ -564,10 +564,10 @@ intersection a b = a * b
564564-- Lifts pointwise disjunction.
565565--
566566-- @
567−-- (r `'union'` s) `'union'` t == r `'union' (s `'union'` t)
568−-- r `'union'` s `'sse'` x == r `'sse'` x && s `'sse'` x
569−-- r `'comp'` (s `'union'` t) == (r `'comp'` s) `'union'` (r `'comp'` t)
570−-- (s `'union'` t) `'comp'` r == (s `'comp'` r) `'union'` (t `'comp'` r)
567+-- (r ``union`` s) ``union`` t == r `'union' (s ``union`` t)
568+-- r ``union`` s ``sse`` x == r ``sse`` x && s ``sse`` x
569+-- r ``comp`` (s ``union`` t) == (r ``comp`` s) ``union`` (r ``comp`` t)
570+-- (s ``union`` t) ``comp`` r == (s ``comp`` r) ``union`` (t ``comp`` r)
571571-- @
572572union :: Relation a b -> Relation a b -> Relation a b
573573union a b = a + b
@@ -575,7 +575,7 @@ union a b = a + b
575575-- | Relation Kernel
576576--
577577-- @
578−-- 'ker' r == 'conv' r `'comp'` r
578+-- 'ker' r == 'conv' r ``comp`` r
579579-- 'ker' r == 'img' ('conv' r)
580580-- @
581581ker :: Relation a b -> Relation a a
@@ -584,7 +584,7 @@ ker r = conv r `comp` r
584584-- | Relation Image
585585--
586586-- @
587−-- 'img' r == r `'comp'` conv r
587+-- 'img' r == r ``comp`` conv r
588588-- 'img' r == 'ker' ('conv' r)
589589-- @
590590img :: Relation a b -> Relation b b
@@ -595,7 +595,7 @@ img r = r `comp` conv r
595595-- NOTE: _This is only valid_ if @f@ and @g@ are 'function's, i.e. 'simple' and
596596-- 'entire'.
597597--
598−-- @division f g == conv g `'comp'` f@
598+-- @'divisionF' f g == 'conv' g ``comp`` f@
599599divisionF :: Relation a c -> Relation b c -> Relation a b
600600divisionF f g = conv g `comp` f
601601
@@ -623,8 +623,8 @@ surjective = reflexive . img
623623-- relations:
624624--
625625-- @
626−-- f `'comp'` r `'sse'` s == r `'sse'` f `'comp'` s
627−-- r `'comp'` f `'sse'` s == r `'sse'` s `'comp'` f
626+-- f ``comp`` r ``sse`` s == r ``sse`` f ``comp`` s
627+-- r ``comp`` f ``sse`` s == r ``sse`` s ``comp`` f
628628-- @
629629function ::
630630 ( KnownNat (I.Count (I.Normalize b)),
@@ -683,15 +683,15 @@ bijection r = injection r && surjection r
683683
684684-- Properties of relations
685685
686−-- | A 'Relation' @r@ is 'reflexive' 'iff' @'identity' `'sse'` r@
686+-- | A 'Relation' @r@ is 'reflexive' 'iff' @'identity' ``sse`` r@
687687reflexive :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
688688reflexive r = identity <= r
689689
690−-- | A 'Relation' @r@ is 'coreflexive' 'iff' @r `'sse'` 'identity'@
690+-- | A 'Relation' @r@ is 'coreflexive' 'iff' @r ``sse`` 'identity'@
691691coreflexive :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
692692coreflexive r = r <= identity
693693
694−-- | A 'Relation' @r@ is 'transitive' 'iff' @(r `'comp'` r) `'sse'` r@
694+-- | A 'Relation' @r@ is 'transitive' 'iff' @(r ``comp`` r) ``sse`` r@
695695transitive :: Relation a a -> Bool
696696transitive r = (r `comp` r) `sse` r
697697
@@ -699,15 +699,15 @@ transitive r = (r `comp` r) `sse` r
699699symmetric :: Relation a a -> Bool
700700symmetric r = r == conv r
701701
702−-- | A 'Relation' @r@ is anti-symmetric 'iff' @(r `'intersection'` 'conv' r) `'sse'` 'identity'@
702+-- | A 'Relation' @r@ is anti-symmetric 'iff' @(r ``intersection`` 'conv' r) ``sse`` 'identity'@
703703antiSymmetric :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
704704antiSymmetric r = (r `intersection` conv r) `sse` identity
705705
706−-- | A 'Relation' @r@ is 'irreflexive' 'iff' @(r `'intersection'` 'identity') == 'zeros'@
706+-- | A 'Relation' @r@ is 'irreflexive' 'iff' @(r ``intersection`` 'identity') == 'zeros'@
707707irreflexive :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
708708irreflexive r = (r `intersection` identity) == zeros
709709
710−-- | A 'Relation' @r@ is 'connected' 'iff' @(r `'union'` 'conv' r) == 'ones'@
710+-- | A 'Relation' @r@ is 'connected' 'iff' @(r ``union`` 'conv' r) == 'ones'@
711711connected :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
712712connected r = (r `union` conv r) == ones
713713
@@ -732,7 +732,7 @@ partialEquivalence :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (
732732partialEquivalence r = partialOrder r && equivalence r
733733
734734-- | A 'Relation' @r@ is 'difunctional' or regular wherever
735−-- @r `comp` 'conv' r `comp` r == r@
735+-- @r ``comp`` 'conv' r ``comp`` r == r@
736736difunctional :: Relation a b -> Bool
737737difunctional r = r `comp` conv r `comp` r == r
738738
@@ -743,17 +743,17 @@ difunctional r = r `comp` conv r `comp` r == r
743743-- NOTE: That this is not a true categorical product, see for instance:
744744--
745745-- @
746−-- | 'p1' `'comp'` 'splitR' a b `'sse'` a
747−-- 'splitR' a b <=> |
748−-- | 'p2' `'comp'` 'splitR' a b `'sse'` b
746+-- | 'p1' ``comp`` 'splitR' a b ``sse`` a
747+-- 'splitR' a b <=> |
748+-- | 'p2' ``comp`` 'splitR' a b ``sse`` b
749749-- @
750750--
751751-- __Emphasis__ on the 'sse'.
752752--
753753-- @
754−-- 'splitR' r s `'comp'` f == 'splitR' (r `'comp'` f) (s `'comp'` f)
755−-- (R '><' S) `'comp'` 'splitR' p q == 'splitR' (r `'comp'` p) (s `'comp'` q)
756−-- 'conv' ('splitR' r s) `'comp'` 'splitR' x y == ('conv' r `'comp'` x) `'intersection'` ('conv' s `'comp'` y)
754+-- 'splitR' r s ``comp`` f == 'splitR' (r ``comp`` f) (s ``comp`` f)
755+-- (R '><' S) ``comp`` 'splitR' p q == 'splitR' (r ``comp`` p) (s ``comp`` q)
756+-- 'conv' ('splitR' r s) ``comp`` 'splitR' x y == ('conv' r ``comp`` x) ``intersection`` ('conv' s ``comp`` y)
757757-- @
758758--
759759-- @
@@ -773,7 +773,7 @@ splitR (R f) (R g) = R (I.khatri f g)
773773-- | Relational pairing first component projection
774774--
775775-- @
776−-- 'p1' `'comp'` 'splitR' r s `'sse'` r
776+-- 'p1' ``comp`` 'splitR' r s ``sse`` r
777777-- @
778778p1 ::
779779 forall a b .
@@ -789,7 +789,7 @@ p1 = R (I.kp1 @Boolean @(I.Normalize a) @(I.Normalize b))
789789-- | Relational pairing second component projection
790790--
791791-- @
792−-- 'p2' `'comp'` 'splitR' r s `'sse'` s
792+-- 'p2' ``comp`` 'splitR' r s ``sse`` s
793793-- @
794794p2 ::
795795 forall a b .
@@ -808,8 +808,8 @@ infixl 4 ><
808808-- | Relational pairing functor
809809--
810810-- @
811−-- r '><' s == 'splitR' (r `'comp'` p1) (s `'comp'` p2)
812−-- (r '><' s) `'comp'` (p '><' q) == (r `'comp'` p) '><' (s `'comp'` q)
811+-- r '><' s == 'splitR' (r ``comp`` p1) (s ``comp`` p2)
812+-- (r '><' s) ``comp`` (p '><' q) == (r ``comp`` p) '><' (s ``comp`` q)
813813-- @
814814(><) ::
815815 ( KnownNat (I.Count (I.Normalize a)),
@@ -833,14 +833,13 @@ infixl 4 ><
833833-- | Relational coproduct.
834834--
835835-- @
836−-- | 'eitherR' a b `'comp'` 'i1' == a
837−-- 'eitherR' a b <=> |
838−-- | 'eitherR' a b `'comp'` 'i2' == b
836+-- | 'eitherR' a b ``comp`` 'i1' == a
837+-- 'eitherR' a b <=> |
838+-- | 'eitherR' a b ``comp`` 'i2' == b
839839-- @
840840--
841841-- @
842−-- [R,S]·[T,U]◦= (R·T◦)∪(S·U◦)
843−-- 'eitherR' r s `'comp'` 'conv' ('eitherR' t u) == (r `'comp'` 'conv' t) `'union'` (s `'comp'` 'conv' u)
842+-- 'eitherR' r s ``comp`` 'conv' ('eitherR' t u) == (r ``comp`` 'conv' t) ``union`` (s ``comp`` 'conv' u)
844843-- @
845844--
846845-- @
@@ -853,8 +852,8 @@ eitherR = junc
853852-- | Relational coproduct first component injection
854853--
855854-- @
856−-- 'img' 'i1' `union` 'img' 'i2' == 'identity'
857−-- 'i1' `'comp'` 'i2' = 'zeros'
855+-- 'img' 'i1' ``union`` 'img' 'i2' == 'identity'
856+-- 'i1' ``comp`` 'i2' = 'zeros'
858857-- @
859858i1 ::
860859 ( KnownNat (I.Count (I.Normalize b)),
@@ -869,8 +868,8 @@ i1 = R I.i1
869868-- | Relational coproduct second component injection
870869--
871870-- @
872−-- 'img' 'i1' `union` 'img' 'i2' == 'identity'
873−-- 'i1' `'comp'` 'i2' = 'zeros'
871+-- 'img' 'i1' ``union`` 'img' 'i2' == 'identity'
872+-- 'i1' ``comp`` 'i2' = 'zeros'
874873-- @
875874i2 ::
876875 ( KnownNat (I.Count (I.Normalize b)),
@@ -887,7 +886,7 @@ infixl 5 -|-
887886-- | Relational coproduct functor.
888887--
889888-- @
890−-- r '-|-' s == 'eitherR' ('i1' `'comp'` r) ('i2' `'comp'` s)
889+-- r '-|-' s == 'eitherR' ('i1' ``comp`` r) ('i2' ``comp`` s)
891890-- @
892891(-|-) ::
893892 ( KnownNat (I.Count (I.Normalize d)),
@@ -958,7 +957,7 @@ untrans s = p1 `comp` conv (splitR (conv s) p2)
958957-- @
959958--
960959-- @
961−-- 'predR' q `'comp'` 'predR' p == 'predR' q `'union'` 'predR' p
960+-- 'predR' q ``comp`` 'predR' p == 'predR' q ``union`` 'predR' p
962961-- @
963962predR ::
964963 ( Bounded a,
@@ -988,7 +987,7 @@ equalizer f g = identity `intersection` divisionF f g
988987-- | Relational conditional guard.
989988--
990989-- @
991−-- 'guard' p = 'i2' `'overriddenBy'` 'i1' `'comp'` 'predR' p
990+-- 'guard' p = 'i2' ``overriddenBy`` 'i1' ``comp`` 'predR' p
992991-- @
993992guard ::
994993 ( Bounded b,
@@ -1015,7 +1014,7 @@ cond p r s = eitherR r s `comp` guard p
10151014-- | Relational domain.
10161015--
10171016-- For injective relations, 'domain' and 'ker'nel coincide,
1018−-- since @'ker' r `'sse'` 'identity'@ in such situations.
1017+-- since @'ker' r ``sse`` 'identity'@ in such situations.
10191018domain ::
10201019 ( KnownNat (I.Count (I.Normalize a)),
10211020 I.FromLists Boolean (I.Normalize a) (I.Normalize a)
@@ -1025,7 +1024,7 @@ domain r = ker r `intersection` identity
10251024-- | Relational range.
10261025--
10271026-- For functions, 'range' and 'img' (image) coincide,
1028−-- since@'img' f `'sse'` 'identity'@ for any @f@.
1027+-- since @'img' f ``sse`` 'identity'@ for any @f@.
10291028range ::
10301029 ( I.FromLists Boolean (I.Normalize b) (I.Normalize b),
10311030 KnownNat (I.Count (I.Normalize b))