A coherence theorem for Martin-Löf's type theory
type: Item
instance of: scholarly article
title: A coherence theorem for Martin-Löf's type theory
zbMATH Open document ID: 0917.03028
DOI: 10.1017/S0956796898003153
author: Michael Hedberg
published in: Journal of Functional Programming
publication date: 1999-07-15T00:00:00Z
Mathematics Subject Classification ID: 03F35
Mathematics Subject Classification ID: 03G30
Mathematics Subject Classification ID: 03B40
zbMATH DE Number: 1270254
zbMATH Keywords: identity proofs
zbMATH Keywords: types with decidable identities
zbMATH Keywords: kernel fragment of Martin-Löf's type theory
zbMATH Keywords: category-theoretical properties
zbMATH Keywords: coherence
zbMATH Keywords: inductive equality
zbMATH Keywords: initial category structure
describes a project that uses: ALF
MaRDI profile type: Publication
full work available at URL: s0956796898003153
OpenAlex ID: W2102861499
description: scientific article; zbMATH DE number 1270254