(X : Type) (f : X -> X) (S : Splitting f) `{IsEmbedding (retract_sect S.1)} : forall x, Collapsible (f x = x). Proof. intros x. destruct S as [[A r s H] K]; simpl in *. assert (c1 : f x = x -> { a : A & s a = x }). { intros p; exists (r x). exact (K x @ p). } assert (c2 : { a : A & s a = x } -> f x = x). { intros [a q]. exact ((K x)^ @ ap (s o r) q^ @ ap s (H a) @ q). } exists (c2 o c1). apply wconst_through_hprop. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Constant. Require Import Truncations.Core Modalities.Modality. Require Import Homotopy.IdentitySystems.