{X Y : Type} (f : X -> Y) {Ys : IsHSet Y} {wc : WeaklyConstant f} (x : X) : merely_rec_hset f (tr x) = f x := idpath.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions Factorization. Require Import Truncations.Core Modalities.Modality.