It is well known that a set of natural transformations can be expressed as an end:
$$\int_{A \in \mathcal{A}} \mathcal{B}(FA, GA) =_{\operatorname{Set}} \operatorname{Nat}(F, G)$$ This holds for functors $F, G \colon \mathcal{A} \to \mathcal{B}$.
Now in polymorphic lambda calculus (such as System F), there is a very similar phenomenon. Terms satisfy free theorems. As a special case of this, terms of type $\forall A. F A \to G A$ satisfy naturality. Now if we interpret this statement with semantics in $\operatorname{Set}$, it seems like well-typed terms of the above type again correspond to natural transformations from $F$ to $G$!
In Martin-Löf type theory, a similar statement should hold for types of the form $\Pi_{A : \operatorname{Set}} F A \to G A$.
Is there a connection between ends and parametricity? E.g. are ends the semantics of polymorphic types (or $\Pi$-types)?
Bonus: Is there a similar phenomenon for coends? (E.g. $\Sigma$-types or existential quantification?)
