Math.Categories.FinCat

The FinCat category has as objects finite categories and as morphisms homogeneous functors between them.

Functors must be homogeneous because otherwise we would not be able to compose them with the Morphism typeclass.

The FinCat datatype 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 Category.

A FinFunctor is a Diagram where the source and target category are the same. The source category of a FinFunctor should be finite.

Homogeneous functor

type FinFunctor c m o = Diagram c m o c m o

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

funct ->$ (source f) == source (funct ->£ f)

funct ->$ (target f) == target (funct ->£ f)

funct ->£ (f @ g) = (funct ->£ f) @ (funct ->£ g)

funct ->£ (identity a) = identity (funct ->$ a)

A FinFunctor is a type of Diagram.

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 in Math.Categories.FunctorCategory for heterogeneous ones.

FinCat

data FinCat c m o

The FinCat category has as objects finite categories and as morphisms homogeneous functors between them.

Constructors

FinCat

Instances

Eq (FinCat c m o)

Defined in Math.Categories.FinCat

Methods

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

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

Show (FinCat c m o)

Defined in Math.Categories.FinCat

Methods

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

show :: FinCat c m o -> String

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

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

Defined in Math.Categories.FinCat

Methods

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

ar :: FinCat c m o -> c -> c -> Set (Diagram c m o c m o)

genAr :: FinCat c m o -> c -> c -> Set (Diagram c m o c m o)

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

Orphan instances

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

Methods

(@?) :: Diagram c m o c m o -> Diagram c m o c m o -> Maybe (Diagram c m o c m o)

source :: Diagram c m o c m o -> c

target :: Diagram c m o c m o -> c