
  0 | module Control.DistributiveB
  1 | 
  2 | import Control.FunctorB
  3 | 
  4 | %default total
  5 | 
  6 | public export
  7 | interface FunctorB k t => DistributiveB k t | t where
  8 |   constructor MkDistributiveB
  9 |   bdistribute : {0 g : k -> Type} -> Functor f => f (t g) -> t (f . g)
 10 |