Kraus, Nicolai, Nordvall Forsberg, Fredrik, Xu, Chuangjie, "Connecting Constructive Notions of Ordinals in Homotopy Type Theory", , 2021