2728293031323330 of 88
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
A Proof and Formalization of the Initiality Conjecture of Dependent Type Theory
Stockholm University, Faculty of Science, Department of Mathematics.
2020 (English)Licentiate thesis, monograph (Other academic)
Abstract [en]

In this licentiate thesis we present a proof of the initiality conjecture for Martin-Löf’s type theory with 0, 1, N, A+B, AB, AB, IdA(u,v), countable hierarchy of universes (Ui)iєN closed under these type constructors and with type of elements (ELi(a))iєN. We employ the categorical semantics of contextual categories. The proof is based on a formalization in the proof assistant Agda done by Guillaume Brunerie and the author. This work was part of a joint project with Peter LeFanu Lumsdaine and Anders Mörtberg, who are developing a separate formalization of this conjecture with respect to categories with attributes and using the proof assistant Coq over the UniMath library instead. Results from this project are planned to be published in the future.

We start by carefully setting up the syntax and rules for the dependent type theory in question followed by an introduction to contextual categories. We then define the partial interpretation of raw syntax into a contextual category and we prove that this interpretation is total on well-formed input. By doing so, we define a functor from the term model, which is built out of the syntax, into any contextual category and we show that any two such functors are equal. This establishes that the term model is initial among contextual categories. At the end we discuss details of the formalization and future directions for research. In particular, we discuss a memory issue that arose in type checking the formalization and how it was resolved.

Place, publisher, year, edition, pages
Stockholm: Department of Mathematics, Stockholm University , 2020. , p. 94
Keywords [en]
Dependent type theory, Category theory, Contextual categories, Initiality, Formalization
National Category
Algebra and Logic
Research subject
Mathematics; Mathematical Logic
Identifiers
URN: urn:nbn:se:su:diva-181640OAI: oai:DiVA.org:su-181640DiVA, id: diva2:1431287
Presentation
2020-06-15, Stockholm, 14:30 (English)
Opponent
Supervisors
Note

Licentiate defense over Zoom.

Available from: 2020-05-20 Created: 2020-05-19 Last updated: 2020-05-20Bibliographically approved

Open Access in DiVA

fulltext(703 kB)12 downloads
File information
File name FULLTEXT01.pdfFile size 703 kBChecksum SHA-512
d0347443d582d308efaa24cc554088aeefe1a44da6dfec22b4fb08cec9b2b1f49461f9e2886f1eb31b1a302ea2a95d3cde2e2e860d5727cfedaf948042e90089
Type fulltextMimetype application/pdf

Search in DiVA

By author/editor
de Boer, Menno
By organisation
Department of Mathematics
Algebra and Logic

Search outside of DiVA

GoogleGoogle Scholar
Total: 12 downloads
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

urn-nbn

Altmetric score

urn-nbn
Total: 101 hits
2728293031323330 of 88
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf