{X} (s : merely X -> X) : Collapsible X. Proof. refine (Build_Collapsible _ (s o tr) _); intros x y. apply (ap s), path_ishprop. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions Factorization. Require Import Truncations.Core Modalities.Modality.