{X Y Z} (f : X -> Y + Z) : (forall x y, f x <> inl y) -> forall x, { z | inr z = f x }. Proof. intros Hf. enough (H : forall x a, a = f x -> {z : Z & inr z = f x}). - intros x. by apply (H x (f x)). - intros x a Hxa. specialize (Hf x). destruct (f x) as [y|z]. + apply Empty_rect. by apply (Hf y). + by exists z. Qed.
From HoTT Require Import TruncType ExcludedMiddle abstract_algebra. From HoTT Require Import Universes.Smallness. From HoTT Require Import Spaces.Nat.Core Spaces.Card. From HoTT Require Import Equiv.BiInv. From HoTT Require Import HIT.unique_choice. From HoTT.Sets Require Import Ordinals Hartogs Powers GCH AC.