tikzsd-1.0.0: A program for generating LaTeX code of string diagrams.
CopyrightAnthony Wang 2021
LicenseMIT
Maintaineranthony.y.wang.math@gmail.com
Safe HaskellSafe-Inferred
LanguageHaskell2010

Internal.TwoCatOfCats

Description

Internal.TwoCatOfCats defines data structures used to represent the categories, functors and natural transformations which are to be rendered by tikzsd into TikZ picture code.

Currently, the structures defined in this module include data relating how they are displayed by tikzsd, while the functions in the module relate purely to category theory. I plan on rewriting this module so that it is only about category theory, separating out the display aspects in another module. In the future, this may allow greater flexibility in how objects are displayed.

Synopsis

Documentation

data Category Source #

A representation of a category.

Constructors

Category 

Fields

data ZeroGlobelet Source #

A ZeroGlobelet is the structure representing the boundary of a functor (i.e. 1-morphism). It consists of a source Category and a target Category.

Constructors

ZeroGlobelet 

Fields

Instances

Instances details
Eq ZeroGlobelet Source # 
Instance details

Defined in Internal.TwoCatOfCats

Show ZeroGlobelet Source # 
Instance details

Defined in Internal.TwoCatOfCats

data Functor Source #

A representation of a functor between categories.

Constructors

Functor

A data structure specifying a new functor. We shall call Functors of the form (Functor id ds bg o) basic functors.

Fields

CompositeFunctor

A data structure for specifying compositions of functors. A Functor of the form (CompositeFunctor bg fl) is assumed to satisfy the axiom that the functors in the list fl can be composed and that bg is a valid boundary for the composition. We shall call such functors composite functors.

Explicitly, the target of each functor in fl is the source of the next functor in the list. Moreover, if fl is empty, then the source and target of bg must be the same. (This represents an identity functor). Otherwise, the source of bg is equal to the source of the first functor in fl, and the target of bg is equal to the target of the last functor in fl.

See identityFunctor, func_compose and func_compose_with_error for functions which compose functors safely.

Fields

Instances

Instances details
Eq Functor Source #

Two basic functors are deemed equal if func_id and func_boundaryGlobelet are equal. After this identification, two Functors are equal if they describe the same morphism in the free category generated by the basic functors.

Instance details

Defined in Internal.TwoCatOfCats

Methods

(==) :: Functor -> Functor -> Bool #

(/=) :: Functor -> Functor -> Bool #

Show Functor Source # 
Instance details

Defined in Internal.TwoCatOfCats

Structure Functor Source # 
Instance details

Defined in SDNamespace

func_boundary :: Functor -> ZeroGlobelet Source #

A boundary globelet function which works for both basic and composite functors.

func_source :: Functor -> Category Source #

func_source gives the source category of a functor.

func_target :: Functor -> Category Source #

func_target gives the target category of a functor.

identityFunctor :: Category -> Functor Source #

identityFunctor takes a category C and returns the identity functor of that category. The identity functor is represented by a composite functor whose underlying cfg_functorList is empty.

func_composable :: [Functor] -> Bool Source #

func_composable takes a list of functors and returns True if the list of functors can be composed (without specifying additional information), and False otherwise. func_composable will return False on an empty list, since a source (or target) category needs to be specified. Function composition is left to right, so [F,G] represents a composition of F : A -> B and G : B -> C.

func_compose :: [Functor] -> Maybe Functor Source #

func_compose takes a list of functors and returns Just their composite if func_composable is True and Nothing if func_composable is False.

data FuncCompositionError Source #

FuncCompositionError is the type of error which can be thrown by func_compose_with_error.

FunctorCompositionError [] is the error for an empty composition.

Otherwise, an error is given by (FuncCompositionError list) where list is a list of positions where the functors do not compose. n is in list if the functors in positions n and n+1 do not compose. (Indexing starts at 0).

Constructors

FuncCompositionError [Int] 

func_compose_with_error :: [Functor] -> Except FuncCompositionError Functor Source #

func_compose_with_error takes a list of functors and composes them. It throws a FuncCompositionError describing why composition failed if the functors in the list could not be composed.

func_to_single_composition :: Functor -> Functor Source #

func_to_single_composition of f gives a functor of the form (CompositeFunctor bd fl) which is equal to f, where fl is a list of basic functors.

func_to_single_list :: Functor -> [Functor] Source #

func_to_single_list f returns the empty list if f is an identity functor. Otherwise, it returns a list of basic functors whose composition is equal to f.

func_reduced_length :: Functor -> Int Source #

func_reduced_length returns the length of func_to_single_list. For example func_reduced_length of an identity functor is 0, while func_reduced_length of a basic functor is 1.

is_identity_func :: Functor -> Bool Source #

is_identity_func of a functor is True if the functor is an identity functor and False otherwise.

is_basic_func :: Functor -> Bool Source #

is_basic_func of a functor is True if the functor is a basic functor, and False otherwise.

data OneGlobelet Source #

OneGlobelet is the structure representing the boundary of a natural transformation (i.e. 2-morphism). (OneGlobelet s t) represents a globelet with source functor s and target functor t, and is assumed to satisfy the following axiom:

func_boundary s == func_boundary t

See funcs_to_globelet for safe construction of OneGlobelets.

Constructors

OneGlobelet 

Fields

Instances

Instances details
Show OneGlobelet Source # 
Instance details

Defined in Internal.TwoCatOfCats

funcs_globeletable :: Functor -> Functor -> Bool Source #

(funcs_globeletable source target) is True if the Functors source and target have the same boundary globelet, i.e. they have the same source category and the same target category, and False otherwise.

funcs_to_globelet :: Functor -> Functor -> Maybe OneGlobelet Source #

(funcs_to_globelet source target) is Just the OneGlobelet with source source and target target if (funcs_globeletable source target)=True, and Nothing otherwise.

glob1_pos :: OneGlobelet -> Category Source #

glob1_pos of a OneGlobelet is equal to the source category of the source functor of the OneGlobelet. Equivalently, it is equal to the source category of the target functor of the OneGlobelet. We shall refer to this category as the positive pole of the OneGlobelet.

glob1_neg :: OneGlobelet -> Category Source #

glob1_neg of a OneGlobelet is equal to the target category of the target functor of the OneGlobelet. Equivalently, it is equal to the target category of the source functor of the OneGlobelet. We shall refer to this category as the negative pole of the OneGlobelet.

data NaturalTransformation Source #

A representation of a natural transformation between functors.

Constructors

NaturalTransformation

A data structure specifying a new natural transformation. We shall call natural transformations of the form (NaturalTransformation id ds ss bg o) basic natural transformations.

Fields

NatTransHorizontalComposite

A data structure for specifying a horizontal composition of natural transformations. A NaturalTransformation of the form (NatTransHorizontalComposite bg ntl) is assumed to satisfy the axiom that ntl is a list of natural transformations which can be horizontally composed, with bg the boundary for the composition.

Explicitly, ntl is a non-empty list of NaturalTransformations such that the negative pole of each natural transformation in the list is the positive pole of the next element in the list. The source of bg is equal to the composition of the source functors of the natural transformations in ntl and the target of bg is equal to the composition of the target functors of the natural transformations in ntl.

See the nat_horz_compose and nat_horz_compose_with_error functions for safe horizontal composition of natural transformations.

Fields

NatTransVerticalComposite

A data structure for specifying a vertical composition of natural transformations. A NaturalTransformation of the form (NatTransVerticalComposite bg ntl) is assumed to satisfy the axiom that ntl is a list of natural transformations which can be vertically composed, with bg a valid boundary for the composition.

Explicitly, ntl is a list of NaturalTransformations such that the target functor of each natural transformation in the list is equal to the source functor of the next natural transformation. If ntl is empty, then the source and target functors of bg must be equal. (This represents an identity natural transformation.) Otherwise, the source functor of bg is equal to the source functor of the first natural transformation in ntl and the target functor of bg is equal to the target functor of the last natural transformation in ntl.

See identityNaturalTransformation and nat_vert_compose for functions which vertically compose natural transformations safely.

Fields

nat_boundary :: NaturalTransformation -> OneGlobelet Source #

nat_boundary of a natural transformation is its boundary globelet.

nat_source :: NaturalTransformation -> Functor Source #

nat_source of a natural transformation is its source functor.

nat_target :: NaturalTransformation -> Functor Source #

nat_target of a natural transforamtion is its target functor.

nat_pos :: NaturalTransformation -> Category Source #

nat_pos of a natural transformation is its positive pole which we define to be the positive pole of its boundary globelet, i.e. the source of its source, or equivalently, the source of its target.

nat_neg :: NaturalTransformation -> Category Source #

nat_neg of a natural transformation is its negative pole which we define to be the negative pole of its boundary globelet, i.e. the target of its target, or equivalently, the target of its source.

identityNaturalTransformation :: Functor -> NaturalTransformation Source #

identityNaturalTransformation takes a Functor as an argument and returns its identity natural transformation. The identity natural transformation is represented by a vertical composition whose nt_vert_comp_list is empty.

nat_horz_composable :: [NaturalTransformation] -> Bool Source #

nat_horz_composable takes a list of natural transformations and returns True if the natural transformations can be horizontally composed, and False otherwise.

nat_horz_compose :: [NaturalTransformation] -> Maybe NaturalTransformation Source #

nat_horz_compose takes a list of natural transformations and returns Just their horizontal composition if they are horizontally composable, and Nothing otherwise.

data NatHorzCompositionError Source #

NatHorzCompositionError is the possible error thrown by nat_horz_compose_with_error.

(NatHorzCompositionError []) represents an empty horizontal composition.

Otherwise, an error is given by (NatHorzCompositionError list) where list is a list of positions where the natural transformations do not horizontally compose. n is in list if the negative pole of the natural transformation in position n is not equal to the positive pole of the natural transformation in position n+1. (Indexing starts at 0).

nat_horz_compose_with_error :: [NaturalTransformation] -> Except NatHorzCompositionError NaturalTransformation Source #

nat_horz_compose_with_error takes a list of natural transformations and returns their horizontal composition. It throws a NatHorzCompositionError describing why composition failed if the list of natural transformations cannot be horizontally composed. Composition is from left to right.

nat_vert_composable :: [NaturalTransformation] -> Bool Source #

nat_vert_composable takes a list of natural transformations and returns True if the list of natural transformations can be vertically composed (without specifying additional information), and False otherwise. nat_vert_composable will return False on an empty list since a source (or target) functor needs to be specified.

nat_vert_compose :: [NaturalTransformation] -> Maybe NaturalTransformation Source #

nat_vert_compose takes a list of natural transformations and returns Just their vertical composition if the list is vertically composable, and Nothing otherwise.

nat_source_length :: NaturalTransformation -> Int Source #

nat_source_length of a natural transformation is the func_reduced_length of its source functor.

nat_target_length :: NaturalTransformation -> Int Source #

nat_target_length of a natural transformation is the func_reduced_length of its target functor.

is_basic_nt :: NaturalTransformation -> Bool Source #

is_basic_nt of a natural transformation is True if the natural transformation is a basic natural transformation, and false otherwise.

is_identity_nt :: NaturalTransformation -> Bool Source #

is_identity_nt of a natural transformation is True if the natural transformation is the identity of some functor, and False otherwise.