Data.CT.DependentPara.Definition

Definitions

record DepParaMor : DepAct c m -> c .Obj -> c .Obj -> Type

  Data structure holding the morphisms of dependent para

Totality: total
Visibility: public export
Constructor: 

MkPara : (Param : (m .mapObj a) .Obj) -> c .Hom ((depAct .Act a) .mapObj Param) b -> DepParaMor depAct a b

Projections:

.Param : DepParaMor depAct a b -> (m .mapObj a) .Obj

.Run : ({rec:0} : DepParaMor depAct a b) -> c .Hom ((depAct .Act a) .mapObj (Param {rec:0})) b

.Param : DepParaMor depAct a b -> (m .mapObj a) .Obj

Visibility: public export

Param : DepParaMor depAct a b -> (m .mapObj a) .Obj

Visibility: public export

.Run : ({rec:0} : DepParaMor depAct a b) -> c .Hom ((depAct .Act a) .mapObj (Param {rec:0})) b

Visibility: public export

Run : ({rec:0} : DepParaMor depAct a b) -> c .Hom ((depAct .Act a) .mapObj (Param {rec:0})) b

Visibility: public export

DepParaCat : DepAct c m -> Cat

Visibility: public export

composeParaNotUsed : DepParaMor depAct x y -> DepParaMor depAct y z -> DepParaMor depAct x z

  We do not define composition or anything else here. This is because, if we
  did, we'd have to define a lot of other things, like composition in the 
  base category, and associators of the monoidal category and actegory
  While the type below would be "simple", its full abstract implementation is 
  not necessary for us