
  0 | module Data.Bicontravariant
  1 | 
  2 | import Data.Morphisms
  3 | import Data.Contravariant
  4 | import Data.Profunctor
  5 | 
  6 | %default total
  7 | 
  8 | 
  9 | public export
 10 | interface Bicontravariant f where
 11 |   contrabimap : (a -> b) -> (c -> d) -> f b d -> f a c
 12 |   contrabimap f g = contramapFst f . contramapSnd g
 13 | 
 14 |   contramapFst : (a -> b) -> f b c -> f a c
 15 |   contramapFst f = contrabimap f id
 16 | 
 17 |   contramapSnd : (b -> c) -> f a c -> f a b
 18 |   contramapSnd = contrabimap id
 19 | 
 20 | 
 21 | public export
 22 | Contravariant f => Bicontravariant (Star f) where
 23 |   contrabimap f g = MkStar . dimap @{Function} f (contramap g) . applyStar
 24 | 
 25 | public export
 26 | Contravariant f => Bicontravariant (Kleislimorphism f) where
 27 |   contrabimap f g = Kleisli . dimap @{Function} f (contramap g) . applyKleisli
 28 | 
 29 | public export
 30 | Bicontravariant (Forget {k=Type} r) where
 31 |   contrabimap f _ = MkForget . lmap @{Function} f . runForget
 32 | 
 33 | 
 34 | public export
 35 | rphantom : (Profunctor p, Bicontravariant p) => p a b -> p a c
 36 | rphantom = contramapSnd (const ()) . rmap (const ())
 37 | 
 38 | public export
 39 | biphantom : (Bifunctor p, Bicontravariant p) => p a b -> p c d
 40 | biphantom = contrabimap (const ()) (const ()) . bimap (const ()) (const ())
 41 |