
  0 | module Data.CT.Category.Instances
  1 | 
  2 | import Data.CT.Category.Definition
  3 | import Data.CT.Functor.Definition
  4 | 
  5 | import Data.ComMonoid
  6 | import Data.Container.Base
  7 | import Data.Container.Additive
  8 | 
  9 | public export
 10 | TypeCat : Cat
 11 | TypeCat = MkCat Type (\a, b => a -> b)
 12 | 
 13 | public export
 14 | Cat : Cat
 15 | Cat = MkCat Cat Functor
 16 | 
 17 | public export
 18 | opCat : Cat -> Cat
 19 | opCat c = MkCat c.Obj (flip c.Hom)
 20 | 
 21 | public export
 22 | DLens : Cat
 23 | DLens = MkCat Cont (=%>)
 24 | 
 25 | public export
 26 | DChart : Cat
 27 | DChart = MkCat Cont (=&>)
 28 | 
 29 | ||| Category of additive dependent lenses
 30 | public export
 31 | AddDLens : Cat
 32 | AddDLens = MkCat AddCont (=%+>)
 33 | 
 34 | ||| Category of additive dependent charts
 35 | public export
 36 | AddDChart : Cat
 37 | AddDChart = MkCat AddCont (=&+>)
 38 | 
 39 | ||| Category of commutative monoids and commutative monoid homomorphisms
 40 | public export
 41 | ComMon : Cat
 42 | ComMon = MkCat ComMonoid ComMonoidHomo
 43 |