Synthetic Mathematics, Logical Frameworks, and Categorical Algebra

Abstract

I’ll be talking about three topics near and dear to my heart: synthetic mathematics, interactive theorem proving, and categorical algebra. My aim is to give an overview of how these topics are intimately linked, culminating in a discussion of how they can be used in tandem to give an elegant formal approach to problems at the heart of formal logic and type theory. To this end, I will proceed through a series of questions:
What is synthetic mathematics? …and why should I care?What is a logical framework? …and how can I use one to help me do math?What is categorical algebra? …and what are its limits?
4. What do synthetic mathematics, logical frameworks, and categorical algebra have to do with each other?