The extended predicative Mahlo universe in Martin-Löf type theory (Q6636674)
From MaRDI portal
 | This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use this page instead for the normal view: The extended predicative Mahlo universe in Martin-Löf type theory |
scientific article; zbMATH DE number 7942586
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | The extended predicative Mahlo universe in Martin-Löf type theory |
scientific article; zbMATH DE number 7942586 |
Statements
The extended predicative Mahlo universe in Martin-Löf type theory (English)
0 references
12 November 2024
0 references
Martin-Löf type theory
0 references
Mahlo
0 references
universes
0 references
meaning explanations
0 references
extended predicativity
0 references
predicativity
0 references
explicit mathematics
0 references
inductive-recursive definitions
0 references
indexed induction-recursion
0 references
constructive mathematics
0 references
Agda
0 references
partial functions
0 references
