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.
Aref Mohammadzadeh
@aref_mz@mathstodon.xyz
PhD student at the FP Lab, University of Nottingham. I'm interested in homotopy type theory, higher category theory, and constructive math.
mathstodon.xyz