Kraus, N., Nordvall Forsberg, F., & Xu, C. (2021, August). Connecting Constructive Notions of Ordinals in Homotopy Type Theory. Presented at 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021), Tallinn, Estonia