Material Set Theory in Homotopy Type Theory

Abstract

Denne avhandlingen undersøker modeller av materiell mengdelære i homotopi typeteori (HoTT), det vil si, tolkninger av språket for mengdelære inn i HoTT slik at tolkningene av aksiomene i mengdelære kan vises å holde.

En viktig egenskap av en gitt modell er hvordan likhetsrelasjonen blir tolket. I HoTT er typen for likhet mellom to elementer den såkalte identitetstypen. Det sentrale temaet for denne avhandlingen er at alle modellene tolker likhet som identitetstypen.

Avhandlingen består av tre artikler. Den første er en nærmere undersøkning av en spesifikk modell av konstruktiv mengdelære som kalles for det iterative hierarkiet av mengder (denne konstruksjonen ble laget før denne avhandlingen), som blir vist å ha mange ønskelige egenskaper. Det vises spesielt at, i tillegg til å gi en modell for materiell mengdelære i HoTT, så gir den også en modell for ekstensionell typeteori i HoTT.

Den andre artikkelen bruker at HoTT er et bevisrelevant rammeverk med høyere struktur, til å gi en høyereordens generalisering av tolkningene av mengdelæreaksiomene som ble gitt i den første artikkelen. Den inneholder også konstruksjonen av en høyereordens generalisering av modellen i den artikkelen. På det første nivået av generalisering blir dette en modell av multimengder istedet for mengder. Konstruksjonen blir også gjort til et internt univers (dette kan tenkes på som en 'type av typer') av n-typer, som i seg selv er en n-type.

Den siste artikkelen undersøker modeller for ikke-velfundert mengdelære i HoTT. Ikke-velfunderte mengder er mengder som kan inneholde en uendelig lang rekke med medlemskap: a₀ ∋ a₁ ∋ a₂ ∋ ⋯, i motsettning til velfunderte mengder hvor hver slik rekke må være endelig. De ikke-velfunderte mengdene kan brukes til å modellere sirkulære fenomen som for eksempel tilstandsmaskiner eller strømmer i informatikk. Modellene i denne artikkelen tolker ikke-velfunderte mengder som ikke-velfunderte trær. En familie av modeller blir laget ved å dualisere konstruksjonen av det iterative hierarkiet av mengder som ble undersøkt i den første artikkelen. Et overraskende resultat er at denne dualiseringen ikke gir en modell av den vanlige typen ikke-velfunderte mengder (det finnes flere), uten istedet en annen, mindre velkjent versjon av ikke-velfunderte mengder.

This thesis investigates models of material set theory in Homotopy Type Theory (HoTT), that is, interpretations of the language of set theory into HoTT such that the interpretations of the set theoretic axioms can be shown to hold.

An important feature of a given model is how the equality relation is interpreted. In HoTT, the type for equality between two elements is called the identity type. The central theme of this thesis is that all its models interpret equality as the identity type.

The thesis is based on three papers. The first being a closer investigation of one specific model of constructive set theory, called the iterative hierarchy of sets (its construction predating this thesis) which is shown to have many desirable properties. In particular, it is shown that, as well as giving a model of material set theory in HoTT, it also gives a model of extensional type theory inside HoTT.

The second paper utilises that HoTT is a proof relevant framework which has higher structure, to give a higher level generalisation of the interpretations of the set theoretic axioms given in the first paper. It also contains the construction of a higher level generalisation of the model in that paper. At the first level of generalisation, this becomes a model of multisets, rather than sets. The construction is also made into an internal universe (this can be thought of as a 'type of types') of n-types, which is itself an n-type.

The final paper investigates models of non-wellfounded set theory in HoTT. Non-wellfounded sets are sets which may contain an infinite membership chain: a₀ ∋ a₁ ∋ a₂ ∋ ⋯, as opposed to wellfounded sets where every such chain is required to be finite. The non-wellfounded sets are useful for modeling circular phenomena such as state machines or streams in computer science. The models in this paper interpret non-wellfounded sets as non-wellfounded trees. One family of models is obtained by dualising the construction of the iterative hierarchy of sets investigated in the first paper. A surprising result is that this dualisation does not yield a model of the usual kind of non-wellfounded sets (there are several), but rather of a different, less well known, notion of non-wellfounded sets.