@misc{indiciaedd13673b6ffe, title = {Connecting Constructive Notions of Ordinals in Homotopy Type Theory}, author = {Nicolai Kraus and Fredrik Nordvall Forsberg and Chuangjie Xu}, year = {2021}, doi = {10.4230/lipics.mfcs.2021.70}, url = {https://arxiv.org/abs/2104.02549}, note = {Source identifier: 2104.02549} }