Naturality in
a requires that for any
g:a→b the following
diagram commutes:
where
ηg is given by
(ηg)x(f:b→x)=ηx(f∘g).
Equationally this asks that
(ηg)b(idb)=F(g)(ηa(ida))
Applying the definition of
ηg to the left-hand side and applying
(⋆) to the right-hand side rewrites this as
ηb(idb∘g)=ηb(g)
which is true.
Naturality in
F requires that for any
α:F⇒G the following
diagram commutes:
where
αη is given by
(αη)x(f)=αa(ηx(f)).
Equationally this asks that
(αη)a(ida)=αa(ηa(ida))
which follows from the definition of
αη.