Portability | GADTs, TFs, MPTCs |
---|---|
Stability | provisional |
Maintainer | Edward Kmett <ekmett@gmail.com> |
Safe Haskell | Trustworthy |
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
A Contravariant
functor (aka presheaf) suitable for Yoneda reduction.
Contravariant (Coyoneda f) | |
Representable f => Representable (Coyoneda f) | |
Adjunction f g => Adjunction (Coyoneda f) (Coyoneda g) |
liftCoyoneda :: f a -> Coyoneda f aSource
Coyoneda expansion of a presheaf
liftCoyoneda
.lowerCoyoneda
≡id
lowerCoyoneda
.liftCoyoneda
≡id
lowerCoyoneda :: Contravariant f => Coyoneda f a -> f aSource
Coyoneda reduction on a presheaf