research
∙
08/10/2023
Substitution for Non-Wellfounded Syntax with Binders
We describe a generic construction of non-wellfounded syntax involving v...
share
research
∙
07/30/2023
Formalizing Monoidal Categories and Actions for Syntax with Binders
We discuss some aspects of our work on the mechanization of syntax and s...
research
∙
12/06/2022
Univalent Monoidal Categories
Univalent categories constitute a well-behaved and useful notion of cate...
research
∙
09/02/2022
Category Theory for Programming
In these lecture notes, we give a brief introduction to some elements of...
research
∙
02/03/2022
Univalent foundations and the equivalence principle
In this paper, we explore the 'equivalence principle' (EP): roughly, sta...
research
∙
01/25/2022
Semantics for two-dimensional type theory
In this work, we propose a general notion of model for two-dimensional t...
research
∙
01/01/2022
The solutions to single-variable polynomials, implemented and verified in Lean
In this work, we describe our experience in learning the use of a comput...
research
∙
12/13/2021
Implementing a Category-Theoretic Framework for Typed Abstract Syntax
In previous work ("From signatures to monads in UniMath"), we described ...
research
∙
02/11/2021
The Univalence Principle
The Univalence Principle is the statement that equivalent mathematical s...
research
∙
04/14/2020
A Higher Structure Identity Principle
The ordinary Structure Identity Principle states that any property of se...
research
∙
11/14/2019
Reduction Monads and Their Signatures
In this work, we study 'reduction monads', which are essentially the sam...
research
∙
03/04/2019
Bicategories in Univalent Foundations
We develop bicategory theory in univalent foundations. Guided by the not...
research
∙
03/03/2019
Modular specification of monads through higher-order presentations
In their work on second-order equational logic, Fiore and Hur have studi...
research
∙
05/09/2018