
  0 | module Data.CT.DependentAction.Definition
  1 | 
  2 | import Data.CT.Category.Definition
  3 | import Data.CT.Category.Instances
  4 | import Data.CT.Functor.Definition
  5 | import Data.CT.Functor.Instances
  6 | 
  7 | public export
  8 | record DepAct (c : Cat) (i : IndCat c) where
  9 |   constructor MkDepAct
 10 |   Act : (x : c.Obj) -> Functor (i.mapObj x) c
 11 | 
 12 |