Erik Palmgren: Exploring generalized algebraic theories with the proof assistant Agda

ABSTRACT: Generalized algebraic theories (GATs) (Cartmell 1978, 1986) is a general form equational logic where the sorts (types) can depend on other sorts and terms, also, it allows for equations between sorts. GATs can serve as basis for categorical theories, and for type theory itself. Most proof assistants do not allow for the introduction of arbitrary judgemental equalities as GATs do, since this would destroy decidability of type checking. In this talk we explore the possibility of to implement GATs as a term calculus in Agda, and the prospects of formalizing proofs of meta-theorems about GATs.