Internal type theory
type: Item
instance of: scholarly article
title: Internal type theory
zbMATH Open document ID: 1434.03149
DOI: 10.1007/3-540-61780-9_66
author: Peter Dybjer
published in: Lecture Notes in Computer Science
publication date: 2019-01-15T00:00:00Z
Mathematics Subject Classification ID: 03G30
Mathematics Subject Classification ID: 03B38
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 18B99
zbMATH DE Number: 7002049
zbMATH Keywords: type theory
zbMATH Keywords: dependent type
zbMATH Keywords: proof assistant
zbMATH Keywords: coherence condition
zbMATH Keywords: equality judgement
describes a project that uses: LEGO
MaRDI profile type: Publication
full work available at URL: 3-540-61780-9 66
OpenAlex ID: W1494555245
cites work: Fibered categories and the foundations of naive category theory
cites work: Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids
cites work: Generalized algebraic theories and contextual categories
cites work: Intuitionistic model constructions and normalization proofs
cites work: Q3142163
cites work: Q4225149
cites work: Q3886868
cites work: Categorical abstract machines for higher-order typed \(\lambda\)-calculi
cites work: Locally cartesian closed categories and type theory
description: scientific article; zbMATH DE number 7002049