Safe Haskell	None
Language	GHC2021

Data.InternalCategory.Morphism

Synopsis

data Mor k (cat :: k -> k -> Type) where
- Morphism :: forall k (a :: k) (b :: k) (cat :: k -> k -> Type). Sing a -> Sing b -> cat a b -> Mor k cat
identityMorphism :: forall k (cat :: k -> k -> Type). Category cat => SomeSing k -> Mor k cat
composeMorphism :: forall k (cat :: k -> k -> Type). (Category cat, SDecide k) => Mor k cat -> Mor k cat -> Maybe (Mor k cat)

Documentation

data Mor k (cat :: k -> k -> Type) where Source #

Sum of all morphisms in cat.

Constructors

Morphism :: forall k (a :: k) (b :: k) (cat :: k -> k -> Type). Sing a -> Sing b -> cat a b -> Mor k cat

Instances details

(Category cat, SDecide k) => ICategory (SomeSing k) (Mor k cat) Source #
Instance details Defined in Data.InternalCategory.Morphism Methods foldPath :: Path (SomeSing k) (Mor k cat) -> Mor k cat Source #
IQuiver (SomeSing k) (Mor k cat) Source #
Instance details Defined in Data.InternalCategory.Morphism Methods src :: Mor k cat -> SomeSing k Source # tgt :: Mor k cat -> SomeSing k Source #

identityMorphism :: forall k (cat :: k -> k -> Type). Category cat => SomeSing k -> Mor k cat Source #

composeMorphism :: forall k (cat :: k -> k -> Type). (Category cat, SDecide k) => Mor k cat -> Mor k cat -> Maybe (Mor k cat) Source #