Loop suspension adjunction on based homotopy classes

A based map $a:\mathrm{\Sigma }X\to Y$ pulls back to $A:X\times I\to Y$ with A(x,0)=A(x,1)=y0 and A(x0,t)=y0. By F2 its transpose $b(x)(t)=A(x,t)$ is continuous into the based loop space and maps x0 to the constant loop. Conversely a based b uncurries continuously and satisfies exactly those three equations, so descends to a based a by F1. Evaluation at (x,t) verifies both inverse identities.

Apply F2 with the additional homotopy parameter: the same formulas identify homotopies fixing the basepoint in either mapping set, and their inverses preserve both endpoint maps. Thus the map bijection descends to a bijection on based homotopy classes. Replacing x by f(x) or postcomposing each value with g commutes with evaluation, proving naturality in both variables.