Anton Setzer. Extending Martin-Löf Type Theory by one Mahlo-universe. Arch. Math. Log., 39(3):155-181, 2000. [doi]
@article{Setzer00, title = {Extending Martin-Löf Type Theory by one Mahlo-universe}, author = {Anton Setzer}, year = {2000}, doi = {10.1007/s001530050140}, url = {http://dx.doi.org/10.1007/s001530050140}, tags = {type theory}, researchr = {https://researchr.org/publication/Setzer00}, cites = {0}, citedby = {0}, journal = {Arch. Math. Log.}, volume = {39}, number = {3}, pages = {155-181}, }