
  0 | module Data.CT.DependentAction.Instances
  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 | import Data.Container.Base
  9 | import Data.Container.Additive
 10 | 
 11 | namespace Type
 12 |   public export
 13 |   PairType : DepAct TypeCat (Const {c=TypeCat})
 14 |   PairType = MkDepAct $ \x => MkFunctor
 15 |     (x,)
 16 |     (\r, (x, p) => (x, r p))
 17 |   
 18 |   
 19 |   ||| X, X':X -> Set, DPair X X'
 20 |   public export
 21 |   DPairType : DepAct TypeCat (FamIndCat {c=TypeCat})
 22 |   DPairType = MkDepAct $ \x => MkFunctor
 23 |     (DPair x)
 24 |     (\r, (x ** p) => (x ** r x p))
 25 | 
 26 | namespace Cont
 27 |   public export
 28 |   PairCont : DepAct DLens (Const {c=DLens})
 29 |   PairCont = MkDepAct $ \c => MkFunctor
 30 |     (c ><)
 31 |     (Morphism.(><) id)
 32 | 
 33 |   public export
 34 |   DPairCont : DepAct DLens (FamDLens {c=DLens})
 35 |   DPairCont = MkDepAct $ \c => MkFunctor
 36 |     (DepHancockProduct c)
 37 |     (\r => !% \(x ** p) => ((x ** (r x).fwd p) **
 38 |               \(x', p') => (x', (r x).bwd p p')))
 39 | 
 40 | 
 41 | namespace AddCont
 42 |   public export
 43 |   PairAddCont : DepAct AddDLens (Const {c=AddDLens})
 44 |   PairAddCont = MkDepAct $ \c => MkFunctor
 45 |     (c ><)
 46 |     (id ><)
 47 | 
 48 |   public export
 49 |   DPairAddCont : DepAct AddDLens (FamAddDLens {c=AddDLens})
 50 |   DPairAddCont = MkDepAct $ \c => MkFunctor
 51 |     (DepHancockProduct c)
 52 |     (\r => !%+ \(x ** p) => ((x ** (r x).fwd p) **
 53 |                \(x', p') => (x', (r x).bwd p p')))