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