{X} `{Collapsible X} : merely X -> X. Proof. refine (_ o (equiv_fix_merely collapse)^-1). apply pr1. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions Factorization. Require Import Truncations.Core Modalities.Modality.