Håkon Robbestad Gylterud: Iterative multisets and sets in homotopy type theory

Håkon Robbestad Gylterud

University of Stockholm

 

Abstract: In 1977 Aczel [1] constructed a model of constructive set theory (CZF) in Martin-Löf’s dependent type theory. Aczel’s structure is a setoid — a type equipped with an equivalence relation on it. This talk starts out by giving an analysis of the identity type of the underlying type of Aczel’s setoid, relating it to the notion of a multiset.

This relationship serves as motivation for formulating several axioms for iterative multiset theory in type theory, and proving that Aczel’s type forms in a natural way a model of these. This model can then be used to construct a model of set theory, equivalent to the one presented in the book “Homotopy Type Theory” [2], but is less dependent upon on Higher Inductive Types in its formulation.

References:

[1]: Aczel, Peter (1978). “The Type Theoretic Interpretation of Constructive Set Theory”. In: Logic Colloquium ’77.

[2]: Univalent Foundations Programme (2013). “Homotopy type theory: Univelent foundations”.