Introduction
▶
What is a formalization project?
What is this docuemnt?
What is this project about?
1
Single-sorted presentation
▶
1.1
Single-sorted categories
1.2
Single-sorted functors
1.3
The category of single-sorted categories
2
Underlying transformations
▶
2.1
Underlying single-sorted categories
2.2
Underlying single-sorted functors
2.3
Functoriality of the underlying transformations
3
Bibliography
Dependency graph
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?
1
Single-sorted presentation
1.1
Single-sorted categories
1.2
Single-sorted functors
1.3
The category of single-sorted categories
2
Underlying transformations
2.1
Underlying single-sorted categories
2.2
Underlying single-sorted functors
2.3
Functoriality of the underlying transformations
3
Bibliography