proposition: Lemma path_ran {X} {Y : HSet} (f : X -> Y) : IsInjective f -> sig (ran f) = X.
proof: 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. now apply Hf. - intros x. exists (f x). apply tr. exists x. reflexivity. - cbn. intros x. destruct iota as [x' H]. now apply Hf. - cbn. intros [y x]. apply path_sigma_hprop. cbn. destruct iota as [x' Hx]. apply Hx. Qed.
imports: HoTT(TruncType ExcludedMiddle abstract_algebra) HoTT(PropResizing.PropResizing) HoTT(Spaces.Nat.Core Spaces.Card) HoTT(Equiv.BiInv) HoTT(HIT.unique_choice) HoTT.Sets(Ordinals Hartogs Powers GCH AC)