Coslice Colimits in Homotopy Type Theory