I'm reading Tammo tom Dieck's algebraic topology text. In the text the Eckmann–Hilton duality is mentioned several times. My current understanding is that it captures the "equivalence" between a homotopy $X\times I\to Y$ and a parametrized family of paths $X\to Y^I$. This leads to, for example, the adjunction $F^0(\Sigma X,Y)\cong F^0(X,\Omega Y)$.
However, these are all informal ideas which I cannot make mathematically precise. In particular, I wonder if it can be formalized so that, as in category theory, dual statements can be proved to be equivalent? For example, if we have verified that the fiber sequence is indeed exact, then we won't have to take pains to verify the corresponding results for cofiber sequences. Is that possible?