Idris2Doc : Pipeline.Category

Pipeline.Category

(source)
Reexports
import public Data.Vect
import public Data.Vect.Utils
import public Data.Vect.Quantifiers
Definitions
0 ImplCat : Vect (2 + n) obj -> Type
  Visibility: public export
RunCat : Category arr => (p : Vect (2 + n) obj) -> ImplCat p -> arr (head p) (last p)
  Visibility: export
interface CoprodStrength : Monoid a -> (a -> Type) -> Type
  Parameters: mon, f
Constructor: 
MkFCoprod

Methods:
  
left : f x -> f (x <+> y)
  
right : f y -> f (x <+> y)

Implementations:
  
CoprodStrength EitherMon (\x => x)
  
CoprodStrength AnyMon OneOf
left : CoprodStrength mon f => f x -> f (x <+> y)
  Visibility: export
right : CoprodStrength mon f => f y -> f (x <+> y)
  Visibility: export
MkInst : {auto mon : Monoid gr} -> CoprodStrength mon f => GradedCat mon (GradedCoproductMonad f)
  Visibility: public export
foldGrades : Monoid gr => Vect (S n) gr -> gr
  Visibility: public export
0 ImplGr : Vect (2 + n) obj -> Vect (S n) gr -> Type
  Visibility: public export
RunGrCat : {auto mon : Monoid gr} -> GradedCat mon arr -> (p : Vect (2 + n) obj) -> (grades : Vect (S n) gr) -> ImplGr p grades -> arr (foldGrades grades) (head p) (last p)
  Visibility: export