{X : Type} (f : X -> X) {wc : WeaklyConstant f} : FixedBy f <~> merely X. Proof. apply equiv_iff_hprop. - intros [x p]; exact (tr x). - apply Trunc_rec; intros x. exists (f x). apply wconst. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions Factorization. Require Import Truncations.Core Modalities.Modality.