>>11259866https://voca.ro/7GQkvxapVHfFix a functor F and an object A.
u will denote a term parameter of type FA.
f will denote a map of type A->X.
g will denote a map of type X->A.
n will will denote a map of type (A->X) -> FX that works for any type X.
I.e. n is actually a family of maps, one for each X, and we're mostly going to make use of the case X=A.
b : FA -> forall X. ((A->X) -> FX)
b(u) := f F(f)(u)
b(u) is of type of n.
c : forall X. ((A->X) -> FX) -> FA
c(n) = n(id_A)
c(n) is of type of u.
c(b(u)) = F(id_A)(u) = u
The map b ties u's to n's and the n's remember their u's (recovered via c).
b(c(n)) = f F(f)(n(id_A))
Any choice of n(id_A) (some element of FA) induces a map from f's.
For f = id_A, you get
b(c(n))(id_A) = n(id_A)
The naturality condition (pic related)
https://en.wikipedia.org/wiki/Yoneda_lemma#Proofon n says that it must act as above not just for id_A, but for any f.
The choices of u==n(id_A) then correspond with the possible n's.
So
forall X. ((A->X) -> FX) = FA
or
((A->-) -> F-) = FA
or
hom(hom(A, -), F) = FA
You have some similar results for
hom(hom(-, A), F) = FA
E.g. the right homset dominates FA via
d : forall X. ((X->A) -> FX) -> FA
d(n) := n(id_A)
For
>hom(hom(-,A), F) = FAin the case of sets/types with FX = X->B you even get the direction
e : A->B -> forall X. ((X->A) -> (X->B))
e(h) := g (h g)
Back to the general case, this says
>hom(hom(-,A), hom(-,B)) = hom(A,B)where on the left hand side you have the arrows of functors (natural transformations) and on the left hand side the arrows hom(A, B).
If you believe my motivation that the above "=" is indeed a bijection, then this means that the object "A" and "B" and their arrows "hom(A, B)" also exist in the (generally bigger) set valued functor category where those two objects are mirrored by "hom(-, A)" and "hom(-, B)" (and the arrows are in bijection, i.e. the same as before)
