Obrnljive funkcije so sfere v svetu : delo diplomskega seminarja

Najdovski, Timon (avtor), Bauer, Andrej (mentor), Rijke, Egbert Maarten (komentor)

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.

• Jezik: Slovenski jezik
• Ključne besede: Homotopska teorija tipov, obrnljivost, ekvivalenca, sfera
• Vrsta gradiva: Delo diplomskega seminarja/zaključno seminarsko delo/naloga
• Tipologija: 2.11 - Diplomsko delo
• Organizacija: FMF - Fakulteta za matematiko in fiziko
• Leto izida: 2024
• PID: 20.500.12556/RUL-162014
• UDK: 510.6
• COBISS.SI-ID: 208358915
• Datum objave v RUL: 18.09.2024

Sekundarni jezik

• Jezik: Angleški jezik
• Naslov: Invertible maps are spheres in the universe

Izvleček

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.

• Ključne besede: homotopy type theory, invertibility, equivalence, sphere