A Ghost at ω1

In the final chain of the countable powerset functor, we show that the set at
index In the final chain of the countable powerset functor, we show that the set at index ω1, regarded as a transition system, is not strongly extensional because it contains a "ghost" element that has no successor even though its component at each successor index is inhabited. The method, adapted from a construction of Forti and Honsell, also gives ghosts at larger ordinals in the final chain of other subfunctors of the powerset functor. This leads to a precise description of which sets in these final chains are strongly extensional.