
  0 | module Control.FunctorB
  1 | 
  2 | %default total
  3 | 
  4 | public export
  5 | 0 I : Type -> Type
  6 | I a = a
  7 | 
  8 | public export
  9 | 0 K : Type -> Type -> Type
 10 | K e a = e
 11 | 
 12 | public export
 13 | interface FunctorB (0 k : Type) (0 t : (k -> Type) -> Type) | t where
 14 |   constructor MkFunctorB
 15 |   bmap_ : {0 f,g : k -> Type} -> ((0 a : k) -> f a -> g a) -> t f -> t g
 16 | 
 17 | public export
 18 | bmap : FunctorB k t => ({0 a : k} -> f a -> g a) -> t f -> t g
 19 | bmap f = bmap_ (\_ => f)
 20 |