Take
c∈C initial. We need to find a
natural isomorphism η:Mor(c,−)≅⊥; ie, we need to choose an
η so that the
diagram
commutes for all
x,y and
f:x→y and where each
component is an
isomorphism.
Since
⋆ is a singleton
set ⋆={1}, there’s only one choice we can make for
η; namely,
ηa(φ:c→x)=1. This gives
isomorphisms because each mor-
set Mor(c,x) has
cardinality one, since
c is
initial. Futher, this makes the
diagram commute, essentially because
⋆ is a singleton.