Well sums and existential quantifiers are almost the same thing in type theory.

My guess is that sums and existentials /are/ coends of some sort, because then the formula given would be valid for all cases.