A Cartesian Bicategory of Polynomial Functors in Homotopy Type Theory