Data.Category.Graded

Reexports

Definitions

OneOf : List Type -> Type

Visibility: public export

left : Any p xs -> Any p (xs ++ ys)

Visibility: export

right : Any p xs -> Any p (ys ++ xs)

Visibility: export

interface GradedCat : Monoid gr -> (gr -> obj -> obj -> Type) -> Type

Parameters: mon, arr
Constructor: 

MkGradedCat

Methods:

identity : arr neutral x x

(#>) : arr g1 x y -> arr g2 y z -> arr (g1 <+> g2) x z

Fixity Declaration: infixr operator, level 1

Implementation: 

{auto mon : Monoid gr} -> CoprodStrength mon f => GradedCat mon (GradedCoproductMonad f)

identity : GradedCat mon arr => arr neutral x x

Visibility: public export

(#>) : GradedCat mon arr => arr g1 x y -> arr g2 y z -> arr (g1 <+> g2) x z

Visibility: public export
Fixity Declaration: infixr operator, level 1

GradedCoproductMonad : (e -> Type) -> e -> Type -> Type -> Type

Visibility: public export

EitherGradeMor : Type -> Type -> Type -> Type

Visibility: public export

AnyErrGradeMor : List Type -> Type -> Type -> Type

Visibility: public export