An Invitation to Category Theory

Introduction

Advantages of Agda:

• It will tell you precisely where you are wrong.
• When you forget a definition you can just click on the type signature.

Decisions Made for this Website

• I avoided universe levels as much as possible. They make type signatures confusing for beginners.
• I split type signatures (i.e. the proposition/problem) from the function implementation (i.e. the proof/solution)
• I made some assumptions in classical postulates. This avoids using Cubical Agda which is not beginner friendly.

In general, I want readers to be able to grasp the concept of the file within 30s of opening it, and then expand sections to go into finer grained details.

Where to start

Check out Proposition 1.14. Click on the agda code to navigate.