I’m pleased that our paper, together with @de_Jong_Tom@mathstodon.xyz, @Nicolai_Kraus@mathstodon.xyz, and @fnf@mathstodon.xyz, is now on arXiv. In this work, we explore the “sweet spot” of the type of Brouwer ordinals (defined in HoTT as a quotient inductive-inductive type) to develop a theory of ordinal decidability that generalizes decidability and semidecidability. Our results are formalized in cubical Agda.

https://arxiv.org/abs/2602.10844