Cat.FinCat

The FinCat category has as objects finite categories and as morphisms functors between them. It is itself a large category (therefore not a finite one), we only construct finite full subcategories of the mathematical infinite FinCat category. FinCat is the type of full finite subcategories of FinCat.

To instantiate it, use the FinCat constructor on a list of categories.

For example, see ExampleCat.ExampleCat

The FinCat type should not be confused with the FiniteCategory typeclass.

The FiniteCategory typeclass describes axioms a structure should follow to be considered a finite category.

The FinCat type is itself a FiniteCategory and contains finite categories as objects.

To convert a FinFunctor into any other kind of functor, see Diagram.Conversion.

Documentation

data FinFunctor c m o

A FinFunctor F between two categories is a map between objects and a map between arrows of the two categories such that :

F (srcF f) = srcF (F f)

F (tgtF f) = tgtF (F f)

F (f @ g) = F(f) @ F(g)

F (identity a) = identity (F a)

It is meant to be a morphism between categories within FinCat, it is homogeneous, the type of the source category must be the same as the type of the target category.

See Diagram for heterogeneous ones.

To convert a FinFunctor into any other kind of functor, see Diagram.Conversion.

Constructors

FinFunctor

Fields

• srcF :: c
• tgtF :: c
• omapF :: AssociationList o o
• mmapF :: AssociationList m m

Instances

(Eq c, Eq o, Eq m) => Eq (FinFunctor c m o)

Defined in Cat.FinCat

Methods

(==) :: FinFunctor c m o -> FinFunctor c m o -> Bool

(/=) :: FinFunctor c m o -> FinFunctor c m o -> Bool

(Show c, Show o, Show m) => Show (FinFunctor c m o)

Defined in Cat.FinCat

Methods

showsPrec :: Int -> FinFunctor c m o -> ShowS

show :: FinFunctor c m o -> String

showList :: [FinFunctor c m o] -> ShowS

(FiniteCategory c m o, Morphism m o, PrettyPrintable c, PrettyPrintable m, PrettyPrintable o, Eq m, Eq o) => PrettyPrintable (FinFunctor c m o)

Defined in Cat.FinCat

Methods

pprint :: FinFunctor c m o -> String

(Eq c, Eq m, Eq o) => Morphism (FinFunctor c m o) c

Defined in Cat.FinCat

Methods

(@) :: FinFunctor c m o -> FinFunctor c m o -> FinFunctor c m o

source :: FinFunctor c m o -> c

target :: FinFunctor c m o -> c

(FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => GeneratedFiniteCategory (FinCat c m o) (FinFunctor c m o) c

Defined in Cat.FinCat

Methods

genAr :: FinCat c m o -> c -> c -> [FinFunctor c m o]

decompose :: FinCat c m o -> FinFunctor c m o -> [FinFunctor c m o]

genArrows :: FinCat c m o -> [FinFunctor c m o]

(FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => FiniteCategory (FinCat c m o) (FinFunctor c m o) c

Defined in Cat.FinCat

Methods

ob :: FinCat c m o -> [c]

identity :: FinCat c m o -> c -> FinFunctor c m o

ar :: FinCat c m o -> c -> c -> [FinFunctor c m o]

arrows :: FinCat c m o -> [FinFunctor c m o]

newtype FinCat c m o

An instance of FinCat is a list of categories of interest.

Listing all arrows between two objects (i.e. listing FinFunctors between two categories) is slow (there are a lot of candidates).

Constructors

FinCat [c]

Instances

(FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => GeneratedFiniteCategory (FinCat c m o) (FinFunctor c m o) c

Defined in Cat.FinCat

Methods

genAr :: FinCat c m o -> c -> c -> [FinFunctor c m o]

decompose :: FinCat c m o -> FinFunctor c m o -> [FinFunctor c m o]

genArrows :: FinCat c m o -> [FinFunctor c m o]

(FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => FiniteCategory (FinCat c m o) (FinFunctor c m o) c

Defined in Cat.FinCat

Methods

ob :: FinCat c m o -> [c]

identity :: FinCat c m o -> c -> FinFunctor c m o

ar :: FinCat c m o -> c -> c -> [FinFunctor c m o]

arrows :: FinCat c m o -> [FinFunctor c m o]