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 => SOb 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

identityMorphism :: forall k (cat :: k -> k -> Type). Category cat => SOb 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 #