Definition bin_hrel_is_z_iso_to_image {X Y : hSet} {r : bin_hrel X Y} (p : is_z_isomorphism (C := REL) r) : ∏ x : X, ∑ y : Y, r x y. Proof. intro x. set (q := pr12 p). set (q' := base_paths _ _ (!(eqtohomot ((eqtohomot q) x) x))). set (y := path_to_fun q' (idpath _)). use (factor_through_squash_hProp (_ ,, bin_hrel_is_z_iso_to_image_isaprop p x) _ y). intro v. exact (pr1 v ,, pr12 v). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Categories.HSET.All.