{X} {Y : HSet} (f : X -> Y) : IsInjective f -> sig (ran f) = X. Proof. intros Hf. apply path_universe_uncurried. srapply equiv_adjointify. - intros [y H]. destruct (iota (fun x => f x = y) _) as [x Hx]; try exact x. split; try apply H. intros x x'. cbn. intros Hy Hy'. rewrite <- Hy' in Hy. by apply Hf. - intros x. exists (f x). apply tr. exists x. reflexivity. - cbn. intros x. destruct iota as [x' H]. by apply Hf. - cbn. intros [y x]. apply path_sigma_hprop. cbn. destruct iota as [x' Hx]. apply Hx. 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.