Monocle.Rules

Duality

ldual'of :: Mor a -> Mor a

For given object create it's left dual: http://en.wikipedia.org/wiki/Dual_object.

ldual :: Mor a -> Mor a

Same as ldual'of, for usage in calculations.

ldual'r :: Mor a -> Mor a

Same as ldual'of, for usage in rule descriptions.

rdual'of :: Mor a -> Mor a

For given object create it's right dual: http://en.wikipedia.org/wiki/Dual_object.

rdual :: Mor a -> Mor a

Same as rdual'of, for usage in calculations.

rdual'r :: Mor a -> Mor a

Same as rdual'of, for usage in rule descriptions.

unit'of :: Eq a => a -> Mor a -> Mor a -> Mor a

For given dual pair of objects (x, y) and name nm call unit'of nm x y to create named duality unit arrow. Generates error if (x, y) is not a dual pair.

unit :: Mor String -> Mor String -> Mor String

Same as unit'of "\\eta", for usage in calculations.

unit'r :: Mor String -> Mor String -> Mor String

Same as unit'of "*\\eta", except that it does not check duality. For usage in rule descriptions.

counit'of :: Eq a => a -> Mor a -> Mor a -> Mor a

For given dual pair of objects (x, y) and name nm call counit'of nm x y to create named duality counit arrow. Generates error if (x, y) is not a dual pair.

counit :: Mor String -> Mor String -> Mor String

Same as counit'of "\\epsilon", for usage in calculations.

counit'r :: Mor String -> Mor String -> Mor String

Same as counit'of "*\\epsilon", except that it does not check duality. For usage in rule descriptions.

zigzag'rule'Left :: Rule String

One of "zigzag rules" for duality.

zigzag'rule'Right :: Rule String

One of "zigzag rules" for duality.

Braiding

braid'of :: Eq a => a -> Mor a -> Mor a -> Mor a

For given pair of objects (x, y) and name nm call braid'of nm x y to create named braid arrow: http://en.wikipedia.org/wiki/Braided_monoidal_category

braid :: Mor String -> Mor String -> Mor String

Same as braid'of "\\beta", for usage in calculations.

braid'r :: Mor String -> Mor String -> Mor String

Same as braid'of "*\\beta", for usage in rule descriptions.

unbraid'of :: Eq a => a -> Mor a -> Mor a -> Mor a

For given pair of objects (x, y) and name nm call unbraid'of nm x y to create named unbraid arrow (inverse of braid arrow).

unbraid :: Mor String -> Mor String -> Mor String

Same as unbraid'of "\\beta^{-1}", for usage in calculations.

unbraid'r :: Mor String -> Mor String -> Mor String

Same as unbraid'of "*\\beta^{-1}", for usage in rule descriptions.

braid'rule'Iso'Left :: Rule String

Isomorphism rule: unbraid as inverse of braid.

braid'rule'Iso'Right :: Rule String

Isomorphism rule: braid as inverse of unbraid.

braid'rule'Nat'Left :: Rule String

Naturality rule on the "left wire".

braid'rule'Nat'Right :: Rule String

Naturality rule on the "right wire".

braid'rule'Hex'Braid :: Rule String

Hexagon identity for braid, strict monoidal case.

braid'rule'Hex'Unbraid :: Rule String

Hexagon identity for unbraid, strict monoidal case.

Symmetry

cross'rule :: Rule String

Rule for the "cross" arrow: it's simply self-inverse braid.

Twisting

twist'of :: Eq a => a -> Mor a -> Mor a

For given object x and name nm call twist'of nm x to create named twist arrow.

twist :: Mor String -> Mor String

Same as twist'of "\\theta", for usage in calculations.

twist'r :: Mor String -> Mor String

Same as twist'of "*\\theta", for usage in rule descriptions.

untwist'of :: Eq a => a -> Mor a -> Mor a

For given object x and name nm call untwist'of nm x to create named untwist arrow.

untwist :: Mor String -> Mor String

Same as untwist'of "\\theta^{-1}", for usage in calculations.

untwist'r :: Mor String -> Mor String

Same as untwist'of "*\\theta^{-1}", for usage in rule descriptions.

twist'rule'Iso'Left :: Rule String

Isomorphism rule: untwist as inverse of twist.

twist'rule'Iso'Right :: Rule String

Isomorphism rule: twist as inverse of untwist.

twist'rule'Id :: Rule String

Twisting the identity object changes nothing.

twist'rule'Natural :: Rule String

Twisting naturality.

twist'rule'Braid :: Rule String

Twist/braid interaction.

Dagger

dagger'of :: Eq a => Mor a -> Mor a

dagger'of f creates daggered version of the arrow f.

dagger :: Eq a => Mor a -> Mor a

Same as dagger'of, for usage in calculations.

dagger'r :: Eq a => Mor a -> Mor a

Same as dagger'of, for usage in rule descriptions.

dagger'rule'Id :: Rule String

As contravariant functor dagger maps id's to id's.

dagger'rule'Cofunctor :: Rule String

dagger is contravariant functor, i.e. inverts composition order.

dagger'rule'Inv :: Rule String

dagger involution rule.