TwoCatOfCats

TwoCatOfCats is a safe version of Internal.TwoCatOfCats. Please refer to the documentation for that module.

This module does not export the unsafe constructors in Internal.TwoCatOfCats, but does export the safe versions. For example, CompositeFunctor :: ZeroGlobelet -> [Functor] -> Functor is not exported, but func_compose :: [Functor] -> Maybe Functor is. This is because one can use CompositeFunctor to construct invalid composite functors. See the documentation in Internal.TwoCatOfCats for more details.

Documentation

data Category

A representation of a category.

Constructors

Category

Fields

• cat_id :: !String

  the name of the category

• cat_displayString :: !String

  LaTeX code for displaying the category

Instances

Eq Category

Defined in Internal.TwoCatOfCats

Methods

(==) :: Category -> Category -> Bool

(/=) :: Category -> Category -> Bool

Show Category

Defined in Internal.TwoCatOfCats

Methods

showsPrec :: Int -> Category -> ShowS

show :: Category -> String

showList :: [Category] -> ShowS

Structure Category

Defined in SDNamespace

Methods

get_id :: Category -> String

struct_str :: Category -> String

sdns_lens :: Category -> Lens' SDNamespace (Namespace Category)

insertion_error_msg :: Category -> String

data ZeroGlobelet

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

• glob0_source :: !Category

  source category

• glob0_target :: !Category

  target category

Instances

Eq ZeroGlobelet

Defined in Internal.TwoCatOfCats

Methods

(==) :: ZeroGlobelet -> ZeroGlobelet -> Bool

(/=) :: ZeroGlobelet -> ZeroGlobelet -> Bool

Show ZeroGlobelet

Defined in Internal.TwoCatOfCats

Methods

showsPrec :: Int -> ZeroGlobelet -> ShowS

show :: ZeroGlobelet -> String

showList :: [ZeroGlobelet] -> ShowS

data Functor

A representation of a functor between categories.

Constructors

Functor !String !String !ZeroGlobelet !String

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

Instances

Eq Functor

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.

Defined in Internal.TwoCatOfCats

Methods

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

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

Show Functor

Defined in Internal.TwoCatOfCats

Methods

showsPrec :: Int -> Functor -> ShowS

show :: Functor -> String

showList :: [Functor] -> ShowS

Structure Functor

Defined in SDNamespace

Methods

get_id :: Functor -> String

struct_str :: Functor -> String

sdns_lens :: Functor -> Lens' SDNamespace (Namespace Functor)

insertion_error_msg :: Functor -> String

func_boundary :: Functor -> ZeroGlobelet

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

func_source :: Functor -> Category

func_source gives the source category of a functor.

func_target :: Functor -> Category

func_target gives the target category of a functor.

identityFunctor :: Category -> Functor

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

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

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

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

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

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]

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

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_basic_func :: Functor -> Bool

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

is_identity_func :: Functor -> Bool

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

data OneGlobelet

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.

Instances

Show OneGlobelet

Defined in Internal.TwoCatOfCats

Methods

showsPrec :: Int -> OneGlobelet -> ShowS

show :: OneGlobelet -> String

showList :: [OneGlobelet] -> ShowS

funcs_globeletable :: Functor -> Functor -> Bool

(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

(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

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

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

A representation of a natural transformation between functors.

Constructors

NaturalTransformation !String !String !String !OneGlobelet !String

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.

Instances

Show NaturalTransformation

Defined in Internal.TwoCatOfCats

Methods

showsPrec :: Int -> NaturalTransformation -> ShowS

show :: NaturalTransformation -> String

showList :: [NaturalTransformation] -> ShowS

Structure NaturalTransformation

Defined in SDNamespace

Methods

get_id :: NaturalTransformation -> String

struct_str :: NaturalTransformation -> String

sdns_lens :: NaturalTransformation -> Lens' SDNamespace (Namespace NaturalTransformation)

insertion_error_msg :: NaturalTransformation -> String

nat_boundary :: NaturalTransformation -> OneGlobelet

nat_boundary of a natural transformation is its boundary globelet.

nat_source :: NaturalTransformation -> Functor

nat_source of a natural transformation is its source functor.

nat_target :: NaturalTransformation -> Functor

nat_target of a natural transforamtion is its target functor.

identityNaturalTransformation :: Functor -> NaturalTransformation

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_compose :: [NaturalTransformation] -> Maybe NaturalTransformation

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

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

Constructors

NatHorzCompositionError [Int]

nat_horz_compose_with_error :: [NaturalTransformation] -> Except NatHorzCompositionError NaturalTransformation

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_compose :: [NaturalTransformation] -> Maybe NaturalTransformation

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

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

nat_target_length :: NaturalTransformation -> Int

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

is_basic_nt :: NaturalTransformation -> Bool

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

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