Last active
February 4, 2025 04:00
-
-
Save LSLeary/29475c86eec908dc24ede0171fa36d37 to your computer and use it in GitHub Desktop.
A more general treatment of the Yoneda lemma than is given in Data.Functor.Yoneda.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE GHC2021, BlockArguments #-} | |
module Yoneda where | |
import Prelude hiding (id, (.), map) | |
import Control.Category | |
-- Preliminaries | |
class (Category c, Category d) => ExoFunctor c d f where | |
map :: a `c` b -> f a `d` f b | |
type f ~> g = forall x. f x -> g x | |
type c ~~> d = forall x y. c x y -> d x y | |
-- Covariant lemma | |
newtype Yoneda c f a = Yoneda{ unYoneda :: c a ~> f } | |
instance Category c => ExoFunctor c (->) (Yoneda c f) where | |
map f = \y -> Yoneda \g -> unYoneda y (g . f) | |
toYoneda :: ExoFunctor c (->) f => f ~> Yoneda c f | |
toYoneda x = Yoneda (`map` x) | |
fromYoneda :: Category c => Yoneda c f ~> f | |
fromYoneda y = unYoneda y id | |
-- Covariant embedding | |
newtype Embed c a b = Embed{ unEmbed :: c b ~> c a } | |
instance Category (Embed c) where | |
id = Embed id | |
Embed f . Embed g = Embed (g . f) | |
embed :: Category c => c ~~> Embed c | |
embed c = Embed (. c) | |
debed :: Category c => Embed c ~~> c | |
debed e = unEmbed e id |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment