Library
▹
Category theory
Definition 4.5.
Let
u
∈
ℕ
,
C
be a/an
u
-small category
,
X
,
Y
,
Z
∈
C
,
f
:
X
→
Y
,
g
:
Y
→
Z
be
morphisms
. We define:
g
∘
f
:
=
g
∘
X
,
Y
,
Z
f
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:Composition_of_Morphisms