Constructive proof that there are no surjections from {1} to {1,2}

no_surject_12.v

(* There are no surjections from {1} to {1,2} *)

Definition surjective {A B} (f : A -> B) := forall (b : B), exists (a : A), b = f a.

Definition One := unit.

Definition Two := bool.

Theorem no_surject_one_two : ~ exists (f : One -> Two), surjective f.
Proof.
  intros [f Hf].
  unfold surjective in Hf.
  destruct (f tt) eqn:E.
  - pose proof (Hf false). destruct H as [[] Hf']. congruence.
  - pose proof (Hf true). destruct H as [[] Hf']. congruence.
Qed.