Idris2Doc : Data.CT.DependentAction.Definition

Data.CT.DependentAction.Definition

(source)
Definitions
record DepAct : (c : Cat) -> IndCat c -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkDepAct : ((x : c .Obj) -> Functor (i .mapObj x) c) -> DepAct c i

  Projection: 
.Act : DepAct c i -> (x : c .Obj) -> Functor (i .mapObj x) c
.Act : DepAct c i -> (x : c .Obj) -> Functor (i .mapObj x) c
  Totality: total
  Visibility: public export
Act : DepAct c i -> (x : c .Obj) -> Functor (i .mapObj x) c
  Totality: total
  Visibility: public export