Require Import HoTT.Basics HoTT.Types.Require Import HoTT.Basics HoTT.Types.
Require Import Equiv.BiInv Idempotents.
Require Import Universes.BAut Spaces.BAut.Bool.

Local Open Scope path_scope.

(** * An incoherent quasi-idempotent on [BAut (BAut Bool)]. *)

Section IncoherentQuasiIdempotent.
  Context `{Univalence}.

  (** We use the identity map, and the nontrivial 2-central element of [BAut (BAut Bool)]. *)
  Definition nontrivial_qidem_baut_baut_bool
  : IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool)))
    := negb_center2_baut_baut_bool.

  Let ret := splitting_preidem_retractof_qidem (preidem_idmap (BAut (BAut Bool))).
  Let s := retract_sect ret.
  Let r := retract_retr ret.
  Let issect := retract_issect ret : r o s == idmap.

  (** Since the space of splittings of the identity pre-idempotent is contractible, nontriviality of this 2-central element implies that not every quasi-idempotence witness of the identity is recoverable from its own splitting. *)
  Definition splitting_preidem_notequiv_qidem_baut_baut_bool
  : ~ (s o r == idmap).
H: Univalence
ret:= splitting_preidem_retractof_qidem (preidem_idmap (BAut (BAut Bool))): RetractOf (IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))))
s:= retract_sect ret: retract_type ret -> IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool)))
r:= retract_retr ret: IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))) -> retract_type ret
issect:= retract_issect ret: r o s == idmap
~ (s o r == idmap)
  Proof.
H: Univalence
ret:= splitting_preidem_retractof_qidem (preidem_idmap (BAut (BAut Bool))): RetractOf (IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))))
s:= retract_sect ret: retract_type ret -> IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool)))
r:= retract_retr ret: IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))) -> retract_type ret
issect:= retract_issect ret: r o s == idmap
~ (s o r == idmap)
    intros oops.
H: Univalence
ret:= splitting_preidem_retractof_qidem (preidem_idmap (BAut (BAut Bool))): RetractOf (IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))))
s:= retract_sect ret: retract_type ret -> IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool)))
r:= retract_retr ret: IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))) -> retract_type ret
issect:= retract_issect ret: r o s == idmap
oops: (fun x : IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))) => s (r x)) ==
idmap
Empty
    assert (p := oops nontrivial_qidem_baut_baut_bool).
H: Univalence
ret:= splitting_preidem_retractof_qidem (preidem_idmap (BAut (BAut Bool))): RetractOf (IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))))
s:= retract_sect ret: retract_type ret -> IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool)))
r:= retract_retr ret: IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))) -> retract_type ret
issect:= retract_issect ret: r o s == idmap
oops: (fun x : IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))) => s (r x)) ==
idmap
p: (fun x : IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))) => s (r x))
  nontrivial_qidem_baut_baut_bool =
idmap nontrivial_qidem_baut_baut_bool
Empty
    assert (q := oops (isqidem_idmap (BAut (BAut Bool)))); clear oops.
H: Univalence
ret:= splitting_preidem_retractof_qidem (preidem_idmap (BAut (BAut Bool))): RetractOf (IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))))
s:= retract_sect ret: retract_type ret -> IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool)))
r:= retract_retr ret: IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))) -> retract_type ret
issect:= retract_issect ret: r o s == idmap
p: (fun x : IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))) => s (r x))
  nontrivial_qidem_baut_baut_bool =
idmap nontrivial_qidem_baut_baut_bool
q: (fun x : IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))) => s (r x))
  (isqidem_idmap (BAut (BAut Bool))) =
idmap (isqidem_idmap (BAut (BAut Bool)))
Empty
    apply nontrivial_negb_center_baut_baut_bool.
H: Univalence
ret:= splitting_preidem_retractof_qidem (preidem_idmap (BAut (BAut Bool))): RetractOf (IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))))
s:= retract_sect ret: retract_type ret -> IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool)))
r:= retract_retr ret: IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))) -> retract_type ret
issect:= retract_issect ret: r o s == idmap
p: (fun x : IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))) => s (r x))
  nontrivial_qidem_baut_baut_bool =
idmap nontrivial_qidem_baut_baut_bool
q: (fun x : IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))) => s (r x))
  (isqidem_idmap (BAut (BAut Bool))) =
idmap (isqidem_idmap (BAut (BAut Bool)))
negb_center2_baut_baut_bool = (fun Z : BAut (BAut Bool) => 1)
    refine (p^ @ ap s _ @ q).
H: Univalence
ret:= splitting_preidem_retractof_qidem (preidem_idmap (BAut (BAut Bool))): RetractOf (IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))))
s:= retract_sect ret: retract_type ret -> IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool)))
r:= retract_retr ret: IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))) -> retract_type ret
issect:= retract_issect ret: r o s == idmap
p: (fun x : IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))) => s (r x))
  nontrivial_qidem_baut_baut_bool =
idmap nontrivial_qidem_baut_baut_bool
q: (fun x : IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))) => s (r x))
  (isqidem_idmap (BAut (BAut Bool))) =
idmap (isqidem_idmap (BAut (BAut Bool)))
r nontrivial_qidem_baut_baut_bool = r (isqidem_idmap (BAut (BAut Bool)))
    pose (contr_splitting_preidem_idmap (BAut (BAut Bool))).
H: Univalence
ret:= splitting_preidem_retractof_qidem (preidem_idmap (BAut (BAut Bool))): RetractOf (IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))))
s:= retract_sect ret: retract_type ret -> IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool)))
r:= retract_retr ret: IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))) -> retract_type ret
issect:= retract_issect ret: r o s == idmap
p: (fun x : IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))) => s (r x))
  nontrivial_qidem_baut_baut_bool =
idmap nontrivial_qidem_baut_baut_bool
q: (fun x : IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))) => s (r x))
  (isqidem_idmap (BAut (BAut Bool))) =
idmap (isqidem_idmap (BAut (BAut Bool)))
i:= contr_splitting_preidem_idmap (BAut (BAut Bool)): Contr (Splitting_PreIdempotent (preidem_idmap (BAut (BAut Bool))))
r nontrivial_qidem_baut_baut_bool = r (isqidem_idmap (BAut (BAut Bool)))
    apply path_contr.
  Defined.

  (** Therefore, not every quasi-idempotence witness is obtainable from *any* splitting, i.e. it may not have any coherentification. *)
  Definition not_all_coherent_qidem_baut_baut_bool
  : ~ (forall q : IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))),
         { S : Splitting_PreIdempotent (preidem_idmap _) & s S = q }).
H: Univalence
ret:= splitting_preidem_retractof_qidem (preidem_idmap (BAut (BAut Bool))): RetractOf (IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))))
s:= retract_sect ret: retract_type ret -> IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool)))
r:= retract_retr ret: IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))) -> retract_type ret
issect:= retract_issect ret: r o s == idmap
~
(forall q : IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))),
 {S : Splitting_PreIdempotent (preidem_idmap (BAut (BAut Bool))) & s S = q})
  Proof.
H: Univalence
ret:= splitting_preidem_retractof_qidem (preidem_idmap (BAut (BAut Bool))): RetractOf (IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))))
s:= retract_sect ret: retract_type ret -> IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool)))
r:= retract_retr ret: IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))) -> retract_type ret
issect:= retract_issect ret: r o s == idmap
~
(forall q : IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))),
 {S : Splitting_PreIdempotent (preidem_idmap (BAut (BAut Bool))) & s S = q})
    intros oops.
H: Univalence
ret:= splitting_preidem_retractof_qidem (preidem_idmap (BAut (BAut Bool))): RetractOf (IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))))
s:= retract_sect ret: retract_type ret -> IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool)))
r:= retract_retr ret: IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))) -> retract_type ret
issect:= retract_issect ret: r o s == idmap
oops: forall q : IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))),
{S : Splitting_PreIdempotent (preidem_idmap (BAut (BAut Bool))) & s S = q}
Empty
    assert (IsEquiv s).
H: Univalence
ret:= splitting_preidem_retractof_qidem (preidem_idmap (BAut (BAut Bool))): RetractOf (IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))))
s:= retract_sect ret: retract_type ret -> IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool)))
r:= retract_retr ret: IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))) -> retract_type ret
issect:= retract_issect ret: r o s == idmap
oops: forall q : IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))),
{S : Splitting_PreIdempotent (preidem_idmap (BAut (BAut Bool))) & s S = q}
IsEquiv s
H: Univalence
ret:= splitting_preidem_retractof_qidem (preidem_idmap (BAut (BAut Bool))): RetractOf (IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))))
s:= retract_sect ret: retract_type ret -> IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool)))
r:= retract_retr ret: IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))) -> retract_type ret
issect:= retract_issect ret: r o s == idmap
oops: forall q : IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))),
{S : Splitting_PreIdempotent (preidem_idmap (BAut (BAut Bool))) & s S = q}
X: IsEquiv s
Empty
    {
H: Univalence
ret:= splitting_preidem_retractof_qidem (preidem_idmap (BAut (BAut Bool))): RetractOf (IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))))
s:= retract_sect ret: retract_type ret -> IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool)))
r:= retract_retr ret: IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))) -> retract_type ret
issect:= retract_issect ret: r o s == idmap
oops: forall q : IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))),
{S : Splitting_PreIdempotent (preidem_idmap (BAut (BAut Bool))) & s S = q}
IsEquiv s apply isequiv_isbiinv.
H: Univalence
ret:= splitting_preidem_retractof_qidem (preidem_idmap (BAut (BAut Bool))): RetractOf (IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))))
s:= retract_sect ret: retract_type ret -> IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool)))
r:= retract_retr ret: IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))) -> retract_type ret
issect:= retract_issect ret: r o s == idmap
oops: forall q : IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))),
{S : Splitting_PreIdempotent (preidem_idmap (BAut (BAut Bool))) & s S = q}
IsBiInv s
      apply (Build_IsBiInv _ _ s (fun q => (oops q).1) r).
H: Univalence
ret:= splitting_preidem_retractof_qidem (preidem_idmap (BAut (BAut Bool))): RetractOf (IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))))
s:= retract_sect ret: retract_type ret -> IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool)))
r:= retract_retr ret: IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))) -> retract_type ret
issect:= retract_issect ret: r o s == idmap
oops: forall q : IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))),
{S : Splitting_PreIdempotent (preidem_idmap (BAut (BAut Bool))) & s S = q}
(fun x : IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))) => s (oops x).1) ==
idmap
H: Univalence
ret:= splitting_preidem_retractof_qidem (preidem_idmap (BAut (BAut Bool))): RetractOf (IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))))
s:= retract_sect ret: retract_type ret -> IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool)))
r:= retract_retr ret: IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))) -> retract_type ret
issect:= retract_issect ret: r o s == idmap
oops: forall q : IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))),
{S : Splitting_PreIdempotent (preidem_idmap (BAut (BAut Bool))) & s S = q}
(fun x : retract_type ret => r (s x)) == idmap
      2: exact issect.
H: Univalence
ret:= splitting_preidem_retractof_qidem (preidem_idmap (BAut (BAut Bool))): RetractOf (IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))))
s:= retract_sect ret: retract_type ret -> IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool)))
r:= retract_retr ret: IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))) -> retract_type ret
issect:= retract_issect ret: r o s == idmap
oops: forall q : IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))),
{S : Splitting_PreIdempotent (preidem_idmap (BAut (BAut Bool))) & s S = q}
(fun x : IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))) => s (oops x).1) ==
idmap
      exact (fun q => (oops q).2). }
H: Univalence
ret:= splitting_preidem_retractof_qidem (preidem_idmap (BAut (BAut Bool))): RetractOf (IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))))
s:= retract_sect ret: retract_type ret -> IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool)))
r:= retract_retr ret: IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))) -> retract_type ret
issect:= retract_issect ret: r o s == idmap
oops: forall q : IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))),
{S : Splitting_PreIdempotent (preidem_idmap (BAut (BAut Bool))) & s S = q}
X: IsEquiv s
Empty
    apply splitting_preidem_notequiv_qidem_baut_baut_bool; intros q.
H: Univalence
ret:= splitting_preidem_retractof_qidem (preidem_idmap (BAut (BAut Bool))): RetractOf (IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))))
s:= retract_sect ret: retract_type ret -> IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool)))
r:= retract_retr ret: IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))) -> retract_type ret
issect:= retract_issect ret: r o s == idmap
oops: forall q0 : IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))),
{S : Splitting_PreIdempotent (preidem_idmap (BAut (BAut Bool))) & s S = q0}
X: IsEquiv s
q: IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool)))
s (r q) = q
    refine (ap s (ap r (eisretr s q)^) @ _).
H: Univalence
ret:= splitting_preidem_retractof_qidem (preidem_idmap (BAut (BAut Bool))): RetractOf (IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))))
s:= retract_sect ret: retract_type ret -> IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool)))
r:= retract_retr ret: IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))) -> retract_type ret
issect:= retract_issect ret: r o s == idmap
oops: forall q0 : IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))),
{S : Splitting_PreIdempotent (preidem_idmap (BAut (BAut Bool))) & s S = q0}
X: IsEquiv s
q: IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool)))
s (r (s (s^-1 q))) = q
    refine (ap s (issect (s^-1 q)) @ _).
H: Univalence
ret:= splitting_preidem_retractof_qidem (preidem_idmap (BAut (BAut Bool))): RetractOf (IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))))
s:= retract_sect ret: retract_type ret -> IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool)))
r:= retract_retr ret: IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))) -> retract_type ret
issect:= retract_issect ret: r o s == idmap
oops: forall q0 : IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))),
{S : Splitting_PreIdempotent (preidem_idmap (BAut (BAut Bool))) & s S = q0}
X: IsEquiv s
q: IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool)))
s (s^-1 q) = q
    apply eisretr.
  Defined.

  (** These results show only that not *every* quasi-idempotence witness is coherent.  "Clearly" the nontrivial quasi-idempotence witness [nontrivial_qidem_baut_baut_bool] should be the one that is not coherent.  To show this, we would probably need to show that [isqidem_idmap] *is* in the image of [s], and this seems rather annoying to do based on our construction of [splitting_preidem_retractof_qidem]. *)

End IncoherentQuasiIdempotent.