Zobrazeno 1 - 10
of 24
pro vyhledávání: '"GYLTERUD, HÅKON ROBBESTAD"'
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. For material set theory, we also have concrete models as 0-types in HoT
Externí odkaz:
http://arxiv.org/abs/2312.13024
Publikováno v:
Math. Struct. Comp. Sci. 34 (2024) 281-321
In this paper, we present a constructive and proof-relevant development of graph theory, including the notion of maps, their faces, and maps of graphs embedded in the sphere, in homotopy type theory. This allows us to provide an elementary characteri
Externí odkaz:
http://arxiv.org/abs/2112.06633
Non-wellfounded material sets have previously been modeled in Martin-L\"of type theory by Lindstr\"om using setoids. In this paper we construct models of non-wellfounded material sets in Homotopy Type Theory (HoTT) where equality is interpreted as th
Externí odkaz:
http://arxiv.org/abs/2001.06696
Akademický článek
Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.
K zobrazení výsledku je třeba se přihlásit.
Autor:
Gylterud, Håkon Robbestad
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 Martin-L\"of type theory, without Higher Inductive Types (HITs), and
Externí odkaz:
http://arxiv.org/abs/1612.05468
Autor:
Gylterud, Håkon Robbestad
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. In this work we will investigate the notion of iterative multisets, w
Externí odkaz:
http://arxiv.org/abs/1610.08027
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 interest for computer science is that this category can be seen to represent
Externí odkaz:
http://arxiv.org/abs/1406.6268
Autor:
GYLTERUD, HÅKON ROBBESTAD
Publikováno v:
The Journal of Symbolic Logic, 2018 Sep 01. 83(3), 1132-1146.
Externí odkaz:
https://www.jstor.org/stable/26600365
Publikováno v:
Forssell, Jon Henrik Gylterud, Håkon Robbestad Spivak, David I . Type theoretical databases. Jo
Jo
Jo
Externí odkaz:
http://hdl.handle.net/10852/85289
https://www.duo.uio.no/bitstream/handle/10852/85289/1/exaa009.pdf
https://www.duo.uio.no/bitstream/handle/10852/85289/1/exaa009.pdf
Aczel's anti-foundation axiom (AFA) is an alternative -- dual -- axiom to the usual axiom of foundation in set theory. This article constructs a model of AFA in homotopy type theory. Like the previous model of AFA in type theory, by Lindstr\"om (1989
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::8739354d6821059838607399dbc0c415