Per Martin-Löf. An Intuitionistic Theory of Types: Predicative Part. Studies in Logic and the Foundations of Mathematics, 80:73--118, 1975. https://doi.org/10.1016/S0049-237X(08)71945-1
Per Martin-Löf. An Intuitionistic Theory of Types: Predicative Part. Studies in Logic and the Foundations of Mathematics, 80:73--118, 1975. https://doi.org/10.1016/S0049-237X(08)71945-1