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

Monocle.Core

Contents

Synopsis

Morphism

class Eq a => Morphism a whereSource

Class of morphisms.

Methods

dom :: a -> aSource

Returns domain of the given morphism.

cod :: a -> aSource

Returns codomain of the given morphism.

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

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 tensorial Id to the given object.

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

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

object :: a -> Mor aSource

Creates object (actually it's id). Same as objectId.

objectId :: a -> Mor aSource

Creates object id. Same as object.

tid :: Mor aSource

Tensorial Id, 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