Univalent Multisets

Haakon Robbestad Gylterud

(Stockholm University)

Multisets, like sets, consist of elements and the order of appearance of these elements is irrelevant. What distinguishes multisets from sets is the fact that number of occurrences of an element matters. In this talk I will show how one may capture this intuition in Martin-Löf Type Theory.

First, I will present a technical result on the identity types of W-types in type theory (without the Univalence Axiom). In light of this result I will give an analysis of the underlying type of Aczel's model of Constructive Zermelo Fraenkel set theory (CZF) in presence of the Univalence Axiom. The conclusion is that Aczel's type, considered with the identity type as equality, consists of iterative, transfinite multisets.

Thursday 20th March 2014, 14:00
Robert Recorde Room
Department of Computer Science