Library
▹
Category theory
▹
Functors
Definition 4.7.4.
Let
u
∈
ℕ
,
C
be a/an
u
-small category
. We define:
id
C
:
C
→
C
X
↦
X
(
f
:
A
→
B
)
↦
f
References.
https://proofwiki.org/wiki/Definition:Identity_Functor
https://ncatlab.org/nlab/show/identity+functor
https://leanprover-community.github.io/mathlib_docs/category_theory/functor.html#category_theory.functor.id