Skip to content

Instantly share code, notes, and snippets.

@LSLeary
Last active February 4, 2025 04:00
Show Gist options
  • Save LSLeary/29475c86eec908dc24ede0171fa36d37 to your computer and use it in GitHub Desktop.
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.
{-# 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