The extended predicative Mahlo universe in Martin-Löf type theory (2023) 30 points by danny00 3 days ago story