Diplomová práce

Model categories for type theory

Bc. Lukáš Krajíček
Anotace

Práce se zabývá modelovými strukturami a Grothendieckovou konstrukcí. Konstrukce poskytuje 2-ekvivalenci mezi Grothendieckovými fibracemi a indexovanými kategoriemi. Ukazuje se, že právě tyto 2-kategorie lze vyjádřit jako algebry pro vhodnou 2-monádu. V práci také uvádíme větu o zvedání modelových struktur skrze adjunkci. Společně tyto poznatky umožňují zkonstruovat a převést modelovou strukturu představenou …více

Abstract

The thesis revolves around model structures and the Grothendieck construction. The construction shows that there is a 2-equivalence between Grothendieck fibrations and indexed categories. It turns out that we are able to describe these 2-categories as algebras of a specific 2-monad. In the thesis, we also present theorems about lifting model structures via an adjunction. All these topics then provide …více

Klíčová slova
2-kategorie Grothendieckovy fibrace Grothendieckova konstrukce modelové kategorie lokálně prezentovatelné kategorie kombinatoriální modelová kategorie argument malých objektů argument objektů cest 2-monády kategorie T-algeber kanonická modelová struktura komprehenční kategorie teorie typů kategorická sémantika teorie typů 2-categories Grothendieck fibrations Grothendieck construction model categories locally presentable categories combinatorial model category small objects argument path objects argument 2-monads T-algebra categories canonical model structure comprehension categories power object copower object type theory categorical semantics of dependent type theory
Zadání práce
Dependent type theory is often modelled using categorical structures which build on the notion of Grothendieck fibration, such as comprehension categories and categories with attributes. Many 2-categories of categorical structures support Quillen model structures (arising in homotopy theory). The goal of this project will be to construct Quillen model structures for the different models of dependent type theory, using ideas from 2-category theory.
Administrativní informace
Práce zkontrolována:
11. 5. 2026 08:17, doc. John Denis Bourke, PhD, učo 115440
Plný text práce
926,3 KB / soubor PDF
Jazyk práce
angličtina angličtina
Termín obhajoby
9. 6. 2026
Práce byla úspěšně obhájena

Vedoucí

doc. John Denis Bourke, PhD, učo 115440
ÚMS Ústavy PřF MU

Oponent

doc. Lukáš Vokřínek, PhD., učo 43588
ÚMS Ústavy PřF MU
Citovat tuto práci
Masarykova univerzita Přírodovědecká fakulta
Studijní program
Plán
Matematika

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.