Paper Info
Title
Internal Type Theory
Abstract
Abstract: We introduce categories with families as a new notion ofmodel for a basic framework of dependent types. This notion is closeto ordinary syntax and yet has a clean categorical description. We alsopresent categories with families as a generalized algebraic theory. Thenwe define categories with families formally in Martin-Lof's intensionalintuitionistic type theory. Finally, we discuss the coherence problem forthese internal categories with families.
Year
DOI
Venue
1995
10.1007/3-540-61780-9_66
TYPES
Keywords
Field
DocType
internal type theory,dependent types,type theory
Discrete mathematics,Intuitionistic type theory,Algebra,Computer science,Categorical variable,Type theory,Algebraic theory,Syntax,Dependent type,Coherence condition,Proof assistant
Conference
Volume
ISSN
ISBN
1158
0302-9743
3-540-61780-9
Citations 
PageRank 
References 
27
3.67
9
Authors
1
Name
Order
Citations
PageRank
Peter Dybjer154076.99