{X : Type} {x : X} (z1 z2 : { z : X & merely (z = x) }) : merely (z1 = z2). Proof. destruct z1 as [z1 p1], z2 as [z2 p2]. strip_truncations. apply tr. apply path_sigma_hprop; cbn. exact (p1 @ p2^). Defined.
Require Import Basics. Require Import Types. Require Import Extensions. Require Import Factorization. Require Import Modalities.Descent. Require Import Truncations.Core Truncations.SeparatedTrunc.