4 papers
Univalent Material Set Theory
Håkon Robbestad Gylterud, Elisabeth Stenholm
Homotopy type theory (HoTT) can be seen as a generalisation of structural set theory, in the sense that 0-types represent structural sets within the more general notion of types. F…
Terminal Coalgebras and Non-wellfounded Sets in Homotopy Type Theory
Hakon Robbestad Gylterud, Elisabeth Stenholm, Niccolò Veltri
Non-well-founded material sets have been modelled in Martin-Löf type theory by Lindström using setoids. In this paper we construct models of non-wellfounded material sets in Homoto…
From Multisets to Sets in Hotmotopy Type Theory
Håkon Robbestad Gylterud
We give a model of set theory based on multisets in homotopy type theory. The equality of the model is the identity type. The underlying type of iterative sets can be formulated in…
Multisets in Type Theory
Håkon Robbestad Gylterud
A multiset consists of elements, but the notion of a multiset is distinguished from that of a set by carrying information of how many times each element occurs in a given multiset.…