{X : Type} (x : X) : { z : X & merely (z = x) } <~> image (Tr (-1)) (unit_name x). Proof. unfold image; simpl. apply equiv_functor_sigma_id; intros z; simpl. apply Trunc_functor_equiv; unfold hfiber. refine ((equiv_contr_sigma _)^-1 oE _). apply equiv_path_inverse. Defined.
Require Import Basics. Require Import Types. Require Import Extensions. Require Import Factorization. Require Import Modalities.Descent. Require Import Truncations.Core Truncations.SeparatedTrunc.