There seems to be some literature stating that Mahlo Universe is the counterpart of Mahlo Cardinal in type theory, but I don't fully understand this point of knowledge.
More explicitly, I would like to know what condition is missing between
CIC + a Mahlo Universe and
IZF + a Mahlo Cardinal?
 Setzer, A. (2000). Extending Martin-Löf type theory by one Mahlo-universe. Archive for Mathematical Logic, 39(3), 155-181.
 Kahle, R., & Setzer, A. (2010). An extended predicative definition of the Mahlo universe. Ways of Proof Theory. De Gruyter. doi, 10(9783110324907), 315.