Change search
ReferencesLink to record
Permanent link

Direct link
Categories with families, FOLDS and logic enriched type theory
Stockholm University, Faculty of Science, Department of Mathematics.
2016 (English)Manuscript (preprint) (Other academic)
Abstract [en]

Categories with families (cwfs) is an established semantical structure for dependent type theories, such as Martin-Lö type theory. Makkai's first-order logic with dependent sorts (FOLDS) is an example of a so-called logic enriched type theory. We introduce in this article a notion of hyperdoctrine over a cwf, and show how FOLDS and Aczel's and Belo's dependently typed (intuitionistic) first-order logic (DFOL) fit in this semantical framework. A soundness and completeness theorem is proved for such a logic. The semantics is functorial in the sense of Lawvere, and uses a dependent version of the Lindenbaum-Tarski algebra for a DFOL theory. Agreement with standard first-order semantics is established. Some applications of DFOL to constructive mathematics and categorical foundations are given. A key feature is a local propositions-as-types principle.

Place, publisher, year, edition, pages
2016. , 99 p.
Keyword [en]
Intuitionistic first-order logic, dependent types, categorical logic, models of type theory
National Category
Algebra and Logic
Research subject
Mathematical Logic
URN: urn:nbn:se:su:diva-129963OAI: diva2:926427
Konstruktiva och kategoriteoretiska grundvalar för matematik
Swedish Research Council, 2015-03835
Available from: 2016-05-06 Created: 2016-05-06 Last updated: 2016-05-12

Open Access in DiVA

No full text

Other links


Search in DiVA

By author/editor
Palmgren, Erik
By organisation
Department of Mathematics
Algebra and Logic

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 5 hits
ReferencesLink to record
Permanent link

Direct link