Talk:Intuitionistic type theory
Proposed move to “Martin-Löf type theory”: new section
| ← Previous revision | Revision as of 17:12, 24 April 2026 | ||
| Line 95: | Line 95: | ||
I'm confused about the remark regarding the univalence axiom pertaining to MLTT73 -- it seems on the face of it that a statement of the univalence axiom only pertains to the types of a fixed universe, and doesn't seem like it should need identity types that relate types of different universes. But maybe there's a detail about how MLTT73 is structured that I'm not taking into account here. |
I'm confused about the remark regarding the univalence axiom pertaining to MLTT73 -- it seems on the face of it that a statement of the univalence axiom only pertains to the types of a fixed universe, and doesn't seem like it should need identity types that relate types of different universes. But maybe there's a detail about how MLTT73 is structured that I'm not taking into account here. |
||
[[User:Cgibbard|Cgibbard]] ([[User talk:Cgibbard|talk]]) 16:32, 8 November 2024 (UTC) |
[[User:Cgibbard|Cgibbard]] ([[User talk:Cgibbard|talk]]) 16:32, 8 November 2024 (UTC) |
||
== Proposed move to “Martin-Löf type theory” == |
|||
I propose renaming this article to “Martin-Löf type theory” because the latter name is extremely common in literature on the subject whereas I think I've only ever seen “intuitionistic type theory” used in the writings of Per Martin-Löf himself. I will perform the move in a few days if no objection arises. [[User:Jean Abou Samra|Jean Abou Samra]] ([[User talk:Jean Abou Samra|talk]]) 17:12, 24 April 2026 (UTC) |
|||
