Morphisms work out — Given an
∫F-
morphism h:(c,x)→(d,y) we have that
S(α)(h)=h:(c,αc(x))→(d,αd(y)). Since we are mapping into a
category of elements then for this to be a
morphism it must
satisfy the
morphism requirements; namely, we need that
G(S(α)(h))(αc(x))=αd(y), which holds as follows:
G(S(α)(h))(αc(x))=G(h)(αc(x))=αd(F(h)(x))=αd(y)naturality of αh is a ∫F-morphism