1
Introduction
▶
1.1
Formalization and this document
1.2
Project overview
1.3
Project status
1.4
Notation and terminology
2
Single-sorted presentation
▶
2.1
Single-sorted categories
2.2
Single-sorted functors
2.3
The category of single-sorted categories
3
Single-sorted discretization transformations
▶
3.1
Discrete single-sorted categories
3.2
Discrete single-sorted functors
3.3
Single-sorted discretization functors
4
Single-sorted underlying transformations
▶
4.1
Underlying single-sorted categories
4.2
Underlying single-sorted functors
4.3
Single-sorted underlying functors
5
Many-sorted presentation
▶
5.1
Many-sorted categories
5.2
Many-sorted functors
5.3
The category of many-sorted categories
6
Many-sorted discretization transformations
▶
6.1
Discrete many-sorted categories
6.2
Discrete many-sorted functors
6.3
Many-sorted discretization functors
7
Many-sorted underlying transformations
▶
7.1
Underlying many-sorted categories
7.2
Underlying many-sorted functors
7.3
Many-sorted underlying functors
8
Bibliography
Dependency graph
A Formalization of Higher-Order Categories in Lean 4
Enric Cosme Llópez Raúl Ruiz Mora Mario Vago Marzal
2025-2026
1
Introduction
1.1
Formalization and this document
1.2
Project overview
1.3
Project status
1.4
Notation and terminology
2
Single-sorted presentation
2.1
Single-sorted categories
2.2
Single-sorted functors
2.3
The category of single-sorted categories
3
Single-sorted discretization transformations
3.1
Discrete single-sorted categories
3.2
Discrete single-sorted functors
3.3
Single-sorted discretization functors
4
Single-sorted underlying transformations
4.1
Underlying single-sorted categories
4.2
Underlying single-sorted functors
4.3
Single-sorted underlying functors
5
Many-sorted presentation
5.1
Many-sorted categories
5.2
Many-sorted functors
5.3
The category of many-sorted categories
6
Many-sorted discretization transformations
6.1
Discrete many-sorted categories
6.2
Discrete many-sorted functors
6.3
Many-sorted discretization functors
7
Many-sorted underlying transformations
7.1
Underlying many-sorted categories
7.2
Underlying many-sorted functors
7.3
Many-sorted underlying functors
8
Bibliography