Gaïa Loutchmia: A formalization of second-order syntax and its categorical structure
Attention: we meet at a non-standard time on Wednesday, 23. 6. 2021 at 10:00!
Abstract: We present ongoing work on formalisation of the syntax of second order theories, which we are currently implementing in the Agda proof assistant. We shall also outline a possible categorical structure expressing the syntactic aspects (terms, substitutions, renamings), from which follow natural syntactic lemmas. This categorical structure turns out to be a combination of relative monads, which express how terms arise from variables and metavariables. We are working on the relations between the relative monads we defined, that correspond to the interactions between operations related to variables and operations related to metavariables. This is still work in progress.
Joint work with Danel Ahman, Andrej Bauer and Jure Taslak.