Obrnljive funkcije so sfere v svetu : delo diplomskega seminarja

Najdovski, Timon (author), Bauer, Andrej (mentor), Rijke, Egbert Maarten (comentor)

Predstavimo definicijo sodb in kontekstov ter predstavimo njihovo uporabo za definicijo konstrukcij tipov v Martin-Löfovi teoriji odvisnih tipov. Na funkcijah vpeljemo pojma obrnljivosti in ekvivalence ter pokažemo, da sta logično ekvivalentna. Na tipih vpeljemo pojma kontraktibilnosti in propozicij ter pokažemo, da je pojem ekvivalence propozicija. Vpeljemo tip krožnice in aksiom univalence ter ju uporabimo kot protiprimer, da pokažemo, da pojem obrnljivosti ni vedno propozicija. Posledično pojma obrnljivosti in ekvivalence nista ekvivalentna, saj pokažemo, da ekvivalence ohranjajo propozicionalnost. Na tipih vpeljemo še pojem množic in skiciramo razlog, zakaj sta pojma obrnljivosti in ekvivalence na funkcijah med množicami ekvivalentna. Predstavimo še nekaj standardnih trditev homotopske teorije tipov in predstavimo karakterizacijo obrnljivosti, ki jo poveže z ekvivalenco. Karakterizacijo uporabimo, da pokažemo povezavo med obrnljivostjo in tipom sfere.

• Language: Slovenian
• Keywords: Homotopska teorija tipov, obrnljivost, ekvivalenca, sfera
• Work type: Final seminar paper
• Typology: 2.11 - Undergraduate Thesis
• Organization: FMF - Faculty of Mathematics and Physics
• Year: 2024
• PID: 20.500.12556/RUL-162014
• UDC: 510.6
• COBISS.SI-ID: 208358915
• Publication date in RUL: 18.09.2024

Secondary language

• Language: English
• Title: Invertible maps are spheres in the universe

Abstract

We present the definition of judgments and contexts and use them to present the definitions of type formers in Martin-Löf dependent type theory. We introduce the notions of invertibility and equivalence of functions and show that they are logically equivalent. We introduce the notions contractibility and propositionality of types and show that the notion of equivalence always forms a proposition. We introduce the circle type and the univalence axiom and use them as a counterexample to show that the notion of invertibility need not always be a proposition. Consequently, the notions of invertibility and equivalence cannot be equivalent, since we show that equivalences preserve propositionality. We present a few standard results of homotopy type theory and present a characterisation of invertibility that connects it with equivalence. We use this characterisation to show a connection between invertibility and the sphere type.

• Keywords: homotopy type theory, invertibility, equivalence, sphere