Introduction
▶
What is a formalization project?
What is this docuemnt?
What is this project about?
Single-sorted presentation
▶
Single-sorted categories
Single-sorted functors
The category of single-sorted categories
Underlying transformations
▶
Underlying single-sorted categories
Underlying single-sorted functors
Functoriality of the underlying transformations
Many-sorted presentation
▶
Many-sorted categories
Many-sorted functors
The category of many-sorted categories
A Formalization of Higher-Order Categories in Lean 4
Enric Cosme Llópez Raul Ruiz Mora Mario Vago Marzal
2025
Introduction
What is a formalization project?
What is this docuemnt?
What is this project about?
Single-sorted presentation
Single-sorted categories
Single-sorted functors
The category of single-sorted categories
Underlying transformations
Underlying single-sorted categories
Underlying single-sorted functors
Functoriality of the underlying transformations
Many-sorted presentation
Many-sorted categories
Many-sorted functors
The category of many-sorted categories