0 | module Data.CT.DependentPara.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 | import Data.CT.DependentAction.Definition
 7 | import Data.CT.DependentAction.Instances
 8 |
 9 | ||| Data structure holding the morphisms of dependent para
10 | public export
11 | record DepParaMor
12 |   {c : Cat}
13 |   {m : IndCat c}
14 |   (depAct : DepAct c m)
15 |   (a, b : c.Obj)
16 |   where
17 |   constructor MkPara
18 |   Param : (m.mapObj a).Obj
19 |   Run : c.Hom ((depAct.Act a).mapObj Param) b
20 |
21 | public export
22 | DepParaCat : {c : Cat} -> {m : IndCat c} ->
23 |   (depAct : DepAct c m) ->
24 |   Cat
25 | DepParaCat depAct = MkCat c.Obj (DepParaMor depAct)
26 |
27 | ||| We do not define composition or anything else here. This is because, if we
28 | ||| did, we'd have to define a lot of other things, like composition in the 
29 | ||| base category, and associators of the monoidal category and actegory
30 | ||| While the type below would be "simple", its full abstract implementation is 
31 | ||| not necessary for us
32 | public export
33 | composeParaNotUsed : {c : Cat} -> {m : IndCat c} ->
34 |   {depAct : DepAct c m} ->
35 |   {x, y, z : c.Obj} ->
36 |   DepParaMor {c=c} {m=m} depAct x y ->
37 |   DepParaMor {c=c} {m=m} depAct y z ->
38 |   DepParaMor {c=c} {m=m} depAct x z