Håkon Robbestad Gylterud: Strong collection, subset collection and the identity type

Strong collection and subset collection are two axioms of constructive set theory. They are distinct from other set theoretical axioms in that they claim existence of certain sets, but do not characterise these sets precisely. Their constructive justification is closely tied to Aczel’s model of constructive set theory in type theory, and the notion of operation versus the notion of function. I will in this talk discuss these axioms in the context of a model where the interpretation of equality is the identity type. As it turns out, it is instructive to first consider the equivalents of these axioms for multisets.