Coercion foo (n : nat) : Set.
Admitted.
Check (0 : Set).