Require Import HoTT.Basics HoTT.Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import HFiber Constant.
Require Import Truncations.Core Modalities.Modality.
Require Import Homotopy.IdentitySystems.

Local Open Scope nat_scope.
Local Open Scope path_scope.

Local Set Universe Minimization ToSet.

(** * Idempotents and their splittings *)

(** ** Basic definitions *)

(** *** Retracts *)

(** A *retract* of a type [X] is a type [A] equipped with a pair of morphisms [r : X -> A] and [s : A -> X] such that the composite [r o s] is the identity of [A]. *)

Record RetractOf {X : Type} :=
  { retract_type : Type ;
    retract_retr : X -> retract_type ;
    retract_sect : retract_type -> X ;
    retract_issect : retract_retr o retract_sect == idmap }.

Arguments RetractOf X : clear implicits.

Arguments retract_type / .
Arguments retract_retr / .
Arguments retract_sect / .
Arguments retract_issect / .

(** For example, here is the identity retraction. *)
Definition idmap_retractof (X : Type) : RetractOf X
  := Build_RetractOf X X idmap idmap (fun _ => 1).

(** Retractions can be composed with equivalences on either side. *)
Definition retractof_equiv {X Y : Type} (f : X -> Y) `{feq : IsEquiv _ _ f}
: RetractOf X -> RetractOf Y.
X, Y: Type
f: X -> Y
feq: IsEquiv f
RetractOf X -> RetractOf Y
Proof.
X, Y: Type
f: X -> Y
feq: IsEquiv f
RetractOf X -> RetractOf Y
  intros [A r s H]; refine (Build_RetractOf Y A (r o f^-1) (f o s) _); intros x.
X, Y: Type
f: X -> Y
feq: IsEquiv f
A: Type
r: X -> A
s: A -> X
H: (fun x : A => r (s x)) == idmap
x: A
r (f^-1 (f (s x))) = x
  exact (ap r (eissect f (s x)) @ H x).
Defined.

Definition retractof_equiv' {X Y : Type} (f : X <~> Y)
: RetractOf X -> RetractOf Y
  := retractof_equiv f.

Definition equiv_retractof {X : Type} (R : RetractOf X)
           {B : Type} (f : retract_type R -> B) `{feq : IsEquiv _ _ f}
: RetractOf X.
X: Type
R: RetractOf X
B: Type
f: retract_type R -> B
feq: IsEquiv f
RetractOf X
Proof.
X: Type
R: RetractOf X
B: Type
f: retract_type R -> B
feq: IsEquiv f
RetractOf X
  destruct R as [A r s H]; refine (Build_RetractOf X B (f o r) (s o f^-1) _); intros x.
X, A: Type
r: X -> A
s: A -> X
H: (fun x : A => r (s x)) == idmap
B: Type
f: retract_type
  {|
    retract_type := A;
    retract_retr := r;
    retract_sect := s;
    retract_issect := H
  |} -> B
feq: IsEquiv f
x: B
f (r (s (f^-1 x))) = x
  exact (ap f (H (f^-1 x)) @ eisretr f x).
Defined.

Definition equiv_retractof' {X : Type} (R : RetractOf X)
           {B : Type} (f : retract_type R <~> B)
: RetractOf X
  := equiv_retractof R f.

(** A commuting retract of the domain of map induces a retract of its fibers. *)
Definition retractof_hfiber {X Y : Type} (R : RetractOf X) (f : X -> Y)
           (g : retract_type R -> Y) (p : g o retract_retr R == f)
           (y : Y)
: RetractOf (hfiber f y).
X, Y: Type
R: RetractOf X
f: X -> Y
g: retract_type R -> Y
p: g o retract_retr R == f
y: Y
RetractOf (hfiber f y)
Proof.
X, Y: Type
R: RetractOf X
f: X -> Y
g: retract_type R -> Y
p: g o retract_retr R == f
y: Y
RetractOf (hfiber f y)
  destruct R as [A r s H]; simpl in *.
X, Y, A: Type
r: X -> A
s: A -> X
H: (fun x : A => r (s x)) == idmap
f: X -> Y
g: A -> Y
p: (fun x : X => g (r x)) == f
y: Y
RetractOf (hfiber f y)
  simple refine (Build_RetractOf (hfiber f y) (hfiber g y) _ _ _).
X, Y, A: Type
r: X -> A
s: A -> X
H: (fun x : A => r (s x)) == idmap
f: X -> Y
g: A -> Y
p: (fun x : X => g (r x)) == f
y: Y
hfiber f y -> hfiber g y
X, Y, A: Type
r: X -> A
s: A -> X
H: (fun x : A => r (s x)) == idmap
f: X -> Y
g: A -> Y
p: (fun x : X => g (r x)) == f
y: Y
hfiber g y -> hfiber f y
X, Y, A: Type
r: X -> A
s: A -> X
H: (fun x : A => r (s x)) == idmap
f: X -> Y
g: A -> Y
p: (fun x : X => g (r x)) == f
y: Y
?retract_retr o ?retract_sect == idmap
  -
X, Y, A: Type
r: X -> A
s: A -> X
H: (fun x : A => r (s x)) == idmap
f: X -> Y
g: A -> Y
p: (fun x : X => g (r x)) == f
y: Y
hfiber f y -> hfiber g y intros [x q].
X, Y, A: Type
r: X -> A
s: A -> X
H: (fun x : A => r (s x)) == idmap
f: X -> Y
g: A -> Y
p: (fun x : X => g (r x)) == f
y: Y
x: X
q: f x = y
hfiber g y
    exists (r x).
X, Y, A: Type
r: X -> A
s: A -> X
H: (fun x : A => r (s x)) == idmap
f: X -> Y
g: A -> Y
p: (fun x : X => g (r x)) == f
y: Y
x: X
q: f x = y
g (r x) = y
    exact (p x @ q).
  -
X, Y, A: Type
r: X -> A
s: A -> X
H: (fun x : A => r (s x)) == idmap
f: X -> Y
g: A -> Y
p: (fun x : X => g (r x)) == f
y: Y
hfiber g y -> hfiber f y intros [a q].
X, Y, A: Type
r: X -> A
s: A -> X
H: (fun x : A => r (s x)) == idmap
f: X -> Y
g: A -> Y
p: (fun x : X => g (r x)) == f
y: Y
a: A
q: g a = y
hfiber f y
    exists (s a).
X, Y, A: Type
r: X -> A
s: A -> X
H: (fun x : A => r (s x)) == idmap
f: X -> Y
g: A -> Y
p: (fun x : X => g (r x)) == f
y: Y
a: A
q: g a = y
f (s a) = y
    exact ((p (s a))^ @ ap g (H a) @ q).
  -
X, Y, A: Type
r: X -> A
s: A -> X
H: (fun x : A => r (s x)) == idmap
f: X -> Y
g: A -> Y
p: (fun x : X => g (r x)) == f
y: Y
(fun X0 : hfiber f y =>
 (fun (x : X) (q : f x = y) => (r x; p x @ q)) X0.1
   X0.2)
o (fun X0 : hfiber g y =>
   (fun (a : A) (q : g a = y) =>
    (s a; ((p (s a))^ @ ap g (H a)) @ q)) X0.1 X0.2) ==
idmap intros [a q].
X, Y, A: Type
r: X -> A
s: A -> X
H: (fun x : A => r (s x)) == idmap
f: X -> Y
g: A -> Y
p: (fun x : X => g (r x)) == f
y: Y
a: A
q: g a = y
(r (s a); p (s a) @ (((p (s a))^ @ ap g (H a)) @ q)) =
(a; q)
    simple refine (path_sigma' _ _ _).
X, Y, A: Type
r: X -> A
s: A -> X
H: (fun x : A => r (s x)) == idmap
f: X -> Y
g: A -> Y
p: (fun x : X => g (r x)) == f
y: Y
a: A
q: g a = y
r (s a) = a
X, Y, A: Type
r: X -> A
s: A -> X
H: (fun x : A => r (s x)) == idmap
f: X -> Y
g: A -> Y
p: (fun x : X => g (r x)) == f
y: Y
a: A
q: g a = y
transport (fun x : A => g x = y) ?p
  (p (s a) @ (((p (s a))^ @ ap g (H a)) @ q)) = q
    +
X, Y, A: Type
r: X -> A
s: A -> X
H: (fun x : A => r (s x)) == idmap
f: X -> Y
g: A -> Y
p: (fun x : X => g (r x)) == f
y: Y
a: A
q: g a = y
r (s a) = a exact (H a).
    +
X, Y, A: Type
r: X -> A
s: A -> X
H: (fun x : A => r (s x)) == idmap
f: X -> Y
g: A -> Y
p: (fun x : X => g (r x)) == f
y: Y
a: A
q: g a = y
transport (fun x : A => g x = y) (H a)
  (p (s a) @ (((p (s a))^ @ ap g (H a)) @ q)) = q abstract (
        rewrite transport_paths_Fl, !concat_p_pp, concat_pp_V, concat_Vp, concat_1p;
        reflexivity).
Defined.

(** Retraction preserves contractibility **)
Definition contr_retracttype {X : Type} (R : RetractOf X ) (contra : Contr X) : Contr (retract_type R )
  := contr_retract (retract_retr R) (retract_sect R) (retract_issect R).

(** Like any record type, [RetractOf X] is equivalent to a nested sigma-type.  We use a product at one place in the middle, rather than a sigma, to simplify the next proof. *)
Definition issig_retractof (X : Type)
: { A : Type & {r : X -> A & {s : A -> X & r o s == idmap }}}
  <~> RetractOf X.
X: Type
{A : Type &
{r : X -> A & {s : A -> X & r o s == idmap}}} <~>
RetractOf X
Proof.
X: Type
{A : Type &
{r : X -> A & {s : A -> X & r o s == idmap}}} <~>
RetractOf X
  issig.
Defined.

(* Path spaces of types of retractions *)
Definition PathRetractOf (X : Type) (R' R : RetractOf X)
  := { Ap : retract_type R' <~> retract_type R &
     { rp : Ap o retract_retr R' == retract_retr R &
     { sp : retract_sect R' o Ap^-1 == retract_sect R &
            forall a, ap Ap (retract_issect R' (Ap^-1 a))
                         @ eisretr Ap a
                      = rp (retract_sect R' (Ap^-1 a))
                           @ ap (retract_retr R) (sp a)
                           @ retract_issect R a } } }.

Definition equiv_path_retractof `{ua : Univalence} {X : Type}
           (R' R : RetractOf X)
  : PathRetractOf X R' R <~> R' = R.
ua: Univalence
X: Type
R', R: RetractOf X
PathRetractOf X R' R <~> R' = R
Proof.
ua: Univalence
X: Type
R', R: RetractOf X
PathRetractOf X R' R <~> R' = R
  revert R' R; apply (equiv_path_issig_contr (issig_retractof X)).
ua: Univalence
X: Type
forall
b : {A : Type &
    {r : X -> A &
    {s : A -> X & (fun x : A => r (s x)) == idmap}}},
PathRetractOf X (issig_retractof X b)
  (issig_retractof X b)
ua: Univalence
X: Type
forall
b1 : {A : Type &
     {r : X -> A &
     {s : A -> X & (fun x : A => r (s x)) == idmap}}},
Contr
  {b2
  : {A : Type &
    {r : X -> A &
    {s : A -> X & (fun x : A => r (s x)) == idmap}}} &
  PathRetractOf X (issig_retractof X b1)
    (issig_retractof X b2)}
  {
ua: Univalence
X: Type
forall
b : {A : Type &
    {r : X -> A &
    {s : A -> X & (fun x : A => r (s x)) == idmap}}},
PathRetractOf X (issig_retractof X b)
  (issig_retractof X b) intros [A [r [s H]]]; cbn.
ua: Univalence
X, A: Type
r: X -> A
s: A -> X
H: (fun x : A => r (s x)) == idmap
PathRetractOf X
  {|
    retract_type := A;
    retract_retr := r;
    retract_sect := s;
    retract_issect := H
  |}
  {|
    retract_type := A;
    retract_retr := r;
    retract_sect := s;
    retract_issect := H
  |}
    exists equiv_idmap.
ua: Univalence
X, A: Type
r: X -> A
s: A -> X
H: (fun x : A => r (s x)) == idmap
{rp
: (fun x : X =>
   1%equiv
     (retract_retr
        {|
          retract_type := A;
          retract_retr := r;
          retract_sect := s;
          retract_issect := H
        |} x)) ==
  retract_retr
    {|
      retract_type := A;
      retract_retr := r;
      retract_sect := s;
      retract_issect := H
    |} &
{sp
: (fun
     x : retract_type
           {|
             retract_type := A;
             retract_retr := r;
             retract_sect := s;
             retract_issect := H
           |} =>
   retract_sect
     {|
       retract_type := A;
       retract_retr := r;
       retract_sect := s;
       retract_issect := H
     |} ((1%equiv)^-1 x)) ==
  retract_sect
    {|
      retract_type := A;
      retract_retr := r;
      retract_sect := s;
      retract_issect := H
    |} &
forall
a : retract_type
      {|
        retract_type := A;
        retract_retr := r;
        retract_sect := s;
        retract_issect := H
      |},
ap 1%equiv
  (retract_issect
     {|
       retract_type := A;
       retract_retr := r;
       retract_sect := s;
       retract_issect := H
     |} ((1%equiv)^-1 a)) @ eisretr 1%equiv a =
(rp
   (retract_sect
      {|
        retract_type := A;
        retract_retr := r;
        retract_sect := s;
        retract_issect := H
      |} ((1%equiv)^-1 a)) @
 ap
   (retract_retr
      {|
        retract_type := A;
        retract_retr := r;
        retract_sect := s;
        retract_issect := H
      |}) (sp a)) @
retract_issect
  {|
    retract_type := A;
    retract_retr := r;
    retract_sect := s;
    retract_issect := H
  |} a}}
    exists (fun x => 1%path).
ua: Univalence
X, A: Type
r: X -> A
s: A -> X
H: (fun x : A => r (s x)) == idmap
{sp
: (fun
     x : retract_type
           {|
             retract_type := A;
             retract_retr := r;
             retract_sect := s;
             retract_issect := H
           |} =>
   retract_sect
     {|
       retract_type := A;
       retract_retr := r;
       retract_sect := s;
       retract_issect := H
     |} ((1%equiv)^-1 x)) ==
  retract_sect
    {|
      retract_type := A;
      retract_retr := r;
      retract_sect := s;
      retract_issect := H
    |} &
forall
a : retract_type
      {|
        retract_type := A;
        retract_retr := r;
        retract_sect := s;
        retract_issect := H
      |},
ap 1%equiv
  (retract_issect
     {|
       retract_type := A;
       retract_retr := r;
       retract_sect := s;
       retract_issect := H
     |} ((1%equiv)^-1 a)) @ eisretr 1%equiv a =
(1 @
 ap
   (retract_retr
      {|
        retract_type := A;
        retract_retr := r;
        retract_sect := s;
        retract_issect := H
      |}) (sp a)) @
retract_issect
  {|
    retract_type := A;
    retract_retr := r;
    retract_sect := s;
    retract_issect := H
  |} a}
    exists (fun x => 1%path).
ua: Univalence
X, A: Type
r: X -> A
s: A -> X
H: (fun x : A => r (s x)) == idmap
forall
a : retract_type
      {|
        retract_type := A;
        retract_retr := r;
        retract_sect := s;
        retract_issect := H
      |},
ap 1%equiv
  (retract_issect
     {|
       retract_type := A;
       retract_retr := r;
       retract_sect := s;
       retract_issect := H
     |} ((1%equiv)^-1 a)) @ eisretr 1%equiv a =
(1 @
 ap
   (retract_retr
      {|
        retract_type := A;
        retract_retr := r;
        retract_sect := s;
        retract_issect := H
      |}) 1) @
retract_issect
  {|
    retract_type := A;
    retract_retr := r;
    retract_sect := s;
    retract_issect := H
  |} a
    cbn.
ua: Univalence
X, A: Type
r: X -> A
s: A -> X
H: (fun x : A => r (s x)) == idmap
forall a : A, ap idmap (H a) @ 1 = 1 @ H a exact (fun a => equiv_p1_1q (ap_idmap (H a))). }
ua: Univalence
X: Type
forall
b1 : {A : Type &
     {r : X -> A &
     {s : A -> X & (fun x : A => r (s x)) == idmap}}},
Contr
  {b2
  : {A : Type &
    {r : X -> A &
    {s : A -> X & (fun x : A => r (s x)) == idmap}}} &
  PathRetractOf X (issig_retractof X b1)
    (issig_retractof X b2)}
  intros [A [r [s H]]]; cbn.
ua: Univalence
X, A: Type
r: X -> A
s: A -> X
H: (fun x : A => r (s x)) == idmap
Contr
  {b2
  : {A : Type &
    {r : X -> A &
    {s : A -> X & (fun x : A => r (s x)) == idmap}}} &
  PathRetractOf X
    {|
      retract_type := A;
      retract_retr := r;
      retract_sect := s;
      retract_issect := H
    |}
    {|
      retract_type := b2.1;
      retract_retr := (b2.2).1;
      retract_sect := ((b2.2).2).1;
      retract_issect := ((b2.2).2).2
    |}}
  unfold PathRetractOf.
ua: Univalence
X, A: Type
r: X -> A
s: A -> X
H: (fun x : A => r (s x)) == idmap
Contr
  {b2
  : {A : Type &
    {r : X -> A &
    {s : A -> X & (fun x : A => r (s x)) == idmap}}} &
  {Ap
  : retract_type
      {|
        retract_type := A;
        retract_retr := r;
        retract_sect := s;
        retract_issect := H
      |} <~>
    retract_type
      {|
        retract_type := b2.1;
        retract_retr := (b2.2).1;
        retract_sect := ((b2.2).2).1;
        retract_issect := ((b2.2).2).2
      |} &
  {rp
  : (fun x : X =>
     Ap
       (retract_retr
          {|
            retract_type := A;
            retract_retr := r;
            retract_sect := s;
            retract_issect := H
          |} x)) ==
    retract_retr
      {|
        retract_type := b2.1;
        retract_retr := (b2.2).1;
        retract_sect := ((b2.2).2).1;
        retract_issect := ((b2.2).2).2
      |} &
  {sp
  : (fun
       x : retract_type
             {|
               retract_type := b2.1;
               retract_retr := (b2.2).1;
               retract_sect := ((b2.2).2).1;
               retract_issect := ((b2.2).2).2
             |} =>
     retract_sect
       {|
         retract_type := A;
         retract_retr := r;
         retract_sect := s;
         retract_issect := H
       |} (Ap^-1 x)) ==
    retract_sect
      {|
        retract_type := b2.1;
        retract_retr := (b2.2).1;
        retract_sect := ((b2.2).2).1;
        retract_issect := ((b2.2).2).2
      |} &
  forall
  a : retract_type
        {|
          retract_type := b2.1;
          retract_retr := (b2.2).1;
          retract_sect := ((b2.2).2).1;
          retract_issect := ((b2.2).2).2
        |},
  ap Ap
    (retract_issect
       {|
         retract_type := A;
         retract_retr := r;
         retract_sect := s;
         retract_issect := H
       |} (Ap^-1 a)) @ eisretr Ap a =
  (rp
     (retract_sect
        {|
          retract_type := A;
          retract_retr := r;
          retract_sect := s;
          retract_issect := H
        |} (Ap^-1 a)) @
   ap
     (retract_retr
        {|
          retract_type := b2.1;
          retract_retr := (b2.2).1;
          retract_sect := ((b2.2).2).1;
          retract_issect := ((b2.2).2).2
        |}) (sp a)) @
  retract_issect
    {|
      retract_type := b2.1;
      retract_retr := (b2.2).1;
      retract_sect := ((b2.2).2).1;
      retract_issect := ((b2.2).2).2
    |} a}}}}
  contr_sigsig A (equiv_idmap A); cbn.
ua: Univalence
X, A: Type
r: X -> A
s: A -> X
H: (fun x : A => r (s x)) == idmap
Contr
  {y
  : {r : X -> A &
    {s : A -> X & (fun x : A => r (s x)) == idmap}} &
  {rp : (fun x : X => r x) == y.1 &
  {sp : (fun x : A => s x) == (y.2).1 &
  forall a : A,
  ap idmap (H a) @ 1 =
  (rp (s a) @ ap y.1 (sp a)) @ (y.2).2 a}}}
  contr_sigsig r (fun x:X => idpath (r x)); cbn.
ua: Univalence
X, A: Type
r: X -> A
s: A -> X
H: (fun x : A => r (s x)) == idmap
Contr
  {y : {s : A -> X & (fun x : A => r (s x)) == idmap}
  &
  {sp : (fun x : A => s x) == y.1 &
  forall a : A,
  ap idmap (H a) @ 1 = (1 @ ap r (sp a)) @ y.2 a}}
  contr_sigsig s (fun x:A => idpath (s x)); cbn.
ua: Univalence
X, A: Type
r: X -> A
s: A -> X
H: (fun x : A => r (s x)) == idmap
Contr
  {y : (fun x : A => r (s x)) == idmap &
  forall a : A, ap idmap (H a) @ 1 = 1 @ y a}
  refine (contr_equiv' {K : r o s == idmap & H == K} _).
ua: Univalence
X, A: Type
r: X -> A
s: A -> X
H: (fun x : A => r (s x)) == idmap
{K : (fun x : A => r (s x)) == idmap & H == K} <~>
{y : (fun x : A => r (s x)) == idmap &
forall a : A, ap idmap (H a) @ 1 = 1 @ y a}
  apply equiv_functor_sigma_id; intros K.
ua: Univalence
X, A: Type
r: X -> A
s: A -> X
H, K: (fun x : A => r (s x)) == idmap
H == K <~>
(forall a : A, ap idmap (H a) @ 1 = 1 @ K a)
  apply equiv_functor_forall_id; intros a; cbn.
ua: Univalence
X, A: Type
r: X -> A
s: A -> X
H, K: (fun x : A => r (s x)) == idmap
a: A
H a = K a <~> ap idmap (H a) @ 1 = 1 @ K a
  apply equiv_concat_lr.
ua: Univalence
X, A: Type
r: X -> A
s: A -> X
H, K: (fun x : A => r (s x)) == idmap
a: A
ap idmap (H a) @ 1 = H a
ua: Univalence
X, A: Type
r: X -> A
s: A -> X
H, K: (fun x : A => r (s x)) == idmap
a: A
K a = 1 @ K a
  -
ua: Univalence
X, A: Type
r: X -> A
s: A -> X
H, K: (fun x : A => r (s x)) == idmap
a: A
ap idmap (H a) @ 1 = H a exact (concat_p1 _ @ ap_idmap (H a)).
  -
ua: Univalence
X, A: Type
r: X -> A
s: A -> X
H, K: (fun x : A => r (s x)) == idmap
a: A
K a = 1 @ K a symmetry; apply concat_1p.
Defined.

Definition path_retractof `{ua : Univalence} {X : Type} {R' R : RetractOf X}
           Ap rp sp Hp
  : R' = R
  := equiv_path_retractof R' R (Ap;rp;sp;Hp).

(** *** Splittings *)

(** If an endomap [f : X -> X] arises from a retract as [s o r], we say that that retract is a *splitting* of [f]. *)

Definition retract_idem {X : Type} (R : RetractOf X)
: (X -> X)
  := retract_sect R o retract_retr R.

Arguments retract_idem {_} _ / x .

Definition Splitting {X : Type} (f : X -> X)
  := { R : RetractOf X & retract_idem R == f}.

(** For example, here is the canonical splitting of the identity. *)
Definition splitting_idmap (X : Type) : @Splitting X idmap
  := (idmap_retractof X ; fun _ => 1).

(** *** Pre-idempotents *)

(** An "idempotent" is a map that at least "ought" to be splittable.  The naive definition of idempotent, which is correct in set-level mathematics, is a morphism [f : X -> X] such that [forall x, f (f x) = f x].  We will call this a "pre-idempotent". *)

Class IsPreIdempotent {X : Type} (f : X -> X)
  := isidem : forall x, f (f x) = f x.

Arguments isidem {X} f {_} x.

Definition ispreidem_homotopic {X : Type}
           (f : X -> X) `{IsPreIdempotent _ f} {g : X -> X} (p : f == g)
: IsPreIdempotent g.
X: Type
f: X -> X
H: IsPreIdempotent f
g: X -> X
p: f == g
IsPreIdempotent g
Proof.
X: Type
f: X -> X
H: IsPreIdempotent f
g: X -> X
p: f == g
IsPreIdempotent g
  intros x; refine (_ @ isidem f x @ p x).
X: Type
f: X -> X
H: IsPreIdempotent f
g: X -> X
p: f == g
x: X
g (g x) = f (f x)
  refine (_ @ (p (f x))^).
X: Type
f: X -> X
H: IsPreIdempotent f
g: X -> X
p: f == g
x: X
g (g x) = g (f x)
  apply ap; symmetry; apply p.
Defined.

Arguments ispreidem_homotopic / .

Definition PreIdempotent (X : Type) := { f : X -> X & IsPreIdempotent f }.
Definition preidempotent_pr1 {X : Type} : PreIdempotent X -> X -> X := pr1.
Coercion preidempotent_pr1 : PreIdempotent >-> Funclass.

Instance ispreidem_preidem {X : Type} (f : PreIdempotent X)
: IsPreIdempotent f
  := f.2.

(** The identity function has a canonical structure of a pre-idempotent. *)
Instance ispreidem_idmap (X : Type) : @IsPreIdempotent X idmap
  := fun _ => 1.

Definition preidem_idmap (X : Type) : PreIdempotent X.
X: Type
PreIdempotent X
Proof.
X: Type
PreIdempotent X
  exists idmap; exact _.
Defined.

(** Any pre-idempotent on a set splits. *)
Definition split_preidem_set (X : Type) `{IsHSet X} (f : PreIdempotent X)
: Splitting f.
X: Type
IsHSet0: IsHSet X
f: PreIdempotent X
Splitting f
Proof.
X: Type
IsHSet0: IsHSet X
f: PreIdempotent X
Splitting f
  simple refine (Build_RetractOf X { x : X & f x = x }
                                 (fun x => (f x ; isidem f x)) pr1 _ ; _).
X: Type
IsHSet0: IsHSet X
f: PreIdempotent X
(fun x : X => (f x; isidem f x)) o pr1 == idmap
X: Type
IsHSet0: IsHSet X
f: PreIdempotent X
(fun R : RetractOf X => retract_idem R == f)
  {|
    retract_type := {x : X & f x = x};
    retract_retr := fun x : X => (f x; isidem f x);
    retract_sect := pr1;
    retract_issect := ?retract_issect
  |}
  -
X: Type
IsHSet0: IsHSet X
f: PreIdempotent X
(fun x : X => (f x; isidem f x)) o pr1 == idmap intros [x p]; simpl.
X: Type
IsHSet0: IsHSet X
f: PreIdempotent X
x: X
p: f x = x
(f x; isidem f x) = (x; p)
    apply path_sigma with p; simpl.
X: Type
IsHSet0: IsHSet X
f: PreIdempotent X
x: X
p: f x = x
transport (fun x : X => f x = x) p (isidem f x) = p
    apply path_ishprop.
  -
X: Type
IsHSet0: IsHSet X
f: PreIdempotent X
(fun R : RetractOf X => retract_idem R == f)
  {|
    retract_type := {x : X & f x = x};
    retract_retr := fun x : X => (f x; isidem f x);
    retract_sect := pr1;
    retract_issect :=
      (fun x0 : {x : X & f x = x} =>
       (fun (x : X) (p : f x = x) =>
        path_sigma (fun x1 : X => f x1 = x1)
          (f x; isidem f x) (x; p) p
          (path_ishprop
             (transport (fun x1 : X => f x1 = x1) p
                (isidem f x)) p
           :
           transport (fun x1 : X => f x1 = x1) p
             (f x; isidem f x).2 = (x; p).2)
        :
        (f (x; p).1; isidem f (x; p).1) = (x; p)) x0.1
         x0.2)
      :
      (fun x : X => (f x; isidem f x)) o pr1 == idmap
  |} simpl.
X: Type
IsHSet0: IsHSet X
f: PreIdempotent X
(fun x : X => f x) == f intros x; reflexivity.
Defined.

(** Any weakly constant pre-idempotent splits (Escardó) *)
Definition split_preidem_wconst (X : Type) (f : PreIdempotent X)
           `{WeaklyConstant _ _ f}
: Splitting f.
X: Type
f: PreIdempotent X
H: WeaklyConstant f
Splitting f
Proof.
X: Type
f: PreIdempotent X
H: WeaklyConstant f
Splitting f
  simple refine (Build_RetractOf X (FixedBy f)
                                 (fun x => (f x ; isidem f x)) pr1 _ ; _).
X: Type
f: PreIdempotent X
H: WeaklyConstant f
(fun x : X => (f x; isidem f x)) o pr1 == idmap
X: Type
f: PreIdempotent X
H: WeaklyConstant f
(fun R : RetractOf X => retract_idem R == f)
  {|
    retract_type := FixedBy f;
    retract_retr := fun x : X => (f x; isidem f x);
    retract_sect := pr1;
    retract_issect := ?retract_issect
  |}
  -
X: Type
f: PreIdempotent X
H: WeaklyConstant f
(fun x : X => (f x; isidem f x)) o pr1 == idmap intros x; apply path_ishprop.
  -
X: Type
f: PreIdempotent X
H: WeaklyConstant f
(fun R : RetractOf X => retract_idem R == f)
  {|
    retract_type := FixedBy f;
    retract_retr := fun x : X => (f x; isidem f x);
    retract_sect := pr1;
    retract_issect :=
      (fun x : FixedBy f =>
       path_ishprop (f x.1; isidem f x.1) x)
      :
      (fun x : X => (f x; isidem f x)) o pr1 == idmap
  |} simpl.
X: Type
f: PreIdempotent X
H: WeaklyConstant f
(fun x : X => f x) == f intros x; reflexivity.
Defined.

(** If [f] is pre-idempotent and [f x = x] is collapsible for all [x], then [f] splits (Escardó). *)
Definition split_preidem_splitsupp (X : Type) (f : PreIdempotent X)
           (ss : forall x, Collapsible (f x = x))
: Splitting f.
X: Type
f: PreIdempotent X
ss: forall x : X, Collapsible (f x = x)
Splitting f
Proof.
X: Type
f: PreIdempotent X
ss: forall x : X, Collapsible (f x = x)
Splitting f
  simple refine (Build_RetractOf X { x : X & FixedBy (@collapse (f x = x) _) }
                                 _ pr1 _ ; _).
X: Type
f: PreIdempotent X
ss: forall x : X, Collapsible (f x = x)
X -> {x : X & FixedBy collapse}
X: Type
f: PreIdempotent X
ss: forall x : X, Collapsible (f x = x)
?retract_retr o pr1 == idmap
X: Type
f: PreIdempotent X
ss: forall x : X, Collapsible (f x = x)
(fun R : RetractOf X => retract_idem R == f)
  {|
    retract_type := {x : X & FixedBy collapse};
    retract_retr := ?retract_retr;
    retract_sect := pr1;
    retract_issect := ?retract_issect
  |}
  -
X: Type
f: PreIdempotent X
ss: forall x : X, Collapsible (f x = x)
X -> {x : X & FixedBy collapse} intros x; exists (f x); unfold FixedBy.
X: Type
f: PreIdempotent X
ss: forall x : X, Collapsible (f x = x)
x: X
{x0 : f (f x) = f x & collapse x0 = x0}
    exists (collapse (isidem f x)).
X: Type
f: PreIdempotent X
ss: forall x : X, Collapsible (f x = x)
x: X
collapse (collapse (isidem f x)) =
collapse (isidem f x)
    apply wconst.
  -
X: Type
f: PreIdempotent X
ss: forall x : X, Collapsible (f x = x)
(fun x : X =>
 (f x;
 (collapse (isidem f x);
 wconst (collapse (isidem f x)) (isidem f x))
 :
 FixedBy collapse)) o pr1 == idmap intros [x [p q]]; simpl.
X: Type
f: PreIdempotent X
ss: forall x : X, Collapsible (f x = x)
x: X
p: f x = x
q: collapse p = p
(f x; collapse (isidem f x);
wconst (collapse (isidem f x)) (isidem f x)) =
(x; p; q)
    apply path_sigma with p.
X: Type
f: PreIdempotent X
ss: forall x : X, Collapsible (f x = x)
x: X
p: f x = x
q: collapse p = p
transport (fun x : X => FixedBy collapse) p
  (f x; collapse (isidem f x);
  wconst (collapse (isidem f x)) (isidem f x)).2 =
(x; p; q).2
    apply path_ishprop.
  -
X: Type
f: PreIdempotent X
ss: forall x : X, Collapsible (f x = x)
(fun R : RetractOf X => retract_idem R == f)
  {|
    retract_type := {x : X & FixedBy collapse};
    retract_retr :=
      fun x : X =>
      (f x;
      (collapse (isidem f x);
      wconst (collapse (isidem f x)) (isidem f x))
      :
      FixedBy collapse);
    retract_sect := pr1;
    retract_issect :=
      (fun x0 : {x : X & FixedBy collapse} =>
       (fun (x : X) (proj2 : FixedBy collapse) =>
        (fun (p : f x = x) (q : collapse p = p) =>
         path_sigma (fun x1 : X => FixedBy collapse)
           (f x; collapse (isidem f x);
           wconst (collapse (isidem f x)) (isidem f x))
           (x; p; q) p
           (path_ishprop
              (transport
                 (fun x1 : X => FixedBy collapse) p
                 (f x; collapse (isidem f x);
                 wconst (collapse (isidem f x))
                   (isidem f x)).2) (x; p; q).2)
         :
         (f (x; p; q).1;
         collapse (isidem f (x; p; q).1);
         wconst (collapse (isidem f (x; p; q).1))
           (isidem f (x; p; q).1)) = (x; p; q))
          proj2.1 proj2.2) x0.1 x0.2)
      :
      (fun x : X =>
       (f x;
       (collapse (isidem f x);
       wconst (collapse (isidem f x)) (isidem f x))
       :
       FixedBy collapse)) o pr1 == idmap
  |} simpl.
X: Type
f: PreIdempotent X
ss: forall x : X, Collapsible (f x = x)
(fun x : X => f x) == f intros x; reflexivity.
Defined.

(** Moreover, in this case the section is an embedding. *)
Definition isemb_split_preidem_splitsupp (X : Type) (f : PreIdempotent X)
           (ss : forall x, Collapsible (f x = x))
: IsEmbedding (retract_sect (split_preidem_splitsupp X f ss).1).
X: Type
f: PreIdempotent X
ss: forall x : X, Collapsible (f x = x)
IsEmbedding
  (retract_sect (split_preidem_splitsupp X f ss).1)
Proof.
X: Type
f: PreIdempotent X
ss: forall x : X, Collapsible (f x = x)
IsEmbedding
  (retract_sect (split_preidem_splitsupp X f ss).1)
  apply istruncmap_mapinO_tr; exact _.
Defined.

(** Conversely, if [f] splits with a section that is an embedding, then (it is pre-idempotent and) [f x = x] is collapsible for all [x] (Escardó). *)
Definition splitsupp_split_isemb (X : Type) (f : X -> X) (S : Splitting f)
           `{IsEmbedding (retract_sect S.1)}
: forall x, Collapsible (f x = x).
X: Type
f: X -> X
S: Splitting f
IsEmbedding0: IsEmbedding (retract_sect S.1)
forall x : X, Collapsible (f x = x)
Proof.
X: Type
f: X -> X
S: Splitting f
IsEmbedding0: IsEmbedding (retract_sect S.1)
forall x : X, Collapsible (f x = x)
  intros x.
X: Type
f: X -> X
S: Splitting f
IsEmbedding0: IsEmbedding (retract_sect S.1)
x: X
Collapsible (f x = x) destruct S as [[A r s H] K]; simpl in *.
X: Type
f: X -> X
A: Type
r: X -> A
s: A -> X
H: (fun x : A => r (s x)) == idmap
K: (fun x : X => s (r x)) == f
IsEmbedding0: IsEmbedding s
x: X
Collapsible (f x = x)
  assert (c1 : f x = x -> { a : A & s a = x }).
X: Type
f: X -> X
A: Type
r: X -> A
s: A -> X
H: (fun x : A => r (s x)) == idmap
K: (fun x : X => s (r x)) == f
IsEmbedding0: IsEmbedding s
x: X
f x = x -> {a : A & s a = x}
X: Type
f: X -> X
A: Type
r: X -> A
s: A -> X
H: (fun x : A => r (s x)) == idmap
K: (fun x : X => s (r x)) == f
IsEmbedding0: IsEmbedding s
x: X
c1: f x = x -> {a : A & s a = x}
Collapsible (f x = x)
  {
X: Type
f: X -> X
A: Type
r: X -> A
s: A -> X
H: (fun x : A => r (s x)) == idmap
K: (fun x : X => s (r x)) == f
IsEmbedding0: IsEmbedding s
x: X
f x = x -> {a : A & s a = x} intros p; exists (r x).
X: Type
f: X -> X
A: Type
r: X -> A
s: A -> X
H: (fun x : A => r (s x)) == idmap
K: (fun x : X => s (r x)) == f
IsEmbedding0: IsEmbedding s
x: X
p: f x = x
s (r x) = x
    exact (K x @ p). }
X: Type
f: X -> X
A: Type
r: X -> A
s: A -> X
H: (fun x : A => r (s x)) == idmap
K: (fun x : X => s (r x)) == f
IsEmbedding0: IsEmbedding s
x: X
c1: f x = x -> {a : A & s a = x}
Collapsible (f x = x)
  assert (c2 : { a : A & s a = x } -> f x = x).
X: Type
f: X -> X
A: Type
r: X -> A
s: A -> X
H: (fun x : A => r (s x)) == idmap
K: (fun x : X => s (r x)) == f
IsEmbedding0: IsEmbedding s
x: X
c1: f x = x -> {a : A & s a = x}
{a : A & s a = x} -> f x = x
X: Type
f: X -> X
A: Type
r: X -> A
s: A -> X
H: (fun x : A => r (s x)) == idmap
K: (fun x : X => s (r x)) == f
IsEmbedding0: IsEmbedding s
x: X
c1: f x = x -> {a : A & s a = x}
c2: {a : A & s a = x} -> f x = x
Collapsible (f x = x)
  {
X: Type
f: X -> X
A: Type
r: X -> A
s: A -> X
H: (fun x : A => r (s x)) == idmap
K: (fun x : X => s (r x)) == f
IsEmbedding0: IsEmbedding s
x: X
c1: f x = x -> {a : A & s a = x}
{a : A & s a = x} -> f x = x intros [a q].
X: Type
f: X -> X
A: Type
r: X -> A
s: A -> X
H: (fun x : A => r (s x)) == idmap
K: (fun x : X => s (r x)) == f
IsEmbedding0: IsEmbedding s
x: X
c1: f x = x -> {a : A & s a = x}
a: A
q: s a = x
f x = x
    exact ((K x)^ @ ap (s o r) q^ @ ap s (H a) @ q). }
X: Type
f: X -> X
A: Type
r: X -> A
s: A -> X
H: (fun x : A => r (s x)) == idmap
K: (fun x : X => s (r x)) == f
IsEmbedding0: IsEmbedding s
x: X
c1: f x = x -> {a : A & s a = x}
c2: {a : A & s a = x} -> f x = x
Collapsible (f x = x)
  exists (c2 o c1).
X: Type
f: X -> X
A: Type
r: X -> A
s: A -> X
H: (fun x : A => r (s x)) == idmap
K: (fun x : X => s (r x)) == f
IsEmbedding0: IsEmbedding s
x: X
c1: f x = x -> {a : A & s a = x}
c2: {a : A & s a = x} -> f x = x
WeaklyConstant (fun x : f x = x => c2 (c1 x))
  apply wconst_through_hprop.
Defined.

(** *** Quasi-idempotents *)

(** However, homotopically we may naturally expect to need some coherence on the witness [isidem] of idempotency.  And indeed, in homotopy theory there are pre-idempotents which do not split; we will see an example later on.  We expect a "coherent idempotent" to involve infinitely many data.  However, Lemma 7.3.5.14 of *Higher Algebra* suggests that for an idempotent to admit *some* coherentification, hence also a splitting, it suffices to have *one* additional datum.  By modifying the construction given there, we can show similarly in type theory that any idempotent satisfying an additional coherence datum splits.  We will call a pre-idempotent with this one additional datum a "quasi-idempotent", since it is related to a fully coherent idempotent similarly to the way having a "quasi-inverse" is related to being a coherent equivalence. *)

Class IsQuasiIdempotent {X : Type} (f : X -> X) `{IsPreIdempotent _ f}
  := isidem2 : forall x, ap f (isidem f x) = isidem f (f x).

Arguments isidem2 {X} f {_ _} x.

Definition isqidem_homotopic {X : Type}
           (f : X -> X) `{IsQuasiIdempotent _ f} {g : X -> X} (p : f == g)
: @IsQuasiIdempotent X g (ispreidem_homotopic f p).
X: Type
f: X -> X
H: IsPreIdempotent f
H0: IsQuasiIdempotent f
g: X -> X
p: f == g
IsQuasiIdempotent g
Proof.
X: Type
f: X -> X
H: IsPreIdempotent f
H0: IsQuasiIdempotent f
g: X -> X
p: f == g
IsQuasiIdempotent g
  intros x; unfold isidem; simpl.
X: Type
f: X -> X
H: IsPreIdempotent f
H0: IsQuasiIdempotent f
g: X -> X
p: f == g
x: X
ap g (((ap g (p x)^ @ (p (f x))^) @ isidem f x) @ p x) =
((ap g (p (g x))^ @ (p (f (g x)))^) @ isidem f (g x)) @
p (g x)
  Open Scope long_path_scope.
X: Type
f: X -> X
H: IsPreIdempotent f
H0: IsQuasiIdempotent f
g: X -> X
p: f == g
x: X
ap g (ap g (p x)^
      @' (p (f x))^
      @' isidem f x
      @' p x) =
ap g (p (g x))^
@' (p (f (g x)))^
@' isidem f (g x)
@' p (g x)
  rewrite (concat_Ap (fun x => (p x)^) (p x)^).
X: Type
f: X -> X
H: IsPreIdempotent f
H0: IsQuasiIdempotent f
g: X -> X
p: f == g
x: X
ap g ((p (g x))^
      @' ap f (p x)^
      @' isidem f x
      @' p x) =
ap g (p (g x))^
@' (p (f (g x)))^
@' isidem f (g x)
@' p (g x)
  rewrite !ap_pp, !concat_pp_p; apply whiskerL.
X: Type
f: X -> X
H: IsPreIdempotent f
H0: IsQuasiIdempotent f
g: X -> X
p: f == g
x: X
ap g (ap f (p x)^)
@' (ap g (isidem f x)
    @' ap g (p x)) =
(p (f (g x)))^
@' (isidem f (g x)
    @' p (g x))
  rewrite !concat_p_pp; apply moveL_pM.
X: Type
f: X -> X
H: IsPreIdempotent f
H0: IsQuasiIdempotent f
g: X -> X
p: f == g
x: X
ap g (ap f (p x)^)
@' ap g (isidem f x)
@' ap g (p x)
@' (p (g x))^ = (p (f (g x)))^
                @' isidem f (g x)
  rewrite (concat_pA_p (fun x => (p x)^) (p x)).
X: Type
f: X -> X
H: IsPreIdempotent f
H0: IsQuasiIdempotent f
g: X -> X
p: f == g
x: X
ap g (ap f (p x)^)
@' ap g (isidem f x)
@' (p (f x))^
@' ap f (p x) = (p (f (g x)))^
                @' isidem f (g x)
  rewrite (concat_pA_p (fun x => (p x)^) (isidem _ x)).
X: Type
f: X -> X
H: IsPreIdempotent f
H0: IsQuasiIdempotent f
g: X -> X
p: f == g
x: X
ap g (ap f (p x)^)
@' (p (f (f x)))^
@' ap f (isidem f x)
@' ap f (p x) = (p (f (g x)))^
                @' isidem f (g x)
  rewrite (concat_Ap (fun x => (p x)^) (ap f (p x)^)).
X: Type
f: X -> X
H: IsPreIdempotent f
H0: IsQuasiIdempotent f
g: X -> X
p: f == g
x: X
(p (f (g x)))^
@' ap f (ap f (p x)^)
@' ap f (isidem f x)
@' ap f (p x) = (p (f (g x)))^
                @' isidem f (g x)
  rewrite !concat_pp_p; apply whiskerL.
X: Type
f: X -> X
H: IsPreIdempotent f
H0: IsQuasiIdempotent f
g: X -> X
p: f == g
x: X
ap f (ap f (p x)^)
@' (ap f (isidem f x)
    @' ap f (p x)) = isidem f (g x)
  rewrite !ap_V; apply moveR_Vp.
X: Type
f: X -> X
H: IsPreIdempotent f
H0: IsQuasiIdempotent f
g: X -> X
p: f == g
x: X
ap f (isidem f x)
@' ap f (p x) = ap f (ap f (p x))
                @' isidem f (g x)
  rewrite <- ap_compose.
X: Type
f: X -> X
H: IsPreIdempotent f
H0: IsQuasiIdempotent f
g: X -> X
p: f == g
x: X
ap f (isidem f x)
@' ap f (p x) =
ap (fun x : X => f (f x)) (p x)
@' isidem f (g x)
  rewrite isidem2; try exact _.
X: Type
f: X -> X
H: IsPreIdempotent f
H0: IsQuasiIdempotent f
g: X -> X
p: f == g
x: X
isidem f (f x)
@' ap f (p x) =
ap (fun x : X => f (f x)) (p x)
@' isidem f (g x)
  symmetry; exact (concat_Ap (isidem f) (p x)).
  Close Scope long_path_scope.
Qed.

Definition QuasiIdempotent (X : Type) := { f : PreIdempotent X & IsQuasiIdempotent f }.
Definition quasiidempotent_pr1 {X : Type} : QuasiIdempotent X -> X -> X := pr1.
Coercion quasiidempotent_pr1 : QuasiIdempotent >-> Funclass.

Instance isqidem_qidem {X : Type} (f : QuasiIdempotent X)
: IsQuasiIdempotent f
  := f.2.

(** The identity function has a canonical structure of a quasi-idempotent. *)
Instance isqidem_idmap (X : Type) : @IsQuasiIdempotent X idmap _
  := fun _ => 1.

Definition qidem_idmap (X : Type) : QuasiIdempotent X.
X: Type
QuasiIdempotent X
Proof.
X: Type
QuasiIdempotent X
  exists (preidem_idmap X); exact _.
Defined.

(** We have made [IsPreIdempotent] and [IsQuasiIdempotent] typeclasses as an experiment.  It could be that they should revert back to [Definitions]. *)

(** ** Split morphisms are quasi-idempotent *)

(** First we show that given a retract, the composite [s o r] is quasi-idempotent. *)

Instance ispreidem_retract {X : Type} (R : RetractOf X)
: IsPreIdempotent (retract_idem R).
X: Type
R: RetractOf X
IsPreIdempotent (retract_idem R)
Proof.
X: Type
R: RetractOf X
IsPreIdempotent (retract_idem R)
  exact (fun x => ap (retract_sect R) (retract_issect R (retract_retr R x))).
Defined.

Definition preidem_retract {X : Type} (R : RetractOf X)
: PreIdempotent X
:= (retract_idem R ; ispreidem_retract R).

Arguments ispreidem_retract / .
Arguments preidem_retract / .

Instance isqidem_retract {X : Type} (R : RetractOf X)
: IsQuasiIdempotent (retract_idem R).
X: Type
R: RetractOf X
IsQuasiIdempotent (retract_idem R)
Proof.
X: Type
R: RetractOf X
IsQuasiIdempotent (retract_idem R)
  destruct R as [A r s H]; intros x; unfold isidem; simpl.
X, A: Type
r: X -> A
s: A -> X
H: (fun x : A => r (s x)) == idmap
x: X
ap (fun x : X => s (r x)) (ap s (H (r x))) =
ap s (H (r (s (r x))))
  refine ((ap_compose _ _ _) @ _).
X, A: Type
r: X -> A
s: A -> X
H: (fun x : A => r (s x)) == idmap
x: X
ap s (ap r (ap s (H (r x)))) = ap s (H (r (s (r x))))
  apply ap.
X, A: Type
r: X -> A
s: A -> X
H: (fun x : A => r (s x)) == idmap
x: X
ap r (ap s (H (r x))) = H (r (s (r x)))
  refine ((ap_compose _ _ _)^ @ _).
X, A: Type
r: X -> A
s: A -> X
H: (fun x : A => r (s x)) == idmap
x: X
ap (fun x : A => r (s x)) (H (r x)) = H (r (s (r x)))
  refine (cancelR _ _ (H (r x)) _).
X, A: Type
r: X -> A
s: A -> X
H: (fun x : A => r (s x)) == idmap
x: X
ap (fun x : A => r (s x)) (H (r x)) @ H (r x) =
H (r (s (r x))) @ H (r x)
  refine (concat_A1p H (H (r x))).
Defined.

Definition qidem_retract {X : Type} (R : RetractOf X)
: QuasiIdempotent X
:= (preidem_retract R ; isqidem_retract R).

(** In particular, it follows that any split function is quasi-idempotent. *)

Instance ispreidem_split {X : Type} (f : X -> X) (S : Splitting f)
: IsPreIdempotent f.
X: Type
f: X -> X
S: Splitting f
IsPreIdempotent f
Proof.
X: Type
f: X -> X
S: Splitting f
IsPreIdempotent f
  destruct S as [R p].
X: Type
f: X -> X
R: RetractOf X
p: retract_idem R == f
IsPreIdempotent f
  exact (ispreidem_homotopic _ p).
Defined.

Arguments ispreidem_split / .

Instance isqidem_split {X : Type} (f : X -> X) (S : Splitting f)
: @IsQuasiIdempotent X f (ispreidem_split f S).
X: Type
f: X -> X
S: Splitting f
IsQuasiIdempotent f
Proof.
X: Type
f: X -> X
S: Splitting f
IsQuasiIdempotent f
  destruct S as [R p].
X: Type
f: X -> X
R: RetractOf X
p: retract_idem R == f
IsQuasiIdempotent f
  exact (isqidem_homotopic _ p).
Defined.

Arguments isqidem_split / .

(** ** Quasi-idempotents split *)

(** We now show the converse, that every quasi-idempotent splits. *)

Section Splitting.
  (** We need funext because our construction will involve a sequential limit.  We could probably also use a HIT sequential colimit, which is more like what Lurie does.  (Note that, like an interval type, HIT sequential colimits probably imply funext, so our construction uses strictly weaker hypotheses.) *)
  Context `{Funext}.
  Context {X : Type} (f : X -> X).
  Context `{IsQuasiIdempotent _ f}.

  Let I := isidem f.
  Let J : forall x, ap f (I x) = I (f x)
    := isidem2 f.

  (** The splitting will be the sequential limit of the sequence [... -> X -> X -> X]. *)
  Definition split_idem : Type
    := { a : nat -> X & forall n, f (a n.+1) = a n }.

  Definition split_idem_pr1 : split_idem -> (nat -> X)
    := pr1.
  Coercion split_idem_pr1 : split_idem >-> Funclass.
  Arguments split_idem_pr1 / .

  (** The section, retraction, and the fact that the composite in one direction is [f] are easy. *)

  Definition split_idem_sect : split_idem -> X
    := fun a => a 0.
  Arguments split_idem_sect / .

  Definition split_idem_retr : X -> split_idem.
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
X -> split_idem
  Proof.
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
X -> split_idem
    intros x.
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
x: X
split_idem
    exists (fun n => f x).
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
x: X
nat -> f (f x) = f x
    exact (fun n => I x).
  Defined.
  Arguments split_idem_retr / .

  Definition split_idem_splits (x : X)
  : split_idem_sect (split_idem_retr x) = f x
    := 1.

  (** What remains is to show that the composite in the other direction is the identity.  We begin by showing how to construct paths in [split_idem]. *)

  Definition path_split_idem {a a' : split_idem}
    (p : a.1 == a'.1)
    (q : forall n, a.2 n @ p n = ap f (p n.+1) @ a'.2 n)
  : a = a'.
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a, a': split_idem
p: a.1 == a'.1
q: forall n : nat,
a.2 n @ p n = ap f (p n.+1) @ a'.2 n
a = a'
  Proof.
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a, a': split_idem
p: a.1 == a'.1
q: forall n : nat,
a.2 n @ p n = ap f (p n.+1) @ a'.2 n
a = a'
    simple refine (path_sigma' _ _ _).
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a, a': split_idem
p: a.1 == a'.1
q: forall n : nat,
a.2 n @ p n = ap f (p n.+1) @ a'.2 n
a.1 = a'.1
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a, a': split_idem
p: a.1 == a'.1
q: forall n : nat,
a.2 n @ p n = ap f (p n.+1) @ a'.2 n
transport
  (fun a : nat -> X =>
   forall n : nat, f (a n.+1) = a n) ?p a.2 = a'.2
    -
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a, a': split_idem
p: a.1 == a'.1
q: forall n : nat,
a.2 n @ p n = ap f (p n.+1) @ a'.2 n
a.1 = a'.1 apply path_arrow; intros n.
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a, a': split_idem
p: a.1 == a'.1
q: forall n : nat,
a.2 n @ p n = ap f (p n.+1) @ a'.2 n
n: nat
a.1 n = a'.1 n
      exact (p n).
    -
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a, a': split_idem
p: a.1 == a'.1
q: forall n : nat,
a.2 n @ p n = ap f (p n.+1) @ a'.2 n
transport
  (fun a : nat -> X =>
   forall n : nat, f (a n.+1) = a n)
  (path_arrow a.1 a'.1
     ((fun n : nat => p n) : a.1 == a'.1)) a.2 = a'.2 apply path_forall; intros n.
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a, a': split_idem
p: a.1 == a'.1
q: forall n : nat,
a.2 n @ p n = ap f (p n.+1) @ a'.2 n
n: nat
transport
  (fun a : nat -> X =>
   forall n : nat, f (a n.+1) = a n)
  (path_arrow a.1 a'.1 (fun n : nat => p n)) a.2 n =
a'.2 n
      abstract (
          rewrite transport_forall_constant;
          rewrite transport_paths_FlFr;
          rewrite ap_apply_l, ap10_path_arrow;
          rewrite (ap_compose (fun b => b n.+1) (fun x => f x) _);
          rewrite ap_apply_l, ap10_path_arrow;
          rewrite concat_pp_p;
          apply moveR_Vp; by symmetry ).
  Defined.

  (** And we verify how those paths compute under [split_idem_sect]. *)
  Definition sect_path_split_idem {a a' : split_idem}
    (p : a.1 == a'.1)
    (q : forall n, a.2 n @ p n = ap f (p n.+1) @ a'.2 n)
  : ap split_idem_sect (path_split_idem p q) = p 0.
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a, a': split_idem
p: a.1 == a'.1
q: forall n : nat,
a.2 n @ p n = ap f (p n.+1) @ a'.2 n
ap split_idem_sect (path_split_idem p q) = p 0
  Proof.
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a, a': split_idem
p: a.1 == a'.1
q: forall n : nat,
a.2 n @ p n = ap f (p n.+1) @ a'.2 n
ap split_idem_sect (path_split_idem p q) = p 0
    change (ap ((fun b => b 0) o pr1) (path_split_idem p q) = p 0).
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a, a': split_idem
p: a.1 == a'.1
q: forall n : nat,
a.2 n @ p n = ap f (p n.+1) @ a'.2 n
ap ((fun b : nat -> X => b 0) o pr1)
  (path_split_idem p q) = p 0
    refine (ap_compose pr1 (fun b => b 0) _ @ _).
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a, a': split_idem
p: a.1 == a'.1
q: forall n : nat,
a.2 n @ p n = ap f (p n.+1) @ a'.2 n
ap (fun b : nat -> X => b 0)
  (ap pr1 (path_split_idem p q)) = p 0
    refine (ap (ap (fun b => b 0)) (pr1_path_sigma _ _) @ _).
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a, a': split_idem
p: a.1 == a'.1
q: forall n : nat,
a.2 n @ p n = ap f (p n.+1) @ a'.2 n
ap (fun b : nat -> X => b 0)
  (path_arrow a.1 a'.1 (fun n : nat => p n)) = p 0
    refine (ap_apply_l _ 0 @ _).
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a, a': split_idem
p: a.1 == a'.1
q: forall n : nat,
a.2 n @ p n = ap f (p n.+1) @ a'.2 n
ap10 (path_arrow a.1 a'.1 (fun n : nat => p n)) 0 =
p 0
    apply ap10_path_arrow.
  Defined.

  (** Next we show that every element of [split_idem] can be nudged to an equivalent one in which all the elements of [X] occurring are double applications of [f]. *)

  Local Definition nudge (a : split_idem) : split_idem.
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a: split_idem
split_idem
  Proof.
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a: split_idem
split_idem
    exists (fun n => f (f (a (n.+1)))).
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a: split_idem
forall n : nat, f (f (f (a n.+2))) = f (f (a n.+1))
    exact (fun n => ap f (ap f (a.2 n.+1))).
  Defined.

  Local Definition nudge_eq a : nudge a = a.
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a: split_idem
nudge a = a
  Proof.
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a: split_idem
nudge a = a
    transparent assert (a' : split_idem).
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a: split_idem
split_idem
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a: split_idem
a':= ?Goal: split_idem
nudge a = a
    {
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a: split_idem
split_idem exists (fun n => f (a (n.+1))).
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a: split_idem
forall n : nat, f (f (a n.+2)) = f (a n.+1)
      exact (fun n => ap f (a.2 n.+1)). }
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a: split_idem
a':= (fun n : nat => f (a n.+1);
fun n : nat => ap f (a.2 n.+1)): split_idem
nudge a = a
    transitivity a'; simple refine (path_split_idem _ _); intros n; simpl.
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a: split_idem
a':= (fun n : nat => f (a n.+1);
fun n : nat => ap f (a.2 n.+1)): split_idem
n: nat
f (f (a.1 n.+1)) = f (a.1 n.+1)
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a: split_idem
a':= (fun n : nat => f (a n.+1);
fun n : nat => ap f (a.2 n.+1)): split_idem
n: nat
ap f (ap f (a.2 n.+1)) @ ?Goal =
ap f ?Goal@{n:=n.+1} @ ap f (a.2 n.+1)
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a: split_idem
a':= (fun n : nat => f (a n.+1);
fun n : nat => ap f (a.2 n.+1)): split_idem
n: nat
f (a.1 n.+1) = a.1 n
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a: split_idem
a':= (fun n : nat => f (a n.+1);
fun n : nat => ap f (a.2 n.+1)): split_idem
n: nat
ap f (a.2 n.+1) @ ?Goal1 =
ap f ?Goal1@{n:=n.+1} @ a.2 n
    -
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a: split_idem
a':= (fun n : nat => f (a n.+1);
fun n : nat => ap f (a.2 n.+1)): split_idem
n: nat
f (f (a.1 n.+1)) = f (a.1 n.+1) exact (I (a n.+1)).
    -
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a: split_idem
a':= (fun n : nat => f (a n.+1);
fun n : nat => ap f (a.2 n.+1)): split_idem
n: nat
ap f (ap f (a.2 n.+1)) @ I (a n.+1) =
ap f (I (a n.+2)) @ ap f (a.2 n.+1) exact ((ap_compose f f _ @@ 1)^
               @ concat_Ap I (a.2 n.+1)
               @ (J _ @@ 1)^).
    -
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a: split_idem
a':= (fun n : nat => f (a n.+1);
fun n : nat => ap f (a.2 n.+1)): split_idem
n: nat
f (a.1 n.+1) = a.1 n exact (a.2 n).
    -
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a: split_idem
a':= (fun n : nat => f (a n.+1);
fun n : nat => ap f (a.2 n.+1)): split_idem
n: nat
ap f (a.2 n.+1) @ a.2 n = ap f (a.2 n.+1) @ a.2 n reflexivity.
  Defined.

  (** Now we're ready to prove the final condition.  We prove the two arguments of [path_split_idem] separately, in order to make the first one transparent and the second opaque. *)

  Local Definition split_idem_issect_part1 (a : split_idem) (n : nat)
  : f (f (a n.+1)) = f (a 0).
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a: split_idem
n: nat
f (f (a n.+1)) = f (a 0)
  Proof.
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a: split_idem
n: nat
f (f (a n.+1)) = f (a 0)
    induction n as [|n IH].
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a: split_idem
f (f (a 1)) = f (a 0)
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a: split_idem
n: nat
IH: f (f (a n.+1)) = f (a 0)
f (f (a n.+2)) = f (a 0)
    -
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a: split_idem
f (f (a 1)) = f (a 0) exact (ap f (a.2 0)).
    -
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a: split_idem
n: nat
IH: f (f (a n.+1)) = f (a 0)
f (f (a n.+2)) = f (a 0) exact (ap f (a.2 n.+1) @ (I (a n.+1))^ @ IH).
  Defined.

  Local Definition split_idem_issect_part2 (a : split_idem) (n : nat)
  : ap f (ap f (a.2 n.+1)) @ split_idem_issect_part1 a n =
    ap f ((ap f (a.2 n.+1) @ (I (a.1 n.+1))^) @ split_idem_issect_part1 a n) @ I (a.1 0).
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a: split_idem
n: nat
ap f (ap f (a.2 n.+1)) @ split_idem_issect_part1 a n =
ap f
  ((ap f (a.2 n.+1) @ (I (a.1 n.+1))^) @
   split_idem_issect_part1 a n) @ I (a.1 0)
  Proof.
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a: split_idem
n: nat
ap f (ap f (a.2 n.+1)) @ split_idem_issect_part1 a n =
ap f
  ((ap f (a.2 n.+1) @ (I (a.1 n.+1))^) @
   split_idem_issect_part1 a n) @ I (a.1 0)
    induction n as [|n IH]; simpl.
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a: split_idem
ap f (ap f (a.2 1)) @ ap f (a.2 0) =
ap f ((ap f (a.2 1) @ (I (a.1 1))^) @ ap f (a.2 0)) @
I (a.1 0)
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a: split_idem
n: nat
IH: ap f (ap f (a.2 n.+1)) @
split_idem_issect_part1 a n =
ap f
  ((ap f (a.2 n.+1) @ (I (a.1 n.+1))^) @
   split_idem_issect_part1 a n) @ I (a.1 0)
ap f (ap f (a.2 n.+2)) @
((ap f (a.2 n.+1) @ (I (a.1 n.+1))^) @
 split_idem_issect_part1 a n) =
ap f
  ((ap f (a.2 n.+2) @ (I (a.1 n.+2))^) @
   ((ap f (a.2 n.+1) @ (I (a.1 n.+1))^) @
    split_idem_issect_part1 a n)) @ I (a.1 0)
    Open Scope long_path_scope.
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a: split_idem
ap f (ap f (a.2 1))
@' ap f (a.2 0) =
ap f (ap f (a.2 1)
      @' (I (a.1 1))^
      @' ap f (a.2 0))
@' I (a.1 0)
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a: split_idem
n: nat
IH: ap f (ap f (a.2 n.+1))
@' split_idem_issect_part1 a n =
ap f
  (ap f (a.2 n.+1)
   @' (I (a.1 n.+1))^
   @' split_idem_issect_part1 a n)
@' I (a.1 0)
ap f (ap f (a.2 n.+2))
@' (ap f (a.2 n.+1)
    @' (I (a.1 n.+1))^
    @' split_idem_issect_part1 a n) =
ap f
  (ap f (a.2 n.+2)
   @' (I (a.1 n.+2))^
   @' (ap f (a.2 n.+1)
       @' (I (a.1 n.+1))^
       @' split_idem_issect_part1 a n))
@' I (a.1 0)
    -
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a: split_idem
ap f (ap f (a.2 1))
@' ap f (a.2 0) =
ap f (ap f (a.2 1)
      @' (I (a.1 1))^
      @' ap f (a.2 0))
@' I (a.1 0) rewrite !ap_pp, ap_V, !concat_pp_p.
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a: split_idem
ap f (ap f (a.2 1))
@' ap f (a.2 0) =
ap f (ap f (a.2 1))
@' ((ap f (I (a.1 1)))^
    @' (ap f (ap f (a.2 0))
        @' I (a.1 0)))
      apply whiskerL, moveL_Vp.
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a: split_idem
ap f (I (a.1 1))
@' ap f (a.2 0) = ap f (ap f (a.2 0))
                  @' I (a.1 0)
      rewrite J.
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a: split_idem
I (f (a.1 1))
@' ap f (a.2 0) = ap f (ap f (a.2 0))
                  @' I (a.1 0)
      rewrite <- ap_compose; symmetry; apply (concat_Ap I).
    -
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a: split_idem
n: nat
IH: ap f (ap f (a.2 n.+1))
@' split_idem_issect_part1 a n =
ap f
  (ap f (a.2 n.+1)
   @' (I (a.1 n.+1))^
   @' split_idem_issect_part1 a n)
@' I (a.1 0)
ap f (ap f (a.2 n.+2))
@' (ap f (a.2 n.+1)
    @' (I (a.1 n.+1))^
    @' split_idem_issect_part1 a n) =
ap f
  (ap f (a.2 n.+2)
   @' (I (a.1 n.+2))^
   @' (ap f (a.2 n.+1)
       @' (I (a.1 n.+1))^
       @' split_idem_issect_part1 a n))
@' I (a.1 0) rewrite ap_pp.
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a: split_idem
n: nat
IH: ap f (ap f (a.2 n.+1))
@' split_idem_issect_part1 a n =
ap f
  (ap f (a.2 n.+1)
   @' (I (a.1 n.+1))^
   @' split_idem_issect_part1 a n)
@' I (a.1 0)
ap f (ap f (a.2 n.+2))
@' (ap f (a.2 n.+1)
    @' (I (a.1 n.+1))^
    @' split_idem_issect_part1 a n) =
ap f (ap f (a.2 n.+2)
      @' (I (a.1 n.+2))^)
@' ap f
     (ap f (a.2 n.+1)
      @' (I (a.1 n.+1))^
      @' split_idem_issect_part1 a n)
@' I (a.1 0)
      refine (_ @ (1 @@ IH) @ concat_p_pp _ _ _).
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a: split_idem
n: nat
IH: ap f (ap f (a.2 n.+1))
@' split_idem_issect_part1 a n =
ap f
  (ap f (a.2 n.+1)
   @' (I (a.1 n.+1))^
   @' split_idem_issect_part1 a n)
@' I (a.1 0)
ap f (ap f (a.2 n.+2))
@' (ap f (a.2 n.+1)
    @' (I (a.1 n.+1))^
    @' split_idem_issect_part1 a n) =
ap f (ap f (a.2 n.+2)
      @' (I (a.1 n.+2))^)
@' (ap f (ap f (a.2 n.+1))
    @' split_idem_issect_part1 a n)
      rewrite !ap_pp, !concat_p_pp, ap_V.
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a: split_idem
n: nat
IH: ap f (ap f (a.2 n.+1))
@' split_idem_issect_part1 a n =
ap f
  (ap f (a.2 n.+1)
   @' (I (a.1 n.+1))^
   @' split_idem_issect_part1 a n)
@' I (a.1 0)
ap f (ap f (a.2 n.+2))
@' ap f (a.2 n.+1)
@' (I (a.1 n.+1))^
@' split_idem_issect_part1 a n =
ap f (ap f (a.2 n.+2))
@' (ap f (I (a.1 n.+2)))^
@' ap f (ap f (a.2 n.+1))
@' split_idem_issect_part1 a n
      rewrite J.
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a: split_idem
n: nat
IH: ap f (ap f (a.2 n.+1))
@' split_idem_issect_part1 a n =
ap f
  (ap f (a.2 n.+1)
   @' (I (a.1 n.+1))^
   @' split_idem_issect_part1 a n)
@' I (a.1 0)
ap f (ap f (a.2 n.+2))
@' ap f (a.2 n.+1)
@' (I (a.1 n.+1))^
@' split_idem_issect_part1 a n =
ap f (ap f (a.2 n.+2))
@' (I (f (a.1 n.+2)))^
@' ap f (ap f (a.2 n.+1))
@' split_idem_issect_part1 a n
      rewrite <- !ap_compose.
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a: split_idem
n: nat
IH: ap f (ap f (a.2 n.+1))
@' split_idem_issect_part1 a n =
ap f
  (ap f (a.2 n.+1)
   @' (I (a.1 n.+1))^
   @' split_idem_issect_part1 a n)
@' I (a.1 0)
ap (fun x : X => f (f x)) (a.2 n.+2)
@' ap f (a.2 n.+1)
@' (I (a.1 n.+1))^
@' split_idem_issect_part1 a n =
ap (fun x : X => f (f x)) (a.2 n.+2)
@' (I (f (a.1 n.+2)))^
@' ap (fun x : X => f (f x)) (a.2 n.+1)
@' split_idem_issect_part1 a n
      refine ((concat_pA_p (fun x => (I x)^) _ _) @@ 1).
    Close Scope long_path_scope.
  Qed.

  Definition split_idem_issect (a : split_idem)
  : split_idem_retr (split_idem_sect a) = a.
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a: split_idem
split_idem_retr (split_idem_sect a) = a
  Proof.
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a: split_idem
split_idem_retr (split_idem_sect a) = a
    refine (_ @ nudge_eq a); symmetry.
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a: split_idem
nudge a = split_idem_retr (split_idem_sect a)
    simple refine (path_split_idem _ _).
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a: split_idem
(nudge a).1 == (split_idem_retr (split_idem_sect a)).1
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a: split_idem
forall n : nat,
(nudge a).2 n @ ?p n =
ap f (?p n.+1) @
(split_idem_retr (split_idem_sect a)).2 n
    -
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a: split_idem
(nudge a).1 == (split_idem_retr (split_idem_sect a)).1 exact (split_idem_issect_part1 a).
    -
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
a: split_idem
forall n : nat,
(nudge a).2 n @ split_idem_issect_part1 a n =
ap f (split_idem_issect_part1 a n.+1) @
(split_idem_retr (split_idem_sect a)).2 n exact (split_idem_issect_part2 a).
  Defined.

  Definition split_idem_retract : RetractOf X
    := Build_RetractOf
         X split_idem split_idem_retr split_idem_sect split_idem_issect.

  Definition split_idem_split : Splitting f
    := (split_idem_retract ; split_idem_splits).

  (** We end this section by showing that we can recover the witness [I] of pre-idempotence from the splitting. *)
  Definition split_idem_preidem (x : X)
  : ap split_idem_sect (split_idem_issect (split_idem_retr x))
    = I x.
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
x: X
ap split_idem_sect
  (split_idem_issect (split_idem_retr x)) = I x
  Proof.
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
x: X
ap split_idem_sect
  (split_idem_issect (split_idem_retr x)) = I x
    unfold split_idem_issect, nudge_eq.
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
x: X
ap split_idem_sect
  ((path_split_idem
      (split_idem_issect_part1 (split_idem_retr x))
      (split_idem_issect_part2 (split_idem_retr x)))^ @
   (path_split_idem
      (fun n : nat => I (split_idem_retr x n.+1))
      (fun n : nat =>
       ((ap_compose f f ((split_idem_retr x).2 n.+1) @@
         1)^ @
        concat_Ap I ((split_idem_retr x).2 n.+1)) @
       (J ((split_idem_retr x).1 n.+2) @@ 1)^) @
    path_split_idem
      (fun n : nat => (split_idem_retr x).2 n)
      (fun n : nat => 1))) = I x
    repeat (rewrite !ap_pp, ?ap_V, !sect_path_split_idem; simpl).
H: Funext
X: Type
f: X -> X
H0: IsPreIdempotent f
H1: IsQuasiIdempotent f
I:= isidem f: forall x : X, f (f x) = f x
J:= isidem2 f: forall x : X, ap f (I x) = I (f x)
x: X
(ap f (I x))^ @ (I (f x) @ I x) = I x
    apply moveR_Vp, whiskerR; symmetry; apply J.
  Qed.

  (** However, the particular witness [J] of quasi-idempotence can *not* in general be recovered from the splitting; we will mention a counterexample below.  This is analogous to how [eissect] and [eisretr] cannot both be recovered after [isequiv_adjointify]; one of them has to be modified. *)

End Splitting.

Definition split_idem_retract' `{fs : Funext} {X : Type}
: QuasiIdempotent X -> RetractOf X
:= fun f => split_idem_retract f.

Definition split_idem_split' `{fs : Funext} {X : Type}
           (f : QuasiIdempotent X)
: Splitting f
:= split_idem_split f.

(** ** Splitting already-split idempotents *)

(** In the other direction, suppose we are given a retract, we deduce from this a quasi-idempotent, and then split it by the above construction.  We will show that the resulting retract is equivalent to the original one, so that [RetractOf X] is itelf a retract of [QuasiIdempotent X]. *)

Section AlreadySplit.
  Context `{fs : Funext}.

  Context {X : Type} (R : RetractOf X).
  Let A := retract_type R.
  Let r := retract_retr R.
  Let s := retract_sect R.
  Let H := retract_issect R.

  (** We begin by constructing an equivalence between [split_idem (s o r)] and [A].  We want to make this equivalence transparent so that we can reason about it later.  In fact, we want to reason not only about the equivalence function and its inverse, but the section and retraction homotopies!  Therefore, instead of using [equiv_adjointify] we will give the coherence proof explicitly, so that we can control these homotopies.  However, we can (and should) make the coherence proof itself opaque.  Thus, we prove it first, and end it with [Qed].  *)
  Lemma equiv_split_idem_retract_isadj (a : split_idem (s o r))
  : H (r (s (r (split_idem_sect (s o r) a)))) @
      H (r (split_idem_sect (s o r) a)) =
    ap (r o split_idem_sect (s o r))
       (ap (split_idem_retr (s o r))
           (1 @
              ap (split_idem_sect (s o r))
              (split_idem_issect (s o r) a)) @
           split_idem_issect (s o r) a).
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: split_idem (s o r)
H (r (s (r (split_idem_sect (s o r) a)))) @
H (r (split_idem_sect (s o r) a)) =
ap (r o split_idem_sect (s o r))
  (ap (split_idem_retr (s o r))
     (1 @
      ap (split_idem_sect (s o r))
        (split_idem_issect (s o r) a)) @
   split_idem_issect (s o r) a)
  Proof.
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: split_idem (s o r)
H (r (s (r (split_idem_sect (s o r) a)))) @
H (r (split_idem_sect (s o r) a)) =
ap (r o split_idem_sect (s o r))
  (ap (split_idem_retr (s o r))
     (1 @
      ap (split_idem_sect (s o r))
        (split_idem_issect (s o r) a)) @
   split_idem_issect (s o r) a)
    rewrite ap_pp.
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: split_idem (s o r)
H
  (r
     (s (r (split_idem_sect (fun x : X => s (r x)) a)))) @
H (r (split_idem_sect (fun x : X => s (r x)) a)) =
ap
  (fun x : split_idem (fun x : X => s (r x)) =>
   r (split_idem_sect (fun x0 : X => s (r x0)) x))
  (ap (split_idem_retr (fun x : X => s (r x)))
     (1 @
      ap (split_idem_sect (fun x : X => s (r x)))
        (split_idem_issect (fun x : X => s (r x)) a))) @
ap
  (fun x : split_idem (fun x : X => s (r x)) =>
   r (split_idem_sect (fun x0 : X => s (r x0)) x))
  (split_idem_issect (fun x : X => s (r x)) a)
    rewrite <- ap_compose; simpl.
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: split_idem (s o r)
H
  (r
     (s (r (split_idem_sect (fun x : X => s (r x)) a)))) @
H (r (split_idem_sect (fun x : X => s (r x)) a)) =
ap (fun x : X => r (s (r x)))
  (1 @
   ap (split_idem_sect (fun x : X => s (r x)))
     (split_idem_issect (fun x : X => s (r x)) a)) @
ap
  (fun x : split_idem (fun x : X => s (r x)) =>
   r (split_idem_sect (fun x0 : X => s (r x0)) x))
  (split_idem_issect (fun x : X => s (r x)) a)
    rewrite concat_1p.
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: split_idem (s o r)
H
  (r
     (s (r (split_idem_sect (fun x : X => s (r x)) a)))) @
H (r (split_idem_sect (fun x : X => s (r x)) a)) =
ap (fun x : X => r (s (r x)))
  (ap (split_idem_sect (fun x : X => s (r x)))
     (split_idem_issect (fun x : X => s (r x)) a)) @
ap
  (fun x : split_idem (fun x : X => s (r x)) =>
   r (split_idem_sect (fun x0 : X => s (r x0)) x))
  (split_idem_issect (fun x : X => s (r x)) a)
    rewrite <- (ap_compose (split_idem_sect (s o r)) (r o s o r)
                           (split_idem_issect (s o r) a)).
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: split_idem (s o r)
H
  (r
     (s (r (split_idem_sect (fun x : X => s (r x)) a)))) @
H (r (split_idem_sect (fun x : X => s (r x)) a)) =
ap
  (fun x : split_idem (fun x : X => s (r x)) =>
   r
     (s
        (r
           (split_idem_sect (fun x0 : X => s (r x0)) x))))
  (split_idem_issect (fun x : X => s (r x)) a) @
ap
  (fun x : split_idem (fun x : X => s (r x)) =>
   r (split_idem_sect (fun x0 : X => s (r x0)) x))
  (split_idem_issect (fun x : X => s (r x)) a)
    rewrite (ap_compose _ (r o s o r) (split_idem_issect (s o r) a)).
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: split_idem (s o r)
H
  (r
     (s (r (split_idem_sect (fun x : X => s (r x)) a)))) @
H (r (split_idem_sect (fun x : X => s (r x)) a)) =
ap (fun x : X => r (s (r x)))
  (ap (split_idem_sect (fun x : X => s (r x)))
     (split_idem_issect (fun x : X => s (r x)) a)) @
ap
  (fun x : split_idem (fun x : X => s (r x)) =>
   r (split_idem_sect (fun x0 : X => s (r x0)) x))
  (split_idem_issect (fun x : X => s (r x)) a)
    rewrite (ap_compose _ r (split_idem_issect (s o r) a)).
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: split_idem (s o r)
H
  (r
     (s (r (split_idem_sect (fun x : X => s (r x)) a)))) @
H (r (split_idem_sect (fun x : X => s (r x)) a)) =
ap (fun x : X => r (s (r x)))
  (ap (split_idem_sect (fun x : X => s (r x)))
     (split_idem_issect (fun x : X => s (r x)) a)) @
ap r
  (ap (split_idem_sect (fun x : X => s (r x)))
     (split_idem_issect (fun x : X => s (r x)) a))
    unfold split_idem_issect, nudge_eq;
      repeat (rewrite !ap_pp, ?ap_V, !sect_path_split_idem; simpl).
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: split_idem (s o r)
H
  (r
     (s (r (split_idem_sect (fun x : X => s (r x)) a)))) @
H (r (split_idem_sect (fun x : X => s (r x)) a)) =
((ap (fun x : X => r (s (r x)))
    (ap (fun x : X => s (r x)) (a.2 0)))^ @
 (ap (fun x : X => r (s (r x)))
    (isidem (fun x : X => s (r x)) (a 1)) @
  ap (fun x : X => r (s (r x))) (a.2 0))) @
((ap r (ap (fun x : X => s (r x)) (a.2 0)))^ @
 (ap r (isidem (fun x : X => s (r x)) (a 1)) @
  ap r (a.2 0)))
    unfold isidem; fold r s H.
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: split_idem (s o r)
H
  (r
     (s (r (split_idem_sect (fun x : X => s (r x)) a)))) @
H (r (split_idem_sect (fun x : X => s (r x)) a)) =
((ap (fun x : X => r (s (r x)))
    (ap (fun x : X => s (r x)) (a.2 0)))^ @
 (ap (fun x : X => r (s (r x))) (ap s (H (r (a 1)))) @
  ap (fun x : X => r (s (r x))) (a.2 0))) @
((ap r (ap (fun x : X => s (r x)) (a.2 0)))^ @
 (ap r (ap s (H (r (a 1)))) @ ap r (a.2 0)))
    rewrite !concat_pp_p.
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: split_idem (s o r)
H
  (r
     (s (r (split_idem_sect (fun x : X => s (r x)) a)))) @
H (r (split_idem_sect (fun x : X => s (r x)) a)) =
(ap (fun x : X => r (s (r x)))
   (ap (fun x : X => s (r x)) (a.2 0)))^ @
(ap (fun x : X => r (s (r x))) (ap s (H (r (a 1)))) @
 (ap (fun x : X => r (s (r x))) (a.2 0) @
  ((ap r (ap (fun x : X => s (r x)) (a.2 0)))^ @
   (ap r (ap s (H (r (a 1)))) @ ap r (a.2 0)))))
    rewrite <- !ap_compose.
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: split_idem (s o r)
H
  (r
     (s (r (split_idem_sect (fun x : X => s (r x)) a)))) @
H (r (split_idem_sect (fun x : X => s (r x)) a)) =
(ap (fun x : X => r (s (r x)))
   (ap (fun x : X => s (r x)) (a.2 0)))^ @
(ap (fun x : retract_type R => r (s (r (s x))))
   (H (r (a 1))) @
 (ap (fun x : X => r (s (r x))) (a.2 0) @
  ((ap r (ap (fun x : X => s (r x)) (a.2 0)))^ @
   (ap (fun x : retract_type R => r (s x))
      (H (r (a 1))) @ ap r (a.2 0)))))
    rewrite <- (ap_compose (s o r) r).
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: split_idem (s o r)
H
  (r
     (s (r (split_idem_sect (fun x : X => s (r x)) a)))) @
H (r (split_idem_sect (fun x : X => s (r x)) a)) =
(ap (fun x : X => r (s (r x)))
   (ap (fun x : X => s (r x)) (a.2 0)))^ @
(ap (fun x : retract_type R => r (s (r (s x))))
   (H (r (a 1))) @
 (ap (fun x : X => r (s (r x))) (a.2 0) @
  ((ap (fun x : X => r (s (r x))) (a.2 0))^ @
   (ap (fun x : retract_type R => r (s x))
      (H (r (a 1))) @ ap r (a.2 0)))))
    rewrite <- (ap_compose (s o r) (r o s o r)).
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: split_idem (s o r)
H
  (r
     (s (r (split_idem_sect (fun x : X => s (r x)) a)))) @
H (r (split_idem_sect (fun x : X => s (r x)) a)) =
(ap (fun x : X => r (s (r (s (r x))))) (a.2 0))^ @
(ap (fun x : retract_type R => r (s (r (s x))))
   (H (r (a 1))) @
 (ap (fun x : X => r (s (r x))) (a.2 0) @
  ((ap (fun x : X => r (s (r x))) (a.2 0))^ @
   (ap (fun x : retract_type R => r (s x))
      (H (r (a 1))) @ ap r (a.2 0)))))
    rewrite (concat_p_Vp (ap (r o s o r) (a.2 0))).
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: split_idem (s o r)
H
  (r
     (s (r (split_idem_sect (fun x : X => s (r x)) a)))) @
H (r (split_idem_sect (fun x : X => s (r x)) a)) =
(ap (fun x : X => r (s (r (s (r x))))) (a.2 0))^ @
(ap (fun x : retract_type R => r (s (r (s x))))
   (H (r (a 1))) @
 (ap (fun x : retract_type R => r (s x)) (H (r (a 1))) @
  ap r (a.2 0)))
    rewrite_moveL_Vp_p.
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: split_idem (s o r)
(ap (fun x : X => r (s (r (s (r x))))) (a.2 0) @
 H
   (r
      (s
         (r (split_idem_sect (fun x : X => s (r x)) a))))) @
H (r (split_idem_sect (fun x : X => s (r x)) a)) =
(ap (fun x : retract_type R => r (s (r (s x))))
   (H (r (a 1))) @
 ap (fun x : retract_type R => r (s x)) (H (r (a 1)))) @
ap r (a.2 0)
    rewrite (ap_compose (r o s o r) (r o s) (a.2 0)).
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: split_idem (s o r)
(ap (fun x : retract_type R => r (s x))
   (ap (fun x : X => r (s (r x))) (a.2 0)) @
 H
   (r
      (s
         (r (split_idem_sect (fun x : X => s (r x)) a))))) @
H (r (split_idem_sect (fun x : X => s (r x)) a)) =
(ap (fun x : retract_type R => r (s (r (s x))))
   (H (r (a 1))) @
 ap (fun x : retract_type R => r (s x)) (H (r (a 1)))) @
ap r (a.2 0)
    rewrite (concat_A1p H (ap (r o s o r) (a.2 0))).
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: split_idem (s o r)
(H (r (s (r (s (r (a.1 1)))))) @
 ap (fun x : X => r (s (r x))) (a.2 0)) @
H (r (split_idem_sect (fun x : X => s (r x)) a)) =
(ap (fun x : retract_type R => r (s (r (s x))))
   (H (r (a 1))) @
 ap (fun x : retract_type R => r (s x)) (H (r (a 1)))) @
ap r (a.2 0)
    rewrite (ap_compose r (r o s) (a.2 0)).
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: split_idem (s o r)
(H (r (s (r (s (r (a.1 1)))))) @
 ap (fun x : retract_type R => r (s x)) (ap r (a.2 0))) @
H (r (split_idem_sect (fun x : X => s (r x)) a)) =
(ap (fun x : retract_type R => r (s (r (s x))))
   (H (r (a 1))) @
 ap (fun x : retract_type R => r (s x)) (H (r (a 1)))) @
ap r (a.2 0)
    rewrite (concat_pA1_p H (ap r (a.2 0))).
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: split_idem (s o r)
(H (r (s (r (s (r (a.1 1)))))) @ H (r (s (r (a.1 1))))) @
ap r (a.2 0) =
(ap (fun x : retract_type R => r (s (r (s x))))
   (H (r (a 1))) @
 ap (fun x : retract_type R => r (s x)) (H (r (a 1)))) @
ap r (a.2 0)
    apply whiskerR.
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: split_idem (s o r)
H (r (s (r (s (r (a.1 1)))))) @ H (r (s (r (a.1 1)))) =
ap (fun x : retract_type R => r (s (r (s x))))
  (H (r (a 1))) @
ap (fun x : retract_type R => r (s x)) (H (r (a 1)))
    refine (cancelR _ _ (H (r (a.1 1%nat))) _).
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: split_idem (s o r)
(H (r (s (r (s (r (a.1 1)))))) @ H (r (s (r (a.1 1))))) @
H (r (a.1 1)) =
(ap (fun x : retract_type R => r (s (r (s x))))
   (H (r (a 1))) @
 ap (fun x : retract_type R => r (s x)) (H (r (a 1)))) @
H (r (a.1 1))
    rewrite (concat_pA1_p H (H (r (a 1%nat)))).
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: split_idem (s o r)
(H (r (s (r (s (r (a.1 1)))))) @ H (r (s (r (a.1 1))))) @
H (r (a.1 1)) =
(ap (fun x : retract_type R => r (s (r (s x))))
   (H (r (a 1))) @
 H (retract_retr R (retract_sect R (r (a 1))))) @
H (r (a 1))
    rewrite !concat_pp_p; symmetry; refine (_ @ concat_pp_p _ _ _).
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: split_idem (s o r)
ap (fun x : retract_type R => r (s (r (s x))))
  (H (r (a 1))) @
(H (retract_retr R (retract_sect R (r (a 1)))) @
 H (r (a 1))) =
(H (r (s (r (s (r (a.1 1)))))) @ H (r (s (r (a.1 1))))) @
H (r (a.1 1))
    exact (concat_A1p (fun x => H (r (s x)) @ H x) (H (r (a 1%nat)))).
  Qed.

  (** Now we can construct the desired equivalence. *)
  Definition equiv_split_idem_retract
  : split_idem (s o r) <~> A.
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
split_idem (s o r) <~> A
  Proof.
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
split_idem (s o r) <~> A
    simple refine (Build_Equiv _ _ (r o split_idem_sect (s o r))
              (Build_IsEquiv _ _ _ (split_idem_retr (s o r) o s) _ _ _)).
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
(fun x : split_idem (s o r) =>
 r (split_idem_sect (s o r) x))
o (split_idem_retr (s o r) o s) == idmap
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
split_idem_retr (s o r) o s
o (fun x : split_idem (s o r) =>
   r (split_idem_sect (s o r) x)) == idmap
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
forall x : split_idem (s o r),
?eisretr
  ((fun x0 : split_idem (s o r) =>
    r (split_idem_sect (s o r) x0)) x) =
ap
  (fun x0 : split_idem (s o r) =>
   r (split_idem_sect (s o r) x0)) (?eissect x)
    -
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
(fun x : split_idem (s o r) =>
 r (split_idem_sect (s o r) x))
o (split_idem_retr (s o r) o s) == idmap intros a; simpl.
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: retract_type R
r (s (r (s a))) = a
      exact (H _ @ H _).
    -
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
split_idem_retr (s o r) o s
o (fun x : split_idem (s o r) =>
   r (split_idem_sect (s o r) x)) == idmap intros a; simpl.
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: split_idem (fun x : X => s (r x))
split_idem_retr (fun x : X => s (r x))
  (s (r (split_idem_sect (fun x : X => s (r x)) a))) =
a
      refine (_ @ split_idem_issect (s o r) a).
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: split_idem (fun x : X => s (r x))
split_idem_retr (fun x : X => s (r x))
  (s (r (split_idem_sect (fun x : X => s (r x)) a))) =
split_idem_retr (fun x : X => s (r x))
  (split_idem_sect (fun x : X => s (r x)) a)
      apply ap.
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: split_idem (fun x : X => s (r x))
s (r (split_idem_sect (fun x : X => s (r x)) a)) =
split_idem_sect (fun x : X => s (r x)) a
      refine ((split_idem_splits (s o r) _)^ @ _).
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: split_idem (fun x : X => s (r x))
split_idem_sect (fun x : X => s (r x))
  (split_idem_retr (fun x : X => s (r x))
     (split_idem_sect (fun x : X => s (r x)) a)) =
split_idem_sect (fun x : X => s (r x)) a
      apply ap, split_idem_issect; exact _.
    -
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
forall x : split_idem (s o r),
((fun a : retract_type R =>
  H (retract_retr R (retract_sect R a)) @ H a
  :
  r
    (split_idem_sect (fun x0 : X => s (r x0))
       (split_idem_retr (fun x0 : X => s (r x0)) (s a))) =
  a)
 :
 (fun x0 : split_idem (s o r) =>
  r (split_idem_sect (s o r) x0))
 o (split_idem_retr (s o r) o s) == idmap)
  ((fun x0 : split_idem (s o r) =>
    r (split_idem_sect (s o r) x0)) x) =
ap
  (fun x0 : split_idem (s o r) =>
   r (split_idem_sect (s o r) x0))
  (((fun a : split_idem (fun x0 : X => s (r x0)) =>
     ap (split_idem_retr (fun x0 : X => s (r x0)))
       ((split_idem_splits (s o r)
           (split_idem_sect (fun x0 : X => s (r x0)) a))^ @
        ap (split_idem_sect (fun x0 : X => s (r x0)))
          (split_idem_issect (fun x0 : X => s (r x0))
             a)) @ split_idem_issect (s o r) a
     :
     split_idem_retr (fun x0 : X => s (r x0))
       (s
          (r
             (split_idem_sect (fun x0 : X => s (r x0))
                a))) = a)
    :
    split_idem_retr (s o r) o s
    o (fun x0 : split_idem (s o r) =>
       r (split_idem_sect (s o r) x0)) == idmap) x) intros a; simpl; apply equiv_split_idem_retract_isadj.
  Defined.

  (** It is easy to show that this equivalence respects the section and the retraction. *)

  Definition equiv_split_idem_retract_retr (x : X)
  : equiv_split_idem_retract (split_idem_retr (s o r) x) = r x
    := H (r x).

  Definition equiv_split_idem_retract_sect (a : A)
  : split_idem_sect (s o r) (equiv_split_idem_retract^-1 a) = s a
    := ap s (H a).

  (** Less trivial is to show that it respects the retract homotopy. *)

  Definition equiv_split_idem_retract_issect (a : A)
  : ap equiv_split_idem_retract
       (split_idem_issect (s o r) (equiv_split_idem_retract^-1 a))
       @ eisretr equiv_split_idem_retract a
    = equiv_split_idem_retract_retr
        (split_idem_sect (s o r) (equiv_split_idem_retract^-1 a))
        @ ap r (equiv_split_idem_retract_sect a)
        @ H a.
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: A
ap equiv_split_idem_retract
  (split_idem_issect (s o r)
     (equiv_split_idem_retract^-1 a)) @
eisretr equiv_split_idem_retract a =
(equiv_split_idem_retract_retr
   (split_idem_sect (s o r)
      (equiv_split_idem_retract^-1 a)) @
 ap r (equiv_split_idem_retract_sect a)) @ H a
  Proof.
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: A
ap equiv_split_idem_retract
  (split_idem_issect (s o r)
     (equiv_split_idem_retract^-1 a)) @
eisretr equiv_split_idem_retract a =
(equiv_split_idem_retract_retr
   (split_idem_sect (s o r)
      (equiv_split_idem_retract^-1 a)) @
 ap r (equiv_split_idem_retract_sect a)) @ H a
    simpl.
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: A
ap
  (fun x : split_idem (fun x : X => s (r x)) =>
   r (split_idem_sect (fun x0 : X => s (r x0)) x))
  (split_idem_issect (fun x : X => s (r x))
     (split_idem_retr (fun x : X => s (r x)) (s a))) @
(H (retract_retr R (retract_sect R a)) @ H a) =
(equiv_split_idem_retract_retr (s (r (s a))) @
 ap r (equiv_split_idem_retract_sect a)) @ H a
    unfold equiv_split_idem_retract_retr, equiv_split_idem_retract_sect.
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: A
ap
  (fun x : split_idem (fun x : X => s (r x)) =>
   r (split_idem_sect (fun x0 : X => s (r x0)) x))
  (split_idem_issect (fun x : X => s (r x))
     (split_idem_retr (fun x : X => s (r x)) (s a))) @
(H (retract_retr R (retract_sect R a)) @ H a) =
(H (r (s (r (s a)))) @ ap r (ap s (H a))) @ H a
    rewrite ap_compose.
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: A
ap r
  (ap (split_idem_sect (fun x : X => s (r x)))
     (split_idem_issect (fun x : X => s (r x))
        (split_idem_retr (fun x : X => s (r x)) (s a)))) @
(H (retract_retr R (retract_sect R a)) @ H a) =
(H (r (s (r (s a)))) @ ap r (ap s (H a))) @ H a
    unfold split_idem_issect, nudge_eq.
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: A
ap r
  (ap (split_idem_sect (fun x : X => s (r x)))
     ((path_split_idem (fun x : X => s (r x))
         (split_idem_issect_part1
            (fun x : X => s (r x))
            (split_idem_retr (fun x : X => s (r x))
               (s a)))
         (split_idem_issect_part2
            (fun x : X => s (r x))
            (split_idem_retr (fun x : X => s (r x))
               (s a))))^ @
      (path_split_idem (fun x : X => s (r x))
         (fun n : nat =>
          isidem (fun x : X => s (r x))
            (split_idem_retr (fun x : X => s (r x))
               (s a) n.+1))
         (fun n : nat =>
          ((ap_compose (fun x : X => s (r x))
              (fun x : X => s (r x))
              ((split_idem_retr (fun x : X => s (r x))
                  (s a)).2 n.+1) @@ 1)^ @
           concat_Ap (isidem (fun x : X => s (r x)))
             ((split_idem_retr (fun x : X => s (r x))
                 (s a)).2 n.+1)) @
          (isidem2 (fun x : X => s (r x))
             ((split_idem_retr (fun x : X => s (r x))
                 (s a)).1 n.+2) @@ 1)^) @
       path_split_idem (fun x : X => s (r x))
         (fun n : nat =>
          (split_idem_retr (fun x : X => s (r x))
             (s a)).2 n) (fun n : nat => 1)))) @
(H (retract_retr R (retract_sect R a)) @ H a) =
(H (r (s (r (s a)))) @ ap r (ap s (H a))) @ H a
    repeat (rewrite !ap_pp, ?ap_V, !sect_path_split_idem; simpl).
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: A
((ap r
    (ap (fun x : X => s (r x))
       (isidem (fun x : X => s (r x)) (s a))))^ @
 (ap r (isidem (fun x : X => s (r x)) (s (r (s a)))) @
  ap r (isidem (fun x : X => s (r x)) (s a)))) @
(H (retract_retr R (retract_sect R a)) @ H a) =
(H (r (s (r (s a)))) @ ap r (ap s (H a))) @ H a
    unfold isidem; fold A r s H.
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: A
((ap r
    (ap (fun x : X => s (r x)) (ap s (H (r (s a))))))^ @
 (ap r (ap s (H (r (s (r (s a)))))) @
  ap r (ap s (H (r (s a)))))) @ (H (r (s a)) @ H a) =
(H (r (s (r (s a)))) @ ap r (ap s (H a))) @ H a
    Open Scope long_path_scope.
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: A
(ap r (ap (fun x : X => s (r x)) (ap s (H (r (s a))))))^
@' (ap r (ap s (H (r (s (r (s a))))))
    @' ap r (ap s (H (r (s a)))))
@' (H (r (s a))
    @' H a) =
H (r (s (r (s a))))
@' ap r (ap s (H a))
@' H a
    rewrite !concat_pp_p; apply moveR_Vp; rewrite !concat_p_pp.
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: A
ap r (ap s (H (r (s (r (s a))))))
@' ap r (ap s (H (r (s a))))
@' H (r (s a))
@' H a =
ap r (ap (fun x : X => s (r x)) (ap s (H (r (s a)))))
@' H (r (s (r (s a))))
@' ap r (ap s (H a))
@' H a
    do 4 rewrite <- ap_compose.
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: A
ap (fun x : A => r (s x)) (H (r (s (r (s a)))))
@' ap (fun x : A => r (s x)) (H (r (s a)))
@' H (r (s a))
@' H a =
ap r (ap (fun x : A => s (r (s x))) (H (r (s a))))
@' H (r (s (r (s a))))
@' ap (fun x : A => r (s x)) (H a)
@' H a
    (** For some reason this last one needs help. *)
    rewrite <- (ap_compose (s o r o s) r (H (r (s a)))).
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: A
ap (fun x : A => r (s x)) (H (r (s (r (s a)))))
@' ap (fun x : A => r (s x)) (H (r (s a)))
@' H (r (s a))
@' H a =
ap (fun x : retract_type R => r (s (r (s x))))
  (H (r (s a)))
@' H (r (s (r (s a))))
@' ap (fun x : A => r (s x)) (H a)
@' H a
    rewrite <- (ap_pp (r o s) _ _).
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: A
ap (fun x : retract_type R => r (s x))
  (H (r (s (r (s a))))
   @' H (r (s a)))
@' H (r (s a))
@' H a =
ap (fun x : retract_type R => r (s (r (s x))))
  (H (r (s a)))
@' H (r (s (r (s a))))
@' ap (fun x : A => r (s x)) (H a)
@' H a
    rewrite <- (concat_A1p H (H (r (s a)))).
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: A
ap (fun x : retract_type R => r (s x))
  (ap
     (fun x : retract_type R =>
      retract_retr R (retract_sect R x)) (H (r (s a)))
   @' H (r (s a)))
@' H (r (s a))
@' H a =
ap (fun x : retract_type R => r (s (r (s x))))
  (H (r (s a)))
@' H (r (s (r (s a))))
@' ap (fun x : A => r (s x)) (H a)
@' H a
    rewrite ap_pp.
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: A
ap (fun x : retract_type R => r (s x))
  (ap
     (fun x : retract_type R =>
      retract_retr R (retract_sect R x)) (H (r (s a))))
@' ap (fun x : retract_type R => r (s x))
     (H (r (s a)))
@' H (r (s a))
@' H a =
ap (fun x : retract_type R => r (s (r (s x))))
  (H (r (s a)))
@' H (r (s (r (s a))))
@' ap (fun x : A => r (s x)) (H a)
@' H a
    rewrite <- (ap_compose (r o s) (r o s) _).
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: A
ap (fun x : retract_type R => r (s (r (s x))))
  (H (r (s a)))
@' ap (fun x : retract_type R => r (s x))
     (H (r (s a)))
@' H (r (s a))
@' H a =
ap (fun x : retract_type R => r (s (r (s x))))
  (H (r (s a)))
@' H (r (s (r (s a))))
@' ap (fun x : A => r (s x)) (H a)
@' H a
    rewrite !concat_pp_p; apply whiskerL; rewrite !concat_p_pp.
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: A
ap (fun x : retract_type R => r (s x)) (H (r (s a)))
@' H (r (s a))
@' H a =
H (r (s (r (s a))))
@' ap (fun x : A => r (s x)) (H a)
@' H a
    rewrite (concat_A1p H (H (r (s a)))).
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: A
H (retract_retr R (retract_sect R (r (s a))))
@' H (r (s a))
@' H a =
H (r (s (r (s a))))
@' ap (fun x : A => r (s x)) (H a)
@' H a
    rewrite !concat_pp_p; apply whiskerL.
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
a: A
H (r (s a))
@' H a = ap (fun x : A => r (s x)) (H a)
         @' H a
    symmetry; refine (concat_A1p H (H a)).
    Close Scope long_path_scope.
  Qed.

  (** We will also show that it respects the homotopy to the split map.  It's unclear whether this has any use. *)
  Definition equiv_split_idem_retract_splits (x : X)
  : split_idem_splits (s o r) x
    = ap (split_idem_sect (s o r))
         (eissect equiv_split_idem_retract
                  (split_idem_retr (s o r) x))^
      @ equiv_split_idem_retract_sect
        (equiv_split_idem_retract (split_idem_retr (s o r) x))
        @ ap s (equiv_split_idem_retract_retr x).
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
x: X
split_idem_splits (s o r) x =
(ap (split_idem_sect (s o r))
   (eissect equiv_split_idem_retract
      (split_idem_retr (s o r) x))^ @
 equiv_split_idem_retract_sect
   (equiv_split_idem_retract
      (split_idem_retr (s o r) x))) @
ap s (equiv_split_idem_retract_retr x)
  Proof.
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
x: X
split_idem_splits (s o r) x =
(ap (split_idem_sect (s o r))
   (eissect equiv_split_idem_retract
      (split_idem_retr (s o r) x))^ @
 equiv_split_idem_retract_sect
   (equiv_split_idem_retract
      (split_idem_retr (s o r) x))) @
ap s (equiv_split_idem_retract_retr x)
    simpl.
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
x: X
split_idem_splits (fun x : X => s (r x)) x =
(ap (split_idem_sect (fun x : X => s (r x)))
   (ap (split_idem_retr (fun x : X => s (r x)))
      (1 @
       ap (split_idem_sect (fun x : X => s (r x)))
         (split_idem_issect (fun x : X => s (r x))
            (split_idem_retr (fun x : X => s (r x)) x))) @
    split_idem_issect (fun x : X => s (r x))
      (split_idem_retr (fun x : X => s (r x)) x))^ @
 equiv_split_idem_retract_sect (r (s (r x)))) @
ap s (equiv_split_idem_retract_retr x)
    unfold equiv_split_idem_retract_retr, equiv_split_idem_retract_sect, split_idem_splits.
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
x: X
1 =
(ap (split_idem_sect (fun x : X => s (r x)))
   (ap (split_idem_retr (fun x : X => s (r x)))
      (1 @
       ap (split_idem_sect (fun x : X => s (r x)))
         (split_idem_issect (fun x : X => s (r x))
            (split_idem_retr (fun x : X => s (r x)) x))) @
    split_idem_issect (fun x : X => s (r x))
      (split_idem_retr (fun x : X => s (r x)) x))^ @
 ap s (H (r (s (r x))))) @ ap s (H (r x))
    rewrite concat_1p, concat_pp_p, ap_V; apply moveL_Vp; rewrite concat_p1.
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
x: X
ap (split_idem_sect (fun x : X => s (r x)))
  (ap (split_idem_retr (fun x : X => s (r x)))
     (ap (split_idem_sect (fun x : X => s (r x)))
        (split_idem_issect (fun x : X => s (r x))
           (split_idem_retr (fun x : X => s (r x)) x))) @
   split_idem_issect (fun x : X => s (r x))
     (split_idem_retr (fun x : X => s (r x)) x)) =
ap s (H (r (s (r x)))) @ ap s (H (r x))
    (** Brace yourself. *)
    unfold split_idem_issect, nudge_eq.
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
x: X
ap (split_idem_sect (fun x : X => s (r x)))
  (ap (split_idem_retr (fun x : X => s (r x)))
     (ap (split_idem_sect (fun x : X => s (r x)))
        ((path_split_idem (fun x : X => s (r x))
            (split_idem_issect_part1
               (fun x : X => s (r x))
               (split_idem_retr (fun x : X => s (r x))
                  x))
            (split_idem_issect_part2
               (fun x : X => s (r x))
               (split_idem_retr (fun x : X => s (r x))
                  x)))^ @
         (path_split_idem (fun x : X => s (r x))
            (fun n : nat =>
             isidem (fun x : X => s (r x))
               (split_idem_retr (fun x : X => s (r x))
                  x n.+1))
            (fun n : nat =>
             ((ap_compose (fun x : X => s (r x))
                 (fun x : X => s (r x))
                 ((split_idem_retr (fun ... => s ...)
                     x).2 n.+1) @@ 1)^ @
              concat_Ap
                (isidem (fun x : X => s (r x)))
                ((split_idem_retr
                    (fun x : X => s (r x)) x).2 n.+1)) @
             (isidem2 (fun x : X => s (r x))
                ((split_idem_retr
                    (fun x : X => s (r x)) x).1 n.+2) @@
              1)^) @
          path_split_idem (fun x : X => s (r x))
            (fun n : nat =>
             (split_idem_retr (fun x : X => s (r x)) x).2
               n) (fun n : nat => 1)))) @
   ((path_split_idem (fun x : X => s (r x))
       (split_idem_issect_part1 (fun x : X => s (r x))
          (split_idem_retr (fun x : X => s (r x)) x))
       (split_idem_issect_part2 (fun x : X => s (r x))
          (split_idem_retr (fun x : X => s (r x)) x)))^ @
    (path_split_idem (fun x : X => s (r x))
       (fun n : nat =>
        isidem (fun x : X => s (r x))
          (split_idem_retr (fun x : X => s (r x)) x
             n.+1))
       (fun n : nat =>
        ((ap_compose (fun x : X => s (r x))
            (fun x : X => s (r x))
            ((split_idem_retr (fun x : X => s (r x)) x).2
               n.+1) @@ 1)^ @
         concat_Ap (isidem (fun x : X => s (r x)))
           ((split_idem_retr (fun x : X => s (r x)) x).2
              n.+1)) @
        (isidem2 (fun x : X => s (r x))
           ((split_idem_retr (fun x : X => s (r x)) x).1
              n.+2) @@ 1)^) @
     path_split_idem (fun x : X => s (r x))
       (fun n : nat =>
        (split_idem_retr (fun x : X => s (r x)) x).2 n)
       (fun n : nat => 1)))) =
ap s (H (r (s (r x)))) @ ap s (H (r x))
    repeat (rewrite !ap_pp, ?ap_V, !sect_path_split_idem; simpl).
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
x: X
((ap (split_idem_sect (fun x : X => s (r x)))
    (ap (split_idem_retr (fun x : X => s (r x)))
       (ap (fun x : X => s (r x))
          (isidem (fun x : X => s (r x)) x))))^ @
 (ap (split_idem_sect (fun x : X => s (r x)))
    (ap (split_idem_retr (fun x : X => s (r x)))
       (isidem (fun x : X => s (r x)) (s (r x)))) @
  ap (split_idem_sect (fun x : X => s (r x)))
    (ap (split_idem_retr (fun x : X => s (r x)))
       (isidem (fun x : X => s (r x)) x)))) @
((ap (fun x : X => s (r x))
    (isidem (fun x : X => s (r x)) x))^ @
 (isidem (fun x : X => s (r x)) (s (r x)) @
  isidem (fun x : X => s (r x)) x)) =
ap s (H (r (s (r x)))) @ ap s (H (r x))
    (** Whew, that's not so bad. *)
    unfold isidem; fold A r s H.
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
x: X
((ap (split_idem_sect (fun x : X => s (r x)))
    (ap (split_idem_retr (fun x : X => s (r x)))
       (ap (fun x : X => s (r x)) (ap s (H (r x))))))^ @
 (ap (split_idem_sect (fun x : X => s (r x)))
    (ap (split_idem_retr (fun x : X => s (r x)))
       (ap s (H (r (s (r x)))))) @
  ap (split_idem_sect (fun x : X => s (r x)))
    (ap (split_idem_retr (fun x : X => s (r x)))
       (ap s (H (r x)))))) @
((ap (fun x : X => s (r x)) (ap s (H (r x))))^ @
 (ap s (H (r (s (r x)))) @ ap s (H (r x)))) =
ap s (H (r (s (r x)))) @ ap s (H (r x))
    Open Scope long_path_scope.
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
x: X
(ap (split_idem_sect (fun x : X => s (r x)))
   (ap (split_idem_retr (fun x : X => s (r x)))
      (ap (fun x : X => s (r x)) (ap s (H (r x))))))^
@' (ap (split_idem_sect (fun x : X => s (r x)))
      (ap (split_idem_retr (fun x : X => s (r x)))
         (ap s (H (r (s (r x))))))
    @' ap (split_idem_sect (fun x : X => s (r x)))
         (ap (split_idem_retr (fun x : X => s (r x)))
            (ap s (H (r x)))))
@' ((ap (fun x : X => s (r x)) (ap s (H (r x))))^
    @' (ap s (H (r (s (r x))))
        @' ap s (H (r x)))) =
ap s (H (r (s (r x))))
@' ap s (H (r x))
    rewrite !concat_p_pp.
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
x: X
(ap (split_idem_sect (fun x : X => s (r x)))
   (ap (split_idem_retr (fun x : X => s (r x)))
      (ap (fun x : X => s (r x)) (ap s (H (r x))))))^
@' ap (split_idem_sect (fun x : X => s (r x)))
     (ap (split_idem_retr (fun x : X => s (r x)))
        (ap s (H (r (s (r x))))))
@' ap (split_idem_sect (fun x : X => s (r x)))
     (ap (split_idem_retr (fun x : X => s (r x)))
        (ap s (H (r x))))
@' (ap (fun x : X => s (r x)) (ap s (H (r x))))^
@' ap s (H (r (s (r x))))
@' ap s (H (r x)) =
ap s (H (r (s (r x))))
@' ap s (H (r x))
    rewrite <- !ap_compose; simpl.
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
x: X
(ap (fun x : X => s (r x))
   (ap (fun x : A => s (r (s x))) (H (r x))))^
@' ap (fun x : A => s (r (s x))) (H (r (s (r x))))
@' ap (fun x : A => s (r (s x))) (H (r x))
@' (ap (fun x : A => s (r (s x))) (H (r x)))^
@' ap s (H (r (s (r x))))
@' ap s (H (r x)) =
ap s (H (r (s (r x))))
@' ap s (H (r x))
    apply whiskerR.
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
x: X
(ap (fun x : X => s (r x))
   (ap (fun x : A => s (r (s x))) (H (r x))))^
@' ap (fun x : A => s (r (s x))) (H (r (s (r x))))
@' ap (fun x : A => s (r (s x))) (H (r x))
@' (ap (fun x : A => s (r (s x))) (H (r x)))^
@' ap s (H (r (s (r x)))) = ap s (H (r (s (r x))))
    refine (_ @ (concat_1p _)); apply whiskerR.
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
x: X
(ap (fun x : X => s (r x))
   (ap (fun x : A => s (r (s x))) (H (r x))))^
@' ap (fun x : A => s (r (s x))) (H (r (s (r x))))
@' ap (fun x : A => s (r (s x))) (H (r x))
@' (ap (fun x : A => s (r (s x))) (H (r x)))^ = 1
    apply moveR_pV; rewrite concat_1p, concat_pp_p; apply moveR_Vp.
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
x: X
ap (fun x : A => s (r (s x))) (H (r (s (r x))))
@' ap (fun x : A => s (r (s x))) (H (r x)) =
ap (fun x : X => s (r x))
  (ap (fun x : A => s (r (s x))) (H (r x)))
@' ap (fun x : A => s (r (s x))) (H (r x))
    rewrite <- (ap_compose (s o r o s) (s o r)).
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
x: X
ap (fun x : A => s (r (s x))) (H (r (s (r x))))
@' ap (fun x : A => s (r (s x))) (H (r x)) =
ap (fun x : retract_type R => s (r (s (r (s x)))))
  (H (r x))
@' ap (fun x : A => s (r (s x))) (H (r x))
    rewrite (ap_compose (r o s) s _).
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
x: X
ap s
  (ap (fun x : retract_type R => r (s x))
     (H (r (s (r x)))))
@' ap (fun x : A => s (r (s x))) (H (r x)) =
ap (fun x : retract_type R => s (r (s (r (s x)))))
  (H (r x))
@' ap (fun x : A => s (r (s x))) (H (r x))
    rewrite (ap_compose (r o s) s _).
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
x: X
ap s
  (ap (fun x : retract_type R => r (s x))
     (H (r (s (r x)))))
@' ap s
     (ap (fun x : retract_type R => r (s x)) (H (r x))) =
ap (fun x : retract_type R => s (r (s (r (s x)))))
  (H (r x))
@' ap s
     (ap (fun x : retract_type R => r (s x)) (H (r x)))
    rewrite (ap_compose (r o s o r o s) s _).
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
x: X
ap s
  (ap (fun x : retract_type R => r (s x))
     (H (r (s (r x)))))
@' ap s
     (ap (fun x : retract_type R => r (s x)) (H (r x))) =
ap s
  (ap (fun x : retract_type R => r (s (r (s x))))
     (H (r x)))
@' ap s
     (ap (fun x : retract_type R => r (s x)) (H (r x)))
    rewrite <- !ap_pp; apply ap.
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
x: X
ap (fun x : retract_type R => r (s x))
  (H (r (s (r x))))
@' ap (fun x : retract_type R => r (s x)) (H (r x)) =
ap (fun x : retract_type R => r (s (r (s x))))
  (H (r x))
@' ap (fun x : retract_type R => r (s x)) (H (r x))
    refine (cancelR _ _ (H (r x)) _).
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
x: X
ap (fun x : retract_type R => r (s x))
  (H (r (s (r x))))
@' ap (fun x : retract_type R => r (s x)) (H (r x))
@' H (r x) =
ap (fun x : retract_type R => r (s (r (s x))))
  (H (r x))
@' ap (fun x : retract_type R => r (s x)) (H (r x))
@' H (r x)
    rewrite (concat_pA1_p H (H (r x)) _).
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
x: X
ap (fun x : retract_type R => r (s x))
  (H (r (s (r x))))
@' H (retract_retr R (retract_sect R (r x)))
@' H (r x) =
ap (fun x : retract_type R => r (s (r (s x))))
  (H (r x))
@' ap (fun x : retract_type R => r (s x)) (H (r x))
@' H (r x)
    rewrite (concat_pA1_p H (H (r x)) _).
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
x: X
ap (fun x : retract_type R => r (s x))
  (H (r (s (r x))))
@' H (retract_retr R (retract_sect R (r x)))
@' H (r x) =
ap (fun x : retract_type R => r (s (r (s x))))
  (H (r x))
@' H (retract_retr R (retract_sect R (r x)))
@' H (r x)
    refine ((concat_A1p H (H (r (s (r x)))) @@ 1) @ _).
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
x: X
H (retract_retr R (retract_sect R (r (s (r x)))))
@' H (r (s (r x)))
@' H (r x) =
ap (fun x : retract_type R => r (s (r (s x))))
  (H (r x))
@' H (retract_retr R (retract_sect R (r x)))
@' H (r x)
    rewrite (ap_compose (r o s) (r o s) _).
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
x: X
H (retract_retr R (retract_sect R (r (s (r x)))))
@' H (r (s (r x)))
@' H (r x) =
ap (fun x : retract_type R => r (s x))
  (ap (fun x : retract_type R => r (s x)) (H (r x)))
@' H (retract_retr R (retract_sect R (r x)))
@' H (r x)
    rewrite (concat_A1p H (ap (r o s) (H (r x)))).
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
x: X
H (retract_retr R (retract_sect R (r (s (r x)))))
@' H (r (s (r x)))
@' H (r x) =
H (r (s (retract_retr R (retract_sect R (r x)))))
@' ap (fun x : retract_type R => r (s x)) (H (r x))
@' H (r x)
    rewrite !concat_pp_p; apply whiskerL.
fs: Funext
X: Type
R: RetractOf X
A:= retract_type R: Type
r:= retract_retr R: X -> retract_type R
s:= retract_sect R: retract_type R -> X
H:= retract_issect R: retract_retr R o retract_sect R == idmap
x: X
H (r (s (r x)))
@' H (r x) =
ap (fun x : retract_type R => r (s x)) (H (r x))
@' H (r x)
    symmetry; refine (concat_A1p H (H (r x))).
    Close Scope long_path_scope.
  Qed.

End AlreadySplit.

(** Using these facts, we can show that [RetractOf X] is a retract of [QuasiIdempotent X]. *)

Section RetractOfRetracts.
  Context `{ua : Univalence} {X : Type}.

  Definition retract_retractof_qidem : RetractOf (QuasiIdempotent X).
ua: Univalence
X: Type
RetractOf (QuasiIdempotent X)
  Proof.
ua: Univalence
X: Type
RetractOf (QuasiIdempotent X)
    refine (Build_RetractOf (QuasiIdempotent X)
                            (RetractOf X)
                            split_idem_retract'
                            qidem_retract _).
ua: Univalence
X: Type
(fun x : RetractOf X =>
 split_idem_retract' (qidem_retract x)) == idmap
    intros R.
ua: Univalence
X: Type
R: RetractOf X
split_idem_retract' (qidem_retract R) = R
    exact (@path_retractof _ _
             (split_idem_retract' (qidem_retract R)) R
             (equiv_split_idem_retract R)
             (equiv_split_idem_retract_retr R)
             (equiv_split_idem_retract_sect R)
             (equiv_split_idem_retract_issect R)).
  Defined.

  (** We have a similar result for splittings of a fixed map [f].  *)
  Definition splitting_retractof_isqidem (f : X -> X)
  : RetractOf { I : IsPreIdempotent f & IsQuasiIdempotent f }.
ua: Univalence
X: Type
f: X -> X
RetractOf
  {I : IsPreIdempotent f & IsQuasiIdempotent f}
  Proof.
ua: Univalence
X: Type
f: X -> X
RetractOf
  {I : IsPreIdempotent f & IsQuasiIdempotent f}
    simple refine (@equiv_retractof'
              _ (@retractof_equiv'
                   (hfiber quasiidempotent_pr1 f) _ _
                   (retractof_hfiber
                      retract_retractof_qidem quasiidempotent_pr1 retract_idem
                      (fun _ => 1) f))
              (Splitting f) _).
ua: Univalence
X: Type
f: X -> X
hfiber quasiidempotent_pr1 f <~>
{I : IsPreIdempotent f & IsQuasiIdempotent f}
ua: Univalence
X: Type
f: X -> X
retract_type
  (retractof_equiv' ?f
     (retractof_hfiber retract_retractof_qidem
        quasiidempotent_pr1 retract_idem
        (fun x : QuasiIdempotent X => 1) f)) <~>
Splitting f
    -
ua: Univalence
X: Type
f: X -> X
hfiber quasiidempotent_pr1 f <~>
{I : IsPreIdempotent f & IsQuasiIdempotent f} refine ((hfiber_fibration f
                  (fun g => { I : IsPreIdempotent g & @IsQuasiIdempotent _ g I }))^-1 oE _).
ua: Univalence
X: Type
f: X -> X
hfiber quasiidempotent_pr1 f <~> hfiber pr1 f
      unfold hfiber.
ua: Univalence
X: Type
f: X -> X
{x : QuasiIdempotent X & x = f} <~>
{x
: {g : X -> X &
  {I : IsPreIdempotent g & IsQuasiIdempotent g}} &
x.1 = f}
      refine (equiv_functor_sigma' (equiv_sigma_assoc _ _)^-1 (fun a => _)); simpl.
ua: Univalence
X: Type
f: X -> X
a: {f : PreIdempotent X & IsQuasiIdempotent f}
a = f <~> (a.1).1 = f
      destruct a as [[g I] J]; unfold quasiidempotent_pr1; simpl.
ua: Univalence
X: Type
f, g: X -> X
I: IsPreIdempotent g
J: IsQuasiIdempotent (g; I)
g = f <~> g = f
      exact equiv_idmap.
    -
ua: Univalence
X: Type
f: X -> X
retract_type
  (retractof_equiv'
     ((hfiber_fibration f
         (fun g : X -> X =>
          {I : IsPreIdempotent g &
          IsQuasiIdempotent g}))^-1
      oE (equiv_functor_sigma'
            (equiv_sigma_assoc IsPreIdempotent
               (fun f : PreIdempotent X =>
                IsQuasiIdempotent f))^-1
            (fun
               a : {f : PreIdempotent X &
                   IsQuasiIdempotent f} =>
             (fun
                proj2 : {a0 : X -> X &
                        IsPreIdempotent a0} =>
              (fun (g : X -> X)
                 (I : IsPreIdempotent g)
                 (J : IsQuasiIdempotent (g; I)) =>
               (1 : ((g; I); J).1 = f <~> g = f)
               :
               ((g; I); J) = f <~> g = f) proj2.1
                proj2.2) a.1 a.2
             :
             a = f <~>
             ((equiv_sigma_assoc IsPreIdempotent
                 (fun f : PreIdempotent X =>
                  IsQuasiIdempotent f))^-1 a).1 = f)
          :
          hfiber quasiidempotent_pr1 f <~>
          hfiber pr1 f))
     (retractof_hfiber retract_retractof_qidem
        quasiidempotent_pr1 retract_idem
        (fun x : QuasiIdempotent X => 1) f)) <~>
Splitting f simpl.
ua: Univalence
X: Type
f: X -> X
hfiber retract_idem f <~> Splitting f  unfold hfiber, Splitting.
ua: Univalence
X: Type
f: X -> X
{x : RetractOf X & retract_idem x = f} <~>
{R : RetractOf X & retract_idem R == f}
      refine (equiv_functor_sigma_id _);
        intros R; simpl.
ua: Univalence
X: Type
f: X -> X
R: RetractOf X
(fun x : X => retract_sect R (retract_retr R x)) = f <~>
(fun x : X => retract_sect R (retract_retr R x)) == f
      apply equiv_ap10.
  Defined.

  (** And also for splittings of a fixed map that also induce a given witness of pre-idempotency. *)
  Definition Splitting_PreIdempotent (f : PreIdempotent X)
  := { S : Splitting f &
       forall x, ap f (S.2 x)^
                 @ (S.2 (retract_idem S.1 x))^
                 @ ap (retract_sect S.1) (retract_issect S.1 (retract_retr S.1 x))
                 @ S.2 x
                 = (isidem f x) }.

  Definition splitting_preidem_retractof_qidem (f : PreIdempotent X)
  : RetractOf (IsQuasiIdempotent f).
ua: Univalence
X: Type
f: PreIdempotent X
RetractOf (IsQuasiIdempotent f)
  Proof.
ua: Univalence
X: Type
f: PreIdempotent X
RetractOf (IsQuasiIdempotent f)
    simple refine (@equiv_retractof'
              _ (@retractof_equiv'
                   (hfiber (@pr1 _ (fun fi => @IsQuasiIdempotent _ fi.1 fi.2)) f) _ _
                   (retractof_hfiber
                      retract_retractof_qidem pr1 preidem_retract
                      _ f))
              (Splitting_PreIdempotent f) _).
ua: Univalence
X: Type
f: PreIdempotent X
hfiber pr1 f <~> IsQuasiIdempotent f
ua: Univalence
X: Type
f: PreIdempotent X
preidem_retract o retract_retr retract_retractof_qidem ==
pr1
ua: Univalence
X: Type
f: PreIdempotent X
retract_type
  (retractof_equiv' ?f
     (retractof_hfiber retract_retractof_qidem pr1
        preidem_retract ?p f)) <~>
Splitting_PreIdempotent f
    -
ua: Univalence
X: Type
f: PreIdempotent X
hfiber pr1 f <~> IsQuasiIdempotent f symmetry; exact (hfiber_fibration f _).
    -
ua: Univalence
X: Type
f: PreIdempotent X
preidem_retract o retract_retr retract_retractof_qidem ==
pr1 intros [[g I] J]; simpl.
ua: Univalence
X: Type
f: PreIdempotent X
g: X -> X
I: IsPreIdempotent g
J: IsQuasiIdempotent (g; I)
(fun x : X => ((g; I); J) x;
fun x : X =>
ap (split_idem_sect ((g; I); J))
  (split_idem_issect ((g; I); J)
     (split_idem_retr ((g; I); J) x))) = (g; I)
      refine (path_sigma' _ 1 _); simpl.
ua: Univalence
X: Type
f: PreIdempotent X
g: X -> X
I: IsPreIdempotent g
J: IsQuasiIdempotent (g; I)
(fun x : X =>
 ap (split_idem_sect ((g; I); J))
   (split_idem_issect ((g; I); J)
      (split_idem_retr ((g; I); J) x))) = I
      apply path_forall; intros x; apply split_idem_preidem.
    -
ua: Univalence
X: Type
f: PreIdempotent X
retract_type
  (retractof_equiv'
     (hfiber_fibration f
        (fun fi : {x : _ & IsPreIdempotent x} =>
         IsQuasiIdempotent fi.1))^-1
     (retractof_hfiber retract_retractof_qidem pr1
        preidem_retract
        ((fun x : QuasiIdempotent X =>
          (fun proj2 : PreIdempotent X =>
           (fun (g : X -> X) (I : IsPreIdempotent g)
              (J : IsQuasiIdempotent (g; I)) =>
            path_sigma'
              (fun f : X -> X => IsPreIdempotent f) 1
              (path_forall
                 (fun x0 : X =>
                  ap (split_idem_sect (...; J))
                    (split_idem_issect (...; J) (...)))
                 I
                 ((fun x0 : X =>
                   split_idem_preidem (...; J) x0)
                  :
                  (fun ... => ap ... ...) == I)
               :
               transport
                 (fun f : X -> X => IsPreIdempotent f)
                 1
                 (fun x0 : X =>
                  ap (split_idem_sect ...)
                    (split_idem_issect ... ...)) = I)
            :
            preidem_retract
              (retract_retr retract_retractof_qidem
                 ((g; I); J)) = ((g; I); J).1) proj2.1
             proj2.2) x.1 x.2)
         :
         preidem_retract
         o retract_retr retract_retractof_qidem == pr1)
        f)) <~> Splitting_PreIdempotent f simpl; unfold hfiber, Splitting.
ua: Univalence
X: Type
f: PreIdempotent X
{x : RetractOf X &
(fun x0 : X => retract_sect x (retract_retr x x0);
fun x0 : X =>
ap (retract_sect x)
  (retract_issect x (retract_retr x x0))) = f} <~>
Splitting_PreIdempotent f
      refine (equiv_sigma_assoc _ _ oE _).
ua: Univalence
X: Type
f: PreIdempotent X
{x : RetractOf X &
(fun x0 : X => retract_sect x (retract_retr x x0);
fun x0 : X =>
ap (retract_sect x)
  (retract_issect x (retract_retr x x0))) = f} <~>
{a : RetractOf X &
{p : retract_idem a == f &
forall x : X,
((ap f ((a; p).2 x)^ @
  ((a; p).2 (retract_idem (a; p).1 x))^) @
 ap (retract_sect (a; p).1)
   (retract_issect (a; p).1 (retract_retr (a; p).1 x))) @
(a; p).2 x = isidem f x}}
      apply equiv_functor_sigma_id; intros R; simpl.
ua: Univalence
X: Type
f: PreIdempotent X
R: RetractOf X
(fun x : X => retract_sect R (retract_retr R x);
fun x : X =>
ap (retract_sect R)
  (retract_issect R (retract_retr R x))) = f <~>
{p
: (fun x : X => retract_sect R (retract_retr R x)) ==
  f &
forall x : X,
((ap f (p x)^ @
  (p (retract_sect R (retract_retr R x)))^) @
 ap (retract_sect R)
   (retract_issect R (retract_retr R x))) @ p x =
isidem f x}
      refine (_ oE (equiv_path_sigma _ _ _)^-1); simpl.
ua: Univalence
X: Type
f: PreIdempotent X
R: RetractOf X
{p
: (fun x : X => retract_sect R (retract_retr R x)) =
  f.1 &
transport (fun f : X -> X => IsPreIdempotent f) p
  (fun x : X =>
   ap (retract_sect R)
     (retract_issect R (retract_retr R x))) = f.2} <~>
{p
: (fun x : X => retract_sect R (retract_retr R x)) ==
  f &
forall x : X,
((ap f (p x)^ @
  (p (retract_sect R (retract_retr R x)))^) @
 ap (retract_sect R)
   (retract_issect R (retract_retr R x))) @ p x =
isidem f x}
      refine (equiv_functor_sigma' (equiv_ap10 _ _) _); intros H; simpl.
ua: Univalence
X: Type
f: PreIdempotent X
R: RetractOf X
H: (fun x : X => retract_sect R (retract_retr R x)) =
f.1
transport (fun f : X -> X => IsPreIdempotent f) H
  (fun x : X =>
   ap (retract_sect R)
     (retract_issect R (retract_retr R x))) = f.2 <~>
(forall x : X,
 ((ap f (ap10 H x)^ @
   (ap10 H (retract_sect R (retract_retr R x)))^) @
  ap (retract_sect R)
    (retract_issect R (retract_retr R x))) @ ap10 H x =
 isidem f x)
      destruct f as [f I]; simpl in *.
ua: Univalence
X: Type
f: X -> X
I: IsPreIdempotent f
R: RetractOf X
H: (fun x : X => retract_sect R (retract_retr R x)) =
f
transport (fun f : X -> X => IsPreIdempotent f) H
  (fun x : X =>
   ap (retract_sect R)
     (retract_issect R (retract_retr R x))) = I <~>
(forall x : X,
 ((ap f (ap10 H x)^ @
   (ap10 H (retract_sect R (retract_retr R x)))^) @
  ap (retract_sect R)
    (retract_issect R (retract_retr R x))) @ ap10 H x =
 isidem f x)
      destruct H; simpl.
ua: Univalence
X: Type
R: RetractOf X
I: IsPreIdempotent
  (fun x : X => retract_sect R (retract_retr R x))
(fun x : X =>
 ap (retract_sect R)
   (retract_issect R (retract_retr R x))) = I <~>
(forall x : X,
 (1 @
  ap (retract_sect R)
    (retract_issect R (retract_retr R x))) @ 1 =
 isidem
   (fun x0 : X => retract_sect R (retract_retr R x0))
   x)
      refine (_ oE (equiv_path_forall _ _)^-1);
        unfold pointwise_paths.
ua: Univalence
X: Type
R: RetractOf X
I: IsPreIdempotent
  (fun x : X => retract_sect R (retract_retr R x))
(forall x : X,
 ap (retract_sect R)
   (retract_issect R (retract_retr R x)) = I x) <~>
(forall x : X,
 (1 @
  ap (retract_sect R)
    (retract_issect R (retract_retr R x))) @ 1 =
 isidem
   (fun x0 : X => retract_sect R (retract_retr R x0))
   x)
      apply equiv_functor_forall_id; intros x; simpl.
ua: Univalence
X: Type
R: RetractOf X
I: IsPreIdempotent
  (fun x : X => retract_sect R (retract_retr R x))
x: X
ap (retract_sect R)
  (retract_issect R (retract_retr R x)) = I x <~>
(1 @
 ap (retract_sect R)
   (retract_issect R (retract_retr R x))) @ 1 =
isidem
  (fun x : X => retract_sect R (retract_retr R x)) x
      unfold isidem.
ua: Univalence
X: Type
R: RetractOf X
I: IsPreIdempotent
  (fun x : X => retract_sect R (retract_retr R x))
x: X
ap (retract_sect R)
  (retract_issect R (retract_retr R x)) = I x <~>
(1 @
 ap (retract_sect R)
   (retract_issect R (retract_retr R x))) @ 1 = I x
      apply equiv_concat_l.
ua: Univalence
X: Type
R: RetractOf X
I: IsPreIdempotent
  (fun x : X => retract_sect R (retract_retr R x))
x: X
(1 @
 ap (retract_sect R)
   (retract_issect R (retract_retr R x))) @ 1 =
ap (retract_sect R)
  (retract_issect R (retract_retr R x))
      exact (concat_p1 _ @ concat_1p _).
  Defined.

End RetractOfRetracts.

(** ** Fully coherent idempotents *)

(** This gives us a way to define fully coherent idempotents.  By Corollary 4.4.5.14 of *Higher Topos Theory*, if we assume univalence then [RetractOf X] has the correct homotopy type of the type of fully coherent idempotents on [X].  However, its defect is that it raises the universe level.  But now that we've shown that [RetractOf X] is a retract of the type [QuasiIdempotent X], which is of the same size as [X], we can obtain an equivalent type by splitting the resulting idempotent on [QuasiIdempotent X].

For convenience, we instead split the idempotent on splittings of a fixed map [f], and then sum them up to obtain the type of idempotents. *)

Section CoherentIdempotents.
  Context {ua : Univalence}.

  Class IsIdempotent {X : Type} (f : X -> X)
    := is_coherent_idem : split_idem (retract_idem (splitting_retractof_isqidem f)).

  Definition Build_IsIdempotent {X : Type} (f : X -> X)
  : Splitting f -> IsIdempotent f
    := (equiv_split_idem_retract (splitting_retractof_isqidem f))^-1.

  Definition isidem_isqidem {X : Type} (f : X -> X) `{IsQuasiIdempotent _ f}
  : IsIdempotent f
    := Build_IsIdempotent f (split_idem_split f).

  #[export] Instance ispreidem_isidem {X : Type} (f : X -> X)
         `{IsIdempotent _ f} : IsPreIdempotent f.
ua: Univalence
X: Type
f: X -> X
H: IsIdempotent f
IsPreIdempotent f
  Proof.
ua: Univalence
X: Type
f: X -> X
H: IsIdempotent f
IsPreIdempotent f
    refine (split_idem_sect (retract_idem (splitting_retractof_isqidem f)) _).1.
ua: Univalence
X: Type
f: X -> X
H: IsIdempotent f
split_idem
  (retract_idem (splitting_retractof_isqidem f))
    assumption.
  Defined.

  #[export] Instance isqidem_isidem {X : Type} (f : X -> X)
         `{IsIdempotent _ f} : @IsQuasiIdempotent X f (ispreidem_isidem f).
ua: Univalence
X: Type
f: X -> X
H: IsIdempotent f
IsQuasiIdempotent f
  Proof.
ua: Univalence
X: Type
f: X -> X
H: IsIdempotent f
IsQuasiIdempotent f
    exact (split_idem_sect (retract_idem (splitting_retractof_isqidem f)) _).2.
  Defined.

  Definition Idempotent (X : Type) := { f : X -> X & IsIdempotent f }.

  Definition idempotent_pr1 {X : Type} : Idempotent X -> (X -> X) := pr1.
  Coercion idempotent_pr1 : Idempotent >-> Funclass.

  #[export] Instance isidem_idem (X : Type) (f : Idempotent X) : IsIdempotent f
    := f.2.

  (** The above definitions depend on [Univalence].  Technically this is the case by their construction, since they are a splitting of a map that we only know to be idempotent in the presence of univalence.  This map could be defined, and hence "split", without univalence; but also only with univalence do we know that they have the right homotopy type.  Thus univalence is used in two places: concluding (meta-theoretically) from HTT 4.4.5.14 that [RetractOf X] has the right homotopy type, and showing (in the next lemma) that it is equivalent to [Idempotent X].  In the absence of univalence, we don't currently have *any* provably-correct definition of the type of coherent idempotents; it ought to involve an infinite tower of coherences as defined in HTT section 4.4.5.   However, there may be some Yoneda-like meta-theoretic argument which would imply that the above-defined types do have the correct homotopy type without univalence (though almost certainly not without funext). *)

  Definition equiv_idempotent_retractof (X : Type)
  : Idempotent X <~> RetractOf X.
ua: Univalence
X: Type
Idempotent X <~> RetractOf X
  Proof.
ua: Univalence
X: Type
Idempotent X <~> RetractOf X
    transitivity ({ f : X -> X & Splitting f }).
ua: Univalence
X: Type
Idempotent X <~> {f : X -> X & Splitting f}
ua: Univalence
X: Type
{f : X -> X & Splitting f} <~> RetractOf X
    -
ua: Univalence
X: Type
Idempotent X <~> {f : X -> X & Splitting f} unfold Idempotent.
ua: Univalence
X: Type
{f : X -> X & IsIdempotent f} <~>
{f : X -> X & Splitting f}
      refine (equiv_functor_sigma' (equiv_idmap _) _); intros f; simpl.
ua: Univalence
X: Type
f: X -> X
IsIdempotent f <~> Splitting f
      refine (equiv_split_idem_retract (splitting_retractof_isqidem f)).
    -
ua: Univalence
X: Type
{f : X -> X & Splitting f} <~> RetractOf X unfold Splitting.
ua: Univalence
X: Type
{f : X -> X & {R : RetractOf X & retract_idem R == f}} <~>
RetractOf X
      refine (_ oE equiv_sigma_symm _).
ua: Univalence
X: Type
{b : RetractOf X & {a : X -> X & retract_idem b == a}} <~>
RetractOf X
      apply equiv_sigma_contr; intros R.
ua: Univalence
X: Type
R: RetractOf X
Contr {a : X -> X & retract_idem R == a}
      apply contr_basedhomotopy.
  Defined.

  (** For instance, here is the standard coherent idempotent structure on the identity map. *)
  #[export] Instance isidem_idmap (X : Type@{i})
  : @IsIdempotent@{i i j} X idmap
    := Build_IsIdempotent idmap (splitting_idmap X).

  Definition idem_idmap (X : Type@{i}) : Idempotent@{i i j} X
  := (idmap ; isidem_idmap X).
End CoherentIdempotents.

(** ** Quasi-idempotents need not be fully coherent *)

(** We have shown that every quasi-idempotent can be "coherentified" into a fully coherent idempotent, analogously to how every quasi-inverse can be coherentified into an equivalence.  However, just as for quasi-inverses, not every witness to quasi-idempotency *is itself* coherent.  This is in contrast to a witness of pre-idempotency, which (if it extends to a quasi-idempotent) can itself be extended to a coherent idempotent; this is roughly the content of [split_idem_preidem] and [splitting_preidem_retractof_qidem].

  The key step in showing this is to observe that when [f] is the identity, the retract type [Splitting_PreIdempotent f] of [splitting_preidem_retractof_qidem] is equivalent to the type of types-equivalent-to-[X], and hence contractible. *)

Definition contr_splitting_preidem_idmap {ua : Univalence} (X : Type)
: Contr (Splitting_PreIdempotent (preidem_idmap X)).
ua: Univalence
X: Type
Contr (Splitting_PreIdempotent (preidem_idmap X))
Proof.
ua: Univalence
X: Type
Contr (Splitting_PreIdempotent (preidem_idmap X))
  refine (contr_equiv' {Y : Type & X <~> Y} _).
ua: Univalence
X: Type
{Y : Type & X <~> Y} <~>
Splitting_PreIdempotent (preidem_idmap X)
  transitivity { S : Splitting (preidem_idmap X) &
                     forall x : X, (retract_issect S.1) (retract_retr S.1 x) = ap (retract_retr S.1) (S.2 x) }.
ua: Univalence
X: Type
{Y : Type & X <~> Y} <~>
{S : Splitting (preidem_idmap X) &
forall x : X,
retract_issect S.1 (retract_retr S.1 x) =
ap (retract_retr S.1) (S.2 x)}
ua: Univalence
X: Type
{S : Splitting (preidem_idmap X) &
forall x : X,
retract_issect S.1 (retract_retr S.1 x) =
ap (retract_retr S.1) (S.2 x)} <~>
Splitting_PreIdempotent (preidem_idmap X)
  1:make_equiv.
ua: Univalence
X: Type
{S : Splitting (preidem_idmap X) &
forall x : X,
retract_issect S.1 (retract_retr S.1 x) =
ap (retract_retr S.1) (S.2 x)} <~>
Splitting_PreIdempotent (preidem_idmap X)
  apply equiv_functor_sigma_id; intros [[Y r s eta] ep]; cbn in *.
ua: Univalence
X, Y: Type
r: X -> Y
s: Y -> X
eta: (fun x : Y => r (s x)) == idmap
ep: (fun x : X => s (r x)) == idmap
(forall x : X, eta (r x) = ap r (ep x)) <~>
(forall x : X,
 ((ap idmap (ep x)^ @ (ep (s (r x)))^) @
  ap s (eta (r x))) @ ep x = ispreidem_idmap X x)
  apply equiv_functor_forall_id; intros x.
ua: Univalence
X, Y: Type
r: X -> Y
s: Y -> X
eta: (fun x : Y => r (s x)) == idmap
ep: (fun x : X => s (r x)) == idmap
x: X
eta (r x) = ap r (ep x) <~>
((ap idmap (ep x)^ @ (ep (s (r x)))^) @
 ap s (eta (r x))) @ ep x = ispreidem_idmap X x
  unfold ispreidem_idmap; simpl.
ua: Univalence
X, Y: Type
r: X -> Y
s: Y -> X
eta: (fun x : Y => r (s x)) == idmap
ep: (fun x : X => s (r x)) == idmap
x: X
eta (r x) = ap r (ep x) <~>
((ap idmap (ep x)^ @ (ep (s (r x)))^) @
 ap s (eta (r x))) @ ep x = 1
  rewrite ap_idmap, !concat_pp_p.
ua: Univalence
X, Y: Type
r: X -> Y
s: Y -> X
eta: (fun x : Y => r (s x)) == idmap
ep: (fun x : X => s (r x)) == idmap
x: X
eta (r x) = ap r (ep x) <~>
(ep x)^ @
((ep (s (r x)))^ @ (ap s (eta (r x)) @ ep x)) = 1
  refine (equiv_moveR_Vp _ _ _ oE _).
ua: Univalence
X, Y: Type
r: X -> Y
s: Y -> X
eta: (fun x : Y => r (s x)) == idmap
ep: (fun x : X => s (r x)) == idmap
x: X
eta (r x) = ap r (ep x) <~>
(ep (s (r x)))^ @ (ap s (eta (r x)) @ ep x) = ep x @ 1
  rewrite concat_p1, concat_p_pp.
ua: Univalence
X, Y: Type
r: X -> Y
s: Y -> X
eta: (fun x : Y => r (s x)) == idmap
ep: (fun x : X => s (r x)) == idmap
x: X
eta (r x) = ap r (ep x) <~>
((ep (s (r x)))^ @ ap s (eta (r x))) @ ep x = ep x
  refine (equiv_concat_r (concat_1p _) _ oE _).
ua: Univalence
X, Y: Type
r: X -> Y
s: Y -> X
eta: (fun x : Y => r (s x)) == idmap
ep: (fun x : X => s (r x)) == idmap
x: X
eta (r x) = ap r (ep x) <~>
((ep (s (r x)))^ @ ap s (eta (r x))) @ ep x = 1 @ ep x
  refine (equiv_whiskerR _ _ _ oE _).
ua: Univalence
X, Y: Type
r: X -> Y
s: Y -> X
eta: (fun x : Y => r (s x)) == idmap
ep: (fun x : X => s (r x)) == idmap
x: X
eta (r x) = ap r (ep x) <~>
(ep (s (r x)))^ @ ap s (eta (r x)) = 1
  refine (equiv_moveR_Vp _ _ _ oE _).
ua: Univalence
X, Y: Type
r: X -> Y
s: Y -> X
eta: (fun x : Y => r (s x)) == idmap
ep: (fun x : X => s (r x)) == idmap
x: X
eta (r x) = ap r (ep x) <~>
ap s (eta (r x)) = ep (s (r x)) @ 1
  rewrite concat_p1.
ua: Univalence
X, Y: Type
r: X -> Y
s: Y -> X
eta: (fun x : Y => r (s x)) == idmap
ep: (fun x : X => s (r x)) == idmap
x: X
eta (r x) = ap r (ep x) <~>
ap s (eta (r x)) = ep (s (r x))
  pose (isequiv_adjointify s r ep eta).
ua: Univalence
X, Y: Type
r: X -> Y
s: Y -> X
eta: (fun x : Y => r (s x)) == idmap
ep: (fun x : X => s (r x)) == idmap
x: X
i:= isequiv_adjointify s r ep eta: IsEquiv s
eta (r x) = ap r (ep x) <~>
ap s (eta (r x)) = ep (s (r x))
  refine (_ oE equiv_ap (ap s) _ _).
ua: Univalence
X, Y: Type
r: X -> Y
s: Y -> X
eta: (fun x : Y => r (s x)) == idmap
ep: (fun x : X => s (r x)) == idmap
x: X
i:= isequiv_adjointify s r ep eta: IsEquiv s
ap s (eta (r x)) = ap s (ap r (ep x)) <~>
ap s (eta (r x)) = ep (s (r x))
  apply equiv_concat_r.
ua: Univalence
X, Y: Type
r: X -> Y
s: Y -> X
eta: (fun x : Y => r (s x)) == idmap
ep: (fun x : X => s (r x)) == idmap
x: X
i:= isequiv_adjointify s r ep eta: IsEquiv s
ap s (ap r (ep x)) = ep (s (r x))
  refine (cancelR _ _ (ep x) _).
ua: Univalence
X, Y: Type
r: X -> Y
s: Y -> X
eta: (fun x : Y => r (s x)) == idmap
ep: (fun x : X => s (r x)) == idmap
x: X
i:= isequiv_adjointify s r ep eta: IsEquiv s
ap s (ap r (ep x)) @ ep x = ep (s (r x)) @ ep x
  rewrite <- ap_compose.
ua: Univalence
X, Y: Type
r: X -> Y
s: Y -> X
eta: (fun x : Y => r (s x)) == idmap
ep: (fun x : X => s (r x)) == idmap
x: X
i:= isequiv_adjointify s r ep eta: IsEquiv s
ap (fun x : X => s (r x)) (ep x) @ ep x =
ep (s (r x)) @ ep x
  exact (concat_A1p ep (ep x)).
Qed.

(** Therefore, there is a unique coherentification of the canonical witness [preidem_idmap] of pre-idempotency for the identity.  Hence, to show that not every quasi-idempotent is coherent, it suffices to give a witness of quasi-idempotency extending [preidem_idmap] which is nontrivial (i.e. not equal to [qidem_idmap]).  Such a witness is exactly an element of the 2-center, and we know that some types such as [BAut (BAut Bool)] have nontrivial 2-centers.  In [Spaces.BAut.Bool.IncoherentIdempotent] we use this to construct an explicit counterexample. *)


(** ** A pre-idempotent that is not quasi-idempotent *)

(** We can also give a specific example of a pre-idempotent that does not split, hence is not coherentifiable and not even quasi-idempotent.  The construction is inspired by Warning 1.2.4.8 in *Higher Algebra*, and can be found in [Spaces.BAut.Cantor]. *)