{-# LANGUAGE TypeOperators, RankNTypes, TypeFamilies, PatternSynonyms, UndecidableInstances, NoImplicitPrelude #-}
module Data.Category.Yoneda where
import Data.Category
import Data.Category.Functor
import Data.Category.NaturalTransformation
import Data.Category.Adjunction
type YonedaEmbedding k =
Postcompose (Hom k) (Op k) :.:
(Postcompose (Swap k (Op k)) (Op k) :.: Tuple k (Op k))
pattern YonedaEmbedding :: Category k => YonedaEmbedding k
pattern $bYonedaEmbedding :: YonedaEmbedding k
$mYonedaEmbedding :: forall r (k :: * -> * -> *).
Category k =>
YonedaEmbedding k -> (Void# -> r) -> (Void# -> r) -> r
YonedaEmbedding = Postcompose Hom :.: (Postcompose Swap :.: Tuple)
data Yoneda (k :: * -> * -> *) f = Yoneda
instance (Category k, Functor f, Dom f ~ Op k, Cod f ~ (->)) => Functor (Yoneda k f) where
type Dom (Yoneda k f) = Op k
type Cod (Yoneda k f) = (->)
type Yoneda k f :% a = Nat (Op k) (->) (k :-*: a) f
Yoneda k f
Yoneda % :: Yoneda k f
-> Dom (Yoneda k f) a b
-> Cod (Yoneda k f) (Yoneda k f :% a) (Yoneda k f :% b)
% Op ab = \Nat (Op k) (->) (k :-*: a) f
n -> Nat (Op k) (->) (k :-*: a) f
n Nat (Op k) (->) (k :-*: a) f
-> Nat (Op k) (->) (k :-*: b) (k :-*: a)
-> Nat (Op k) (->) (k :-*: b) f
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. (FunctorCompose (Op k) (Op k :**: k) (->)
:.: ((Const
(Nat (Op k) (Op k :**: k)) (Nat (Op k :**: k) (->)) (Hom k)
:***: Id (Nat (Op k) (Op k :**: k)))
:.: DiagProd (Nat (Op k) (Op k :**: k))))
:.: ((FunctorCompose (Op k) (k :**: Op k) (Op k :**: k)
:.: ((Const
(Nat (Op k) (k :**: Op k))
(Nat (k :**: Op k) (Op k :**: k))
((Proj2 k (Op k) :***: Proj1 k (Op k)) :.: DiagProd (k :**: Op k))
:***: Id (Nat (Op k) (k :**: Op k)))
:.: DiagProd (Nat (Op k) (k :**: Op k))))
:.: Tuple k (Op k))
forall (k :: * -> * -> *). Category k => YonedaEmbedding k
YonedaEmbedding ((FunctorCompose (Op k) (Op k :**: k) (->)
:.: ((Const
(Nat (Op k) (Op k :**: k)) (Nat (Op k :**: k) (->)) (Hom k)
:***: Id (Nat (Op k) (Op k :**: k)))
:.: DiagProd (Nat (Op k) (Op k :**: k))))
:.: ((FunctorCompose (Op k) (k :**: Op k) (Op k :**: k)
:.: ((Const
(Nat (Op k) (k :**: Op k))
(Nat (k :**: Op k) (Op k :**: k))
((Proj2 k (Op k) :***: Proj1 k (Op k)) :.: DiagProd (k :**: Op k))
:***: Id (Nat (Op k) (k :**: Op k)))
:.: DiagProd (Nat (Op k) (k :**: Op k))))
:.: Tuple k (Op k)))
-> Dom
((FunctorCompose (Op k) (Op k :**: k) (->)
:.: ((Const
(Nat (Op k) (Op k :**: k)) (Nat (Op k :**: k) (->)) (Hom k)
:***: Id (Nat (Op k) (Op k :**: k)))
:.: DiagProd (Nat (Op k) (Op k :**: k))))
:.: ((FunctorCompose (Op k) (k :**: Op k) (Op k :**: k)
:.: ((Const
(Nat (Op k) (k :**: Op k))
(Nat (k :**: Op k) (Op k :**: k))
((Proj2 k (Op k) :***: Proj1 k (Op k)) :.: DiagProd (k :**: Op k))
:***: Id (Nat (Op k) (k :**: Op k)))
:.: DiagProd (Nat (Op k) (k :**: Op k))))
:.: Tuple k (Op k)))
b
a
-> Cod
((FunctorCompose (Op k) (Op k :**: k) (->)
:.: ((Const
(Nat (Op k) (Op k :**: k)) (Nat (Op k :**: k) (->)) (Hom k)
:***: Id (Nat (Op k) (Op k :**: k)))
:.: DiagProd (Nat (Op k) (Op k :**: k))))
:.: ((FunctorCompose (Op k) (k :**: Op k) (Op k :**: k)
:.: ((Const
(Nat (Op k) (k :**: Op k))
(Nat (k :**: Op k) (Op k :**: k))
((Proj2 k (Op k) :***: Proj1 k (Op k)) :.: DiagProd (k :**: Op k))
:***: Id (Nat (Op k) (k :**: Op k)))
:.: DiagProd (Nat (Op k) (k :**: Op k))))
:.: Tuple k (Op k)))
(((FunctorCompose (Op k) (Op k :**: k) (->)
:.: ((Const
(Nat (Op k) (Op k :**: k)) (Nat (Op k :**: k) (->)) (Hom k)
:***: Id (Nat (Op k) (Op k :**: k)))
:.: DiagProd (Nat (Op k) (Op k :**: k))))
:.: ((FunctorCompose (Op k) (k :**: Op k) (Op k :**: k)
:.: ((Const
(Nat (Op k) (k :**: Op k))
(Nat (k :**: Op k) (Op k :**: k))
((Proj2 k (Op k) :***: Proj1 k (Op k)) :.: DiagProd (k :**: Op k))
:***: Id (Nat (Op k) (k :**: Op k)))
:.: DiagProd (Nat (Op k) (k :**: Op k))))
:.: Tuple k (Op k)))
:% b)
(((FunctorCompose (Op k) (Op k :**: k) (->)
:.: ((Const
(Nat (Op k) (Op k :**: k)) (Nat (Op k :**: k) (->)) (Hom k)
:***: Id (Nat (Op k) (Op k :**: k)))
:.: DiagProd (Nat (Op k) (Op k :**: k))))
:.: ((FunctorCompose (Op k) (k :**: Op k) (Op k :**: k)
:.: ((Const
(Nat (Op k) (k :**: Op k))
(Nat (k :**: Op k) (Op k :**: k))
((Proj2 k (Op k) :***: Proj1 k (Op k)) :.: DiagProd (k :**: Op k))
:***: Id (Nat (Op k) (k :**: Op k)))
:.: DiagProd (Nat (Op k) (k :**: Op k))))
:.: Tuple k (Op k)))
:% a)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% k b a
Dom
((FunctorCompose (Op k) (Op k :**: k) (->)
:.: ((Const
(Nat (Op k) (Op k :**: k)) (Nat (Op k :**: k) (->)) (Hom k)
:***: Id (Nat (Op k) (Op k :**: k)))
:.: DiagProd (Nat (Op k) (Op k :**: k))))
:.: ((FunctorCompose (Op k) (k :**: Op k) (Op k :**: k)
:.: ((Const
(Nat (Op k) (k :**: Op k))
(Nat (k :**: Op k) (Op k :**: k))
((Proj2 k (Op k) :***: Proj1 k (Op k)) :.: DiagProd (k :**: Op k))
:***: Id (Nat (Op k) (k :**: Op k)))
:.: DiagProd (Nat (Op k) (k :**: Op k))))
:.: Tuple k (Op k)))
b
a
ab
fromYoneda :: (Category k, Functor f, Dom f ~ Op k, Cod f ~ (->)) => f -> Nat (Op k) (->) (Yoneda k f) f
fromYoneda :: f -> Nat (Op k) (->) (Yoneda k f) f
fromYoneda f
f = Yoneda k f
-> f
-> (forall z. Obj (Op k) z -> Component (Yoneda k f) f z)
-> Nat (Op k) (->) (Yoneda k f) f
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat Yoneda k f
forall (k :: * -> * -> *) f. Yoneda k f
Yoneda f
f (\(Op a) Nat (Op k) (->) (k :-*: z) f
n -> (Nat (Op k) (->) (k :-*: z) f
n Nat (Op k) (->) (k :-*: z) f
-> Obj (Op k) z -> ((k :-*: z) :% z) -> f :% z
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! k z z -> Obj (Op k) z
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op k z z
a) k z z
a)
toYoneda :: (Category k, Functor f, Dom f ~ Op k, Cod f ~ (->)) => f -> Nat (Op k) (->) f (Yoneda k f)
toYoneda :: f -> Nat (Op k) (->) f (Yoneda k f)
toYoneda f
f = f
-> Yoneda k f
-> (forall z. Obj (Op k) z -> Component f (Yoneda k f) z)
-> Nat (Op k) (->) f (Yoneda k f)
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat f
f Yoneda k f
forall (k :: * -> * -> *) f. Yoneda k f
Yoneda (\(Op a) f :% z
fa -> (k :-*: z)
-> f
-> (forall z. Obj (Op k) z -> Component (k :-*: z) f z)
-> Nat (Op k) (->) (k :-*: z) f
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (Obj k z -> k :-*: z
forall (k :: * -> * -> *) x. Category k => Obj k x -> k :-*: x
Hom_X Obj k z
a) f
f (\Obj (Op k) z
_ k z z
h -> (f
f f -> Dom f z z -> Cod f (f :% z) (f :% z)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% k z z -> Op k z z
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op k z z
h) f :% z
fa))
haskUnit :: Obj (->) ()
haskUnit :: Obj (->) ()
haskUnit () = ()
data M1 = M1
instance Functor M1 where
type Dom M1 = Nat (Op (->)) (->)
type Cod M1 = (->)
type M1 :% f = f :% ()
M1
M1 % :: M1 -> Dom M1 a b -> Cod M1 (M1 :% a) (M1 :% b)
% Dom M1 a b
n = Dom M1 a b
Nat (Op (->)) (->) a b
n Nat (Op (->)) (->) a b -> Op (->) () () -> (a :% ()) -> b :% ()
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! Obj (->) () -> Op (->) () ()
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op Obj (->) ()
haskUnit
haskIsTotal :: Adjunction (->) (Nat (Op (->)) (->)) M1 (YonedaEmbedding (->))
haskIsTotal :: Adjunction (->) (Nat (Op (->)) (->)) M1 (YonedaEmbedding (->))
haskIsTotal = M1
-> ((FunctorCompose (Op (->)) (Op (->) :**: (->)) (->)
:.: Tuple1
(Nat (Op (->) :**: (->)) (->))
(Nat (Op (->)) (Op (->) :**: (->)))
(Hom (->)))
:.: ((FunctorCompose
(Op (->)) ((->) :**: Op (->)) (Op (->) :**: (->))
:.: Tuple1
(Nat ((->) :**: Op (->)) (Op (->) :**: (->)))
(Nat (Op (->)) ((->) :**: Op (->)))
(Swap (->) (Op (->))))
:.: Tuple (->) (Op (->))))
-> (forall a.
Obj (Nat (Op (->)) (->)) a
-> Component
(Id (Nat (Op (->)) (->)))
(((FunctorCompose (Op (->)) (Op (->) :**: (->)) (->)
:.: Tuple1
(Nat (Op (->) :**: (->)) (->))
(Nat (Op (->)) (Op (->) :**: (->)))
(Hom (->)))
:.: ((FunctorCompose
(Op (->)) ((->) :**: Op (->)) (Op (->) :**: (->))
:.: Tuple1
(Nat ((->) :**: Op (->)) (Op (->) :**: (->)))
(Nat (Op (->)) ((->) :**: Op (->)))
(Swap (->) (Op (->))))
:.: Tuple (->) (Op (->))))
:.: M1)
a)
-> (forall a b.
Obj (->) b
-> Nat
(Op (->))
(->)
a
(((FunctorCompose (Op (->)) (Op (->) :**: (->)) (->)
:.: Tuple1
(Nat (Op (->) :**: (->)) (->))
(Nat (Op (->)) (Op (->) :**: (->)))
(Hom (->)))
:.: ((FunctorCompose
(Op (->)) ((->) :**: Op (->)) (Op (->) :**: (->))
:.: Tuple1
(Nat ((->) :**: Op (->)) (Op (->) :**: (->)))
(Nat (Op (->)) ((->) :**: Op (->)))
(Swap (->) (Op (->))))
:.: Tuple (->) (Op (->))))
:% b)
-> (M1 :% a)
-> b)
-> Adjunction
(->)
(Nat (Op (->)) (->))
M1
((FunctorCompose (Op (->)) (Op (->) :**: (->)) (->)
:.: Tuple1
(Nat (Op (->) :**: (->)) (->))
(Nat (Op (->)) (Op (->) :**: (->)))
(Hom (->)))
:.: ((FunctorCompose
(Op (->)) ((->) :**: Op (->)) (Op (->) :**: (->))
:.: Tuple1
(Nat ((->) :**: Op (->)) (Op (->) :**: (->)))
(Nat (Op (->)) ((->) :**: Op (->)))
(Swap (->) (Op (->))))
:.: Tuple (->) (Op (->))))
forall f g (d :: * -> * -> *) (c :: * -> * -> *).
(Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c,
Cod g ~ d) =>
f
-> g
-> (forall a. Obj d a -> Component (Id d) (g :.: f) a)
-> (forall a b. Obj c b -> d a (g :% b) -> c (f :% a) b)
-> Adjunction c d f g
mkAdjunctionUnit M1
M1 (FunctorCompose (Op (->)) (Op (->) :**: (->)) (->)
:.: Tuple1
(Nat (Op (->) :**: (->)) (->))
(Nat (Op (->)) (Op (->) :**: (->)))
(Hom (->)))
:.: ((FunctorCompose
(Op (->)) ((->) :**: Op (->)) (Op (->) :**: (->))
:.: Tuple1
(Nat ((->) :**: Op (->)) (Op (->) :**: (->)))
(Nat (Op (->)) ((->) :**: Op (->)))
(Swap (->) (Op (->))))
:.: Tuple (->) (Op (->)))
forall (k :: * -> * -> *). Category k => YonedaEmbedding k
YonedaEmbedding
(\(Nat f _ _) -> a
-> ((->) :-*: (a :% ()))
-> (forall z.
Obj (Op (->)) z -> Component a ((->) :-*: (a :% ())) z)
-> Nat (Op (->)) (->) a ((->) :-*: (a :% ()))
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat a
f (Obj (->) (a :% ()) -> (->) :-*: (a :% ())
forall (k :: * -> * -> *) x. Category k => Obj k x -> k :-*: x
Hom_X (a
f a -> Dom a () () -> Cod a (a :% ()) (a :% ())
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj (->) () -> Op (->) () ()
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op Obj (->) ()
haskUnit)) (\Obj (Op (->)) z
_ a :% z
fz z
z -> (a
f a -> Dom a z () -> Cod a (a :% z) (a :% ())
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% (() -> z) -> Op (->) z ()
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op (\() -> z
z)) a :% z
fz))
(\Obj (->) b
_ n :: Nat
(Op (->))
(->)
a
(((FunctorCompose (Op (->)) (Op (->) :**: (->)) (->)
:.: Tuple1
(Nat (Op (->) :**: (->)) (->))
(Nat (Op (->)) (Op (->) :**: (->)))
(Hom (->)))
:.: ((FunctorCompose
(Op (->)) ((->) :**: Op (->)) (Op (->) :**: (->))
:.: Tuple1
(Nat ((->) :**: Op (->)) (Op (->) :**: (->)))
(Nat (Op (->)) ((->) :**: Op (->)))
(Swap (->) (Op (->))))
:.: Tuple (->) (Op (->))))
:% b)
n@(Nat f _ _) a :% ()
fu -> (Nat
(Op (->))
(->)
a
(Hom (->)
:.: (Swap (->) (Op (->))
:.: ((Const (Op (->)) (->) b :***: Id (Op (->)))
:.: DiagProd (Op (->)))))
Nat
(Op (->))
(->)
a
(((FunctorCompose (Op (->)) (Op (->) :**: (->)) (->)
:.: Tuple1
(Nat (Op (->) :**: (->)) (->))
(Nat (Op (->)) (Op (->) :**: (->)))
(Hom (->)))
:.: ((FunctorCompose
(Op (->)) ((->) :**: Op (->)) (Op (->) :**: (->))
:.: Tuple1
(Nat ((->) :**: Op (->)) (Op (->) :**: (->)))
(Nat (Op (->)) ((->) :**: Op (->)))
(Swap (->) (Op (->))))
:.: Tuple (->) (Op (->))))
:% b)
n Nat
(Op (->))
(->)
a
(Hom (->)
:.: (Swap (->) (Op (->))
:.: ((Const (Op (->)) (->) b :***: Id (Op (->)))
:.: DiagProd (Op (->)))))
-> Op (->) () ()
-> (a :% ())
-> (Hom (->)
:.: (Swap (->) (Op (->))
:.: ((Const (Op (->)) (->) b :***: Id (Op (->)))
:.: DiagProd (Op (->)))))
:% ()
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! Obj (->) () -> Op (->) () ()
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op Obj (->) ()
haskUnit) a :% ()
fu ())