7 citations · 14 across the 5 of their papers we have counts for
5 papers · 1 filter
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.…
Type theoretical databases
Henrik Forssell, Håkon Robbestad Gylterud, David I. Spivak
We present a soundness theorem for a dependent type theory with context constants with respect to an indexed category of (finite, abstract) simplical complexes. The point of intere…