Idris2Doc : Control.Category

Control.Category

(source)
Definitions
interface Category : (o -> o -> Type) -> Type
  Parameters: m
Methods:
  
identity : (a : o) -> m a a
  
cmp : m b c -> m a b -> m a c

Implementation: 
Category Morphism
identity : Category m => (a : o) -> m a a
  Visibility: public export
cmp : Category m => m b c -> m a b -> m a c
  Visibility: public export
record Op : (o -> o -> Type) -> o -> o -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkOp : m b a -> Op m a b

  Projection: 
.getOp : Op m a b -> m b a
.getOp : Op m a b -> m b a
  Visibility: public export
getOp : Op m a b -> m b a
  Visibility: public export
data ProdC : (o1 -> o1 -> Type) -> (o2 -> o2 -> Type) -> (o1, o2) -> (o1, o2) -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkProdC : m1 a1 b1 -> m2 a2 b2 -> ProdC m1 m2 (a1, a2) (b1, b2)