ICategory ob mor defines a category "internal to" Type.

There are two ways to define ICategory: with identity and compose or with foldPath.

Definition by identity, compose

This is how internal categories are usually defined: by giving identity morphisms and composition of two morphisms, satisfying the following laws:

Domain and codomain of identity v:

   dom (identity v) == cod (identity v) == v
   

compose is defined exactly on matching morphisms:

   isJust (compose f g) == (cod f == dom g)
   

Domain and codomain of compose f g:

For all f,g,h such that compose f g == Just h,

   dom h == dom f, cod h == cod g
   

Left and Right Unit:

   identity (dom f) compose f == Just f
   

   f compose identity (cod f) == Just f
   

Associativity:

For all f,g,h,

   (compose f g >>= fg -> compose fg h)
     ==
   (compose g h >>= gh -> compose f gh)
   

Given identity and compose operation, foldPath p can be defined as the composition morAll of all morphisms in p (and the identity at source in a case of empty path,) which is guaranteed to be Just morAll and not Nothing.

Definition by foldPath:

This is an alternative definition by giving how to collapse any path on IQuiver ob mor into mor, satisfying the following laws.

folding doesn't change endpoints:

   dom (foldPath p) == dom p
   

   cod (foldPath p) == cod p
   

folding commutes with concatPath:

For any pp :: Path ob (Path ob mor),

   foldPath (concatPath pp) = foldPath (errMapPath id foldPath pp)
   

Note that from folding doesn't change endpoints law, errMapPath id foldPath must be a total function.

folding single edge does nothing:

   foldPath (singlePath f) = f
   

Given foldPath, one can defined identity and compose satisfying the laws above, as

identity :: ob -> mor
identity = foldPath . emptyPath

compose :: mor -> mor -> Maybe mor
compose f g = foldPath $ composePath (singlePath f) (singlePath g)

Class for Quiver represented by types of edges and vertices