Obrnljive funkcije so sfere v svetuNajdovski, Timon (Avtor) Bauer, Andrej (Mentor) Rijke, Egbert Maarten (Komentor) Homotopska teorija tipovobrnljivostekvivalencasferaPredstavimo 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.20242024-09-18 08:16:07Delo diplomskega seminarja/zaključno seminarsko delo/naloga162014sl