Functorial

📁 Source: Mathlib/CategoryTheory/Functor/Functorial.lean

Statistics

Metric	Count
Definitions of, Functorial, map, functorial_comp, functorial_id, instFunctorialObj	6
Theorems map_comp, map_id, map_functorial_obj	3
Total	9

CategoryTheory

Definitions

Name	Category	Theorems
Functorial 📖	CompData	—
functorial_comp 📖	CompOp	—
functorial_id 📖	CompOp	—
instFunctorialObj 📖	CompOp	1 math math: map_functorial_obj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_functorial_obj 📖	mathematical	—	Functorial.map Functor.obj instFunctorialObj Functor.map	—	—

CategoryTheory.Functor

Definitions

Name	Category	Theorems
of 📖	CompOp	—

CategoryTheory.Functorial

Definitions

Name	Category	Theorems
map 📖	CompOp	3 math math: CategoryTheory.map_functorial_obj, map_comp, map_id

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_comp 📖	mathematical	—	map CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
map_id 📖	mathematical	—	map CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—

---

← Back to Index