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

Monocle.Core

Synopsis

# Morphism

class Eq a => Morphism a whereSource

Class of morphisms.

Methods

dom :: a -> aSource

Returns domain of the given morphism (actually its id).

cod :: a -> aSource

Returns codomain of the given morphism (actually its id).

isId :: a -> BoolSource

Checks whether morphism is id.

(\.) :: a -> a -> aSource

Composition of two morphisms (should be associative).

(\*) :: a -> a -> aSource

Tensor product of two morphisms.

Instances

 Eq a => Morphism (Mor a) Eq a => Morphism (Lab a)

data FuncT Source

Types of the functional modifier.

Constructors

 Function Function on objects Functor Covariant functor Cofunctor Contravariant functor

Instances

 Eq FuncT Ord FuncT

data Mor a Source

Morphism data type

Constructors

 Arrow a (ArrowData a) Atomary morphism Id a Identity morphism Tensor [Mor a] Tensor product of morphisms Composition [Mor a] Composition of morphisms Func String [Mor a] FuncT Functionional modifier Transform String (Mor a) [Mor a] Naturally transformational modifier

Instances

 Eq a => Eq (Mor a) Ord a => Ord (Mor a) (Printable a, Eq a) => Show (Mor a) (Printable a, Eq a) => Printable (Mor a) Eq a => Morphism (Mor a) (Printable a, Ord a) => Texified (Mor a)

# Basic functions on morphisms

nrm :: Eq t => Mor t -> Mor tSource

Normalizes the term representing morphism, e.g. turns `((a \* b) \* c)` to `(a \* b \* c)`

atomary :: Eq t => Mor t -> BoolSource

Checks whether morphism is an atomary formula.

arrow :: a -> Mor a -> Mor a -> Mor aSource

Creates `Arrow` by morphism information (e.g. name), domain and codomain.

element :: a -> Mor a -> Mor aSource

Creates generalized element, i.e. an arrow from the identity object to the given object.

coelement :: a -> Mor a -> Mor aSource

Creates generalized coelement, i.e. an arrow from the the given object to the identity object.

object :: a -> Mor aSource

Creates object (actually its id). Same as `objectId`.

objectId :: a -> Mor aSource

Creates object id. Same as `object`.

tid :: Mor aSource

Identity object, `tid \* f == f` in strict monoidal category.

# Tensor product functoriality

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

Turns recursively `(a \* b) \. (c \* d)` to `(a \. c) \* (b \. d)`.

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

Turns recursively `(a \. c) \* (b \. d)` to `(a \* b) \. (c \* d)`.

# Utilities

collect :: (Num b, Ord a) => Mor a -> Map (Mor a) bSource

Collects atomary subterms of the given arrow as keys of the map.

# Rules

data Rule a Source

Rule type

Constructors

 DefEqual (Mor a) (Mor a) Declares equality of two morphisms

Instances

 (Printable a, Eq a) => Show (Rule a) (Printable a, Ord a) => Texified (Rule a)

(\==) :: Mor a -> Mor a -> Rule aSource

`x \== y` is the same as `DefEqual x y`

apply :: Eq a => Rule String -> Mor a -> Mor aSource

Applies the `Rule` to the given morphism