Connecting Constructive Notions of Ordinals in Homotopy Type Theory