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?
- What do synthetic mathematics, logical frameworks, and categorical algebra have to do with each other?