| Copyright | (C) 2013-2016 Edward Kmett |
|---|---|
| License | BSD-style (see the file LICENSE) |
| Maintainer | Edward Kmett <ekmett@gmail.com> |
| Stability | provisional |
| Portability | GADTs, TFs, MPTCs |
| Safe Haskell | Trustworthy |
| Language | Haskell98 |
Data.Functor.Contravariant.Coyoneda
Description
The co-Yoneda lemma for presheafs states that f is naturally isomorphic to .Coyoneda f
- data Coyoneda f a where
- liftCoyoneda :: f a -> Coyoneda f a
- lowerCoyoneda :: Contravariant f => Coyoneda f a -> f a
Documentation
data Coyoneda f a where Source #
A Contravariant functor (aka presheaf) suitable for Yoneda reduction.
Instances
| Contravariant (Coyoneda f) Source # | |
| Representable f => Representable (Coyoneda f) Source # | |
| Adjunction f g => Adjunction (Coyoneda f) (Coyoneda g) Source # | |
| type Rep (Coyoneda f) Source # | |
liftCoyoneda :: f a -> Coyoneda f a Source #
Coyoneda "expansion" of a presheaf
liftCoyoneda.lowerCoyoneda≡idlowerCoyoneda.liftCoyoneda≡id
lowerCoyoneda :: Contravariant f => Coyoneda f a -> f a Source #
Coyoneda reduction on a presheaf