20.500.12556/RUL-162014 Obrnljive funkcije so sfere v svetu delo diplomskega seminarja Invertible maps are spheres in the universe 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. 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. Homotopska teorija tipov obrnljivost ekvivalenca sfera homotopy type theory invertibility equivalence sphere true false false Slovenski jezik Angleški jezik Delo diplomskega seminarja/zaključno seminarsko delo/naloga 2024-09-18 08:16:07 2024-09-18 08:16:10 2024-09-20 13:52:04 0000-00-00 00:00:00 2024 0 0 0000-00-00 NiDoloceno NiDoloceno NiDoloceno 0000-00-00 0000-00-00 0000-00-00 510.6 143632 208358915 12933.pdf 12933.pdf 1 9C69E9590B2D583C159B319025CC62EC 5f78be452808eb3282e3dbde4b24745745d7404a767dd55c8c98be3bcb15e9a2 6417dcae-7585-11ef-b232-0050569b8976 https://repozitorij.uni-lj.si/Dokument.php?lang=slv&id=191028 Fakulteta za matematiko in fiziko 0 0 0