Library
▹
Category theory
Definition 4.4.
Let
u
∈
ℕ
,
C
be a/an
u
-small category
,
X
∈
C
. We define:
id
X
:
=
i
X
if
C
=
[
O
(
M
A
,
B
)
A
,
B
∈
O
(
i
C
)
C
∈
O
(
∘
D
,
E
,
F
)
D
,
E
,
F
∈
O
]
u
(
O
is a set,
M
A
,
B
is a set for each
A
,
B
∈
O
,
i
C
∈
M
C
,
C
for each
C
∈
O
,
∘
D
,
E
,
F
:
M
E
,
F
×
M
D
,
E
→
M
D
,
F
is an
operation
for each
D
,
E
,
F
∈
O
with suitable conditions)
References.
https://proofwiki.org/wiki/Definition:Identity_Morphism