Non-Empty set from Contravariant.Adjuction use cases

[subttle]

Writing this idea down before I forget:
Data.Functor.Contravariant.Adjunction has an instance for Predicate Predicate, for which the unit (and also counit) which can be thought of, IIRC, as giving all the possible non-empty "sets" with respect to some unit element. I wonder if there is a way to use that in this library, for example in the synchronizing function below, I have a need for non empty sets. Would it make sense to use the aformention instance here or even perhaps other places?

-- Theorem (Cerny, 1964): A DFA M is (directable) synchronizing iff ∀q ∈ Q, ∃p ∈ Q, ∃w ∈ Σ★: δ(q, w) = δ(p, w)
-- That is, there exists a word w, such that evaluation of w from from any state, q, always ends up in the same state, p.
-- "A DFA is synchronizing if there exists a word that sends all states of the automaton to the same state." - https://arxiv.org/abs/1507.06070
synchronizing ∷ (Finite q, Finite s) ⇒                  DFA q s → Bool
synchronizing = not . isZero . power
          where power ∷ (Finite q) ⇒ DFA q s → DFA (Set q) s -- FIXME supposed to be a non-empty set -- TODO alter this to check for shortest path to get shortest reset word?
                power m@(DFA δ _ _) = DFA { delta = \(states, σ) → map (\q → δ (q, σ)) states
                                          , q0    = qs m
                                          , fs    = map singleton (qs m)
                                          }

The other place I think it could potentially be useful is in the next variant of the co-inductive automata, PA/NA. Will have to look into it.