The extended predicative Mahlo universe in Martin-Löf type theory
type: Item
instance of: scholarly article
title: The extended predicative Mahlo universe in Martin-Löf type theory
author: Peter Dybjer
author: Anton Setzer
publication date: 2024-11-12T00:00:00Z
Mathematics Subject Classification ID: 03-XX
Mathematics Subject Classification ID: 68-XX
zbMATH DE Number: 7942586
zbMATH Keywords: Martin-Löf type theory
zbMATH Keywords: Mahlo
zbMATH Keywords: universes
zbMATH Keywords: meaning explanations
zbMATH Keywords: extended predicativity
zbMATH Keywords: predicativity
zbMATH Keywords: explicit mathematics
zbMATH Keywords: inductive-recursive definitions
zbMATH Keywords: indexed induction-recursion
zbMATH Keywords: constructive mathematics
zbMATH Keywords: Agda
zbMATH Keywords: partial functions
MaRDI profile type: Publication
published in: Journal Of Logic And Computation
DOI: 10.1093/LOGCOM/EXAD022
description: scientific article; zbMATH DE number 7942586