View source for Book/Intuitionistic Type Theory

{{cite book
|title=Intuitionistic type theory
|first=Per
|last=Martin-Löf
|author-link=Per Martin-Löf
|date=June 1980
|url=http://www.cs.cmu.edu/afs/cs/Web/People/crary/819-f09/Martin-Lof80.pdf
|publisher=Springer
|location=[[Book/Intuitionistic Type Theory|local page]]
}}
<noinclude>
{{#Widget:PDF
|url=http://www.cs.cmu.edu/afs/cs/Web/People/crary/819-f09/Martin-Lof80.pdf
|{{#widget:YouTube
|id= hP3ENPc8Jf0
|width= 900
|height=500
}}|height=1200
}}
On page 87 of Martin-Löf's book<ref>{{:Book/Intuitionistic Type Theory}}</ref>, there is a section dedicated to talk about '''Universes''' which is the logical notion of [[Universality]].
=References=
<references/>
=Related Pages=
[[Category:Logic]]
[[Category:Universality]]
[[Category:Poset]]
</noinclude>