Database
BASIC CATEGORY THEORY
Categories
Functors
df-idfu
Next ⟩
df-cofu
Metamath Proof Explorer
Ascii
Unicode
Definition
df-idfu
Description:
Define the identity functor.
(Contributed by
Mario Carneiro
, 3-Jan-2017)
Ref
Expression
Assertion
df-idfu
⊢
id
func
=
t
∈
Cat
⟼
⦋
Base
t
/
b
⦌
I
↾
b
z
∈
b
×
b
⟼
I
↾
Hom
⁡
t
⁡
z
Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
cidfu
class
id
func
1
vt
setvar
t
2
ccat
class
Cat
3
cbs
class
Base
4
1
cv
setvar
t
5
4
3
cfv
class
Base
t
6
vb
setvar
b
7
cid
class
I
8
6
cv
setvar
b
9
7
8
cres
class
I
↾
b
10
vz
setvar
z
11
8
8
cxp
class
b
×
b
12
chom
class
Hom
13
4
12
cfv
class
Hom
⁡
t
14
10
cv
setvar
z
15
14
13
cfv
class
Hom
⁡
t
⁡
z
16
7
15
cres
class
I
↾
Hom
⁡
t
⁡
z
17
10
11
16
cmpt
class
z
∈
b
×
b
⟼
I
↾
Hom
⁡
t
⁡
z
18
9
17
cop
class
I
↾
b
z
∈
b
×
b
⟼
I
↾
Hom
⁡
t
⁡
z
19
6
5
18
csb
class
⦋
Base
t
/
b
⦌
I
↾
b
z
∈
b
×
b
⟼
I
↾
Hom
⁡
t
⁡
z
20
1
2
19
cmpt
class
t
∈
Cat
⟼
⦋
Base
t
/
b
⦌
I
↾
b
z
∈
b
×
b
⟼
I
↾
Hom
⁡
t
⁡
z
21
0
20
wceq
wff
id
func
=
t
∈
Cat
⟼
⦋
Base
t
/
b
⦌
I
↾
b
z
∈
b
×
b
⟼
I
↾
Hom
⁡
t
⁡
z