Coslice Colimits in Homotopy Type Theory. - Perry Hart; Kuen-Bang Hou (Favonia) (CSL, 2025)