Let Hask be Set

gistfile1.txt

http://comonad.com/reader/2008/representing-adjunctions/


Let Hask be Set?
SET:
Objects are sets
Morphisms are total functions between sets
(wait, Hom-Sets are exponentials?????)

HASK:
Objects are types
Morphisms are function terms between sets

HASK as SET:
If we take Hom-sets as exponentials, then we can think of HOM(A, B) as just the type A -> B

COVARIANT Representable Functor
so Hom(A -> _) can be viewed as A -> _
i.e. reader monad

CONTRAVARIANT Representable Functor
so Hom(_ -> B) can be viewed as _ -> B
i.e. ???


Covariant Yoneda Lemma:

In category theory: [C, Set](C(a, -), F) = F a

forall b (a -> b) -> F b

natural transformation from covariant representable functor of a to a functor F : C -> Set
isomorphic to F a


Covariant Yoneda corollary:

In category Theory: [C, Set](C(a, -), C(b, -)) = C (b, a)
ie. Hom(h^a, h^b) = Hom (b, a)

forall b (a -> b) -> (a' -> b) = a' -> a
(CONTRAPOSITIVE!!!!!!!)

Reader monad captures the essence of a covariant representable functor
Natural transformations from reader monads are isomorphic to oppositely directed morphisms (read functions) from their representing types.






Contravariant Yoneda corollary:


In category Theory: [C, Set](C(-, a), C(-, b)) = C (a, b)
ie. Hom(h_a, h_b) = Hom (a, b)


forall b (b -> a) -> (b -> a') = a -> a'

If I can always get (b -> a') from (b -> a), then I can always get a' from a.




So Continuations.
forall b. (a -> b) -> Id b = Id a
forall b. (a -> b) -> b = a

The natural transformations from representable functor on a to the identity functor
are isomorphic the the identity functor on a



covariant representable functors are just reader monads




State monad.

forall a. s -> (s, a)


What the hell is this?
Covariant yoneda lemma applied on writer comonad
forall b. (a -> b) -> (c, b) = (c, a)
forall b. (a -> b) -> (a, b) = (a, a)


Covariant yoneda lemma applied on itself

forall b. (a -> b) -> (a -> b) = (a -> a)


Covariant yoneda applied on maybe

forall b. (a -> b) -> maybe b = maybe a