Universal properties of universal and existential quantification In the paper What You Needa Know about Yoneda, Boisseau and Gibbons appeal to the universal properties of universal and existential quantification in order to derive the "co-Yoneda" data type:
$$
\begin{align*}
& \forall a \,.\, f\,a \to (\forall r \,.\, (a \to r) \to g\,r) \\
\cong & \; \{ \, \text{universal property of universal quantification} \, \} \\
& \forall a \,.\, \forall r \,.\, f\,a \to (a \to r) \to g\,r \\
\cong &\; \{\,\text{uncurrying}\,\} \\
& \forall a \,.\, \forall r \,.\, (f\,a \times (a \to r)) \to g\,r \\
\cong &\; \{\,\text{swapping the two quantifiers}\,\} \\
& \forall r \,.\, \forall a \,.\, (f\,a \times (a \to r)) \to g\,r \\
\cong &\; \{\,\text{universal property of existential quantification}\,\} \\
& \forall r \,.\, (\exists a \,.\, (f\,a \times (a \to r))) \to g\,r \\
\end{align*}
$$
What exactly are these universal properties and how are they related to category theory? In particular, in which category is the above derivation carried?
 A: It's probably worth looking at what these formulas look like in general category theory. These use the very useful but under-discussed concept of (co)ends.
First, we have the naturality formula which states that $\mathsf{Nat}(F,G)\cong\int_{C:\mathcal C}\mathcal{D}(FC,GC)$ where $F, G : \mathcal C\to\mathcal{D}$ are functors and $\mathsf{Nat}(F,G)$ is the set of natural transformations from $F$ to $G$. (In enriched contexts, this formula is taken as the definition of the object of natural transformations.)
The Yoneda lemma (for covariant functors) is then $\int_{R:\mathcal C}\mathbf{Set}(\mathcal{C}(A,R),GR)\cong GA$ where $G:\mathcal C\to\mathbf{Set}$.
Because (co)ends can be expressed as (co)limits, they have the following universal property (which could also be taken axiomatically): $$\mathcal D\left(-,\int_{C:\mathcal C}P(C,C)\right)\cong\int_{C:\mathcal C}\mathcal D(-,P(C,C)) \\ \mathcal D\left(\int^{C:\mathcal C}P(C,C),-\right)\cong\int_{C:\mathcal{C}}\mathcal D(P(C,C),-)$$ where $P : \mathcal C^{op}\times C\to \mathcal D$. This reduces ends and coends in $\mathcal D$ to ends in presheaves on $\mathcal D$ which are evaluated pointwise and so reduce to ends in $\mathbf{Set}$. These are essentially the universal properties being referenced in the form of representability. Let us prove the theorem you reference in full categorical generality. (Actually, we can generalize a bit further than this.)
$$\begin{align}
&\ \mathsf{Nat}(F,G) &\\
\cong & \int_{A:\mathcal C}\mathbf{Set}(FA,GA) & \{\textrm{naturality formula}\} \\
\cong & \int_{A:\mathcal C}\mathbf{Set}\left(FA,\int_{R:\mathcal C}\mathbf{Set}(\mathcal C(A,R), GR)\right) & \{\textrm{Yoneda lemma}\} \\
\cong & \int_{A:\mathcal C}\int_{R:\mathcal C}\mathbf{Set}(FA,\mathbf{Set}(\mathcal C(A,R), GR)) & \{\textrm{end universal property}\} \\
\cong & \int_{A:\mathcal C}\int_{R:\mathcal C}\mathbf{Set}(FA\times\mathcal C(A,R), GR)) & \{\textrm{uncurry}\}  \\
\cong & \int_{R:\mathcal C}\int_{A:\mathcal C}\mathbf{Set}(FA\times\mathcal C(A,R), GR)) & \{\textrm{Fubini theorem}\}  \\
\cong & \int_{R:\mathcal C}\mathbf{Set}\left(\int^{A:\mathcal C}FA\times\mathcal C(A,R), GR\right) & \{\textrm{coend universal property}\}  \\
\cong &\ \mathsf{Nat}\left(\int^{A:\mathcal C}FA\times\mathcal C(A,-), G\right) & \{\textrm{naturality formula}\} 
\end{align}$$
Given that this is natural in $G$, then this implies that $F\cong \int^{A:\mathcal C}FA\times\mathcal{C}(A,-)$ which is the co-Yoneda lemma (for covariant functors).
Now, in the context of Haskell programming, the "functors" would be $\mathbf{Hask}\to\mathbf{Hask}$ where $\mathbf{Hask}$ is often analogized to $\mathbf{Set}$. Doing the above with $\mathcal{C}=\mathbf{Set}$ leads to a variety of size issues, e.g. a category being (co)complete, as $\mathbf{Set}$ is, means that it has all (co)limits indexed by small categories, but $\mathbf{Set}$ is not small so it is not clear whether the (co)ends used above would exist. Nevertheless, the intuition used by people like Ed Kmett and Bartosz Milewski is that these $\mathbf{Set}$-/$\mathbf{Hask}$-indexed ends/coends behave like universal/existential quantifiers. Parametricity is likely what enables this to actually work out. We cannot write down "functors" in Haskell that arbitrarily map types to other types. There is a lot more flexibility for functors $\mathbf{Set}\to\mathbf{Set}$. The precise connection between all of these is still somewhat hazy (at least to me).
(I should add that you can talk about universal properties for universal/existential quantifiers but that requires a bit more machinery and isn't quite what's going on here vis-à-vis (co)Yoneda. However, you could talk about $\mathbf{2}$ "enriched" (co)Yoneda [essentially decategorifying] in which case you will get formulas involving universal and existential quantifiers, but that's also not what's going on here.)
A: Both the existential and the universal quantifier are examples of adjoint functors. They are left and right adjoint, respectively, to an inclusion map. 
You can read about it in Peter Smith‘s The Galois Connection between Syntax and Semantics. 
