Monocle-0.0.4: Symbolic computations in strict monoidal categories with LaTeX output.

Monocle.Rules

Contents

Synopsis

# Duality

ldual'of :: Mor a -> Mor aSource

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

ldual :: Mor a -> Mor aSource

Same as ldual'of, for usage in calculations.

ldual'r :: Mor a -> Mor aSource

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

rdual'of :: Mor a -> Mor aSource

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

rdual :: Mor a -> Mor aSource

Same as rdual'of, for usage in calculations.

rdual'r :: Mor a -> Mor aSource

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

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

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.

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

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 aSource

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.

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

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

One of "zigzag rules" for duality.

One of "zigzag rules" for duality.

# Braiding

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

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

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

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

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

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).

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

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

Isomorphism rule: unbraid as inverse of braid.

Isomorphism rule: braid as inverse of unbraid.

Naturality rule on the "left wire".

Naturality rule on the "right wire".

Hexagon identity for braid, strict monoidal case.

Hexagon identity for unbraid, strict monoidal case.

# Symmetry

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

# Twisting

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

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

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

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

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

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

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

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

Isomorphism rule: untwist as inverse of twist.

Isomorphism rule: twist as inverse of untwist.

Twisting the identity object changes nothing.

Twisting naturality.

Twist/braid interaction.

# Dagger

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

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

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

Same as dagger'of, for usage in calculations.

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

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

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

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

dagger involution rule.