Bakalářská práce

Homotopická teorie typů

Homotopy Type Theory

Marek Coufalík, učo 483954
Anotace

Tato bakalářská práce se věnuje homotopické teorii typů. V práci jsou uvedeny základy teorie typů a souvislosti mezi teorií typů a teorií homotopie. Práce se dále věnuje fundamentální grupě kružnice. Ukázali jsme, že tato grupa je izomorfní grupě celých čísel. Důkaz je proveden jednak topologicky s využitím nakrývacích prostorů a jednak v homotopické teorii typů s implementací v Agdě, která tvoří přílohu práce.

Abstract

This bachelor thesis is devoted to homotopy type theory. The thesis presents the foundations of type theory and the connections between type theory and homotopy theory. The thesis also discusses the fundamental group of the circle. We show that this group is isomorphic to the group of integers. The proof is done both topologically using covering spaces and in homotopy type theory with an implementation in Agda, which is an appendix of the thesis.

Klíčová slova
Homotopická teorie typů Fundamentální grupa kružnice Teorie typů Identický typ Univerzální nakrytí Programovací jazyk Agda Kódování Homotopy type theory Fundamental group of the circle Type theory Identity type Universal cover Programming language Agda Encoding
Zadání práce
Práce vyloží základy homotopické teorie typů.
Administrativní informace
Práce zkontrolována:
11. 5. 2022 14:44, doc. Lukáš Vokřínek, PhD., učo 43588
Plný text práce
551,8 KB / soubor PDF
Přílohy (1)
Jazyk práce
čeština čeština
Termín obhajoby
27. 6. 2022
Práce byla úspěšně obhájena

Vedoucí

doc. Lukáš Vokřínek, PhD., učo 43588
ÚMS Ústavy PřF MU

Oponent

Mgr. Dominik Trnka, Ph.D., učo 449931
ÚMS Ústavy PřF MU

Literatura

  • The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, 2013.
Citovat tuto práci
Masarykova univerzita Přírodovědecká fakulta
Studijní program
Matematika
Obor

Práce na příbuzné téma

Seznam prací, které mají shodná klíčová slova.

Podobné práce

  • Přidání souboru

    Soubor nebo složku lze nahrát pomocí tlačítka Přidat.

  • Další operace se soubory

    Podrobnosti lze zjistit označením příslušného řádku.

  • Pohled pro experty

    Pro častou práci je možné zvolit režim Více možností.

  • Vyhledávání souborů

    Vyhledávaný výraz můžete zadat přímo do adresního řádku.

  • Rychlý přístup k souborům

    Pomocí funkce Nedávné je možné se rychle vrátit k právě prohlíženým souborům. Oblíbené soubory je také možné označit Hvězdičkou.