DROPS

Document

DOI: 10.4230/LIPIcs.TYPES.2021.2

Formalisation of Dependent Type Theory: The Example of CaTT

Authors: Thibaut Benjamin

Published in: LIPIcs, Volume 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021)

Abstract

We present the type theory CaTT, originally introduced by Finster and Mimram to describe globular weak ω-categories, formalise this theory in the language of homotopy type theory and discuss connections with the open problem internalising higher structures. Most of the studies about this type theory assume that it is well-formed and satisfy the usual syntactic properties that dependent type theories enjoy, without being completely clear and thorough about what these properties are exactly. We use our formalisation to list and formally prove all of these meta-properties, thus filling a gap in the foundational aspect. We discuss the aspects of the formalisation inherent to CaTT. We present the formalisation in a way that not only handles the type theory CaTT but also related type theories that share the same structure, and in particular we show that this formalisation provides a proper ground to the study of the theory MCaTT which describes the globular monoidal weak ω-categories. The article is accompanied by a development in the proof assistant Agda to check the formalisation that we present.

Cite as

Thibaut Benjamin. Formalisation of Dependent Type Theory: The Example of CaTT. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 2:1-2:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{benjamin:LIPIcs.TYPES.2021.2,
  author =	{Benjamin, Thibaut},
  title =	{{Formalisation of Dependent Type Theory: The Example of CaTT}},
  booktitle =	{27th International Conference on Types for Proofs and Programs (TYPES 2021)},
  pages =	{2:1--2:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-254-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{239},
  editor =	{Basold, Henning and Cockx, Jesper and Ghilezan, Silvia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.2},
  URN =		{urn:nbn:de:0030-drops-167719},
  doi =		{10.4230/LIPIcs.TYPES.2021.2},
  annote =	{Keywords: Dependent type theory, homotopy type theory, higher categories, formalisation, Agda, proof assistant}
}

Search Results

Documents authored by Benjamin, Thibaut

Formalisation of Dependent Type Theory: The Example of CaTT

Abstract

Cite as

Thanks for your feedback!

Could not send message