Universal algebra via theories of signatures

Témavezető: Kaposi Ambrus
Faculty of Informatics, ELTE
email: akaposi@ik.elte.hu

Témavezetők

Projekt leírás

Algebraic theories can be described concretely via the arities of operations and equations, or representation-independently via Lawvere theories. The theory of signatures (ToS) approach lies halfway between these two: there is a concrete signature, but the semantics is given by type theoretic model constructions for the ToS. The ToS approach also scales to generalised algebraic theories (close to essentially algebraic theories). The goal of the project is to reproduce standard results from universal algebra and generalised universal algebra.

Előfeltételek

Basic semantics of Martin-Löf Type Theory.

Hivatkozások

Ambrus Kaposi, Szumi Xie. Second-order generalised algebraic theories: signatures and first-order semantics. FSCD 2024 András Kovács. Type-Theoretic Signatures for Algebraic Theories and Inductive Types. PhD thesis, ELTE 2022 Ambrus Kaposi. Second-order generalised algebraic theories, by examples. Draft course notes, 2026