Require Import HoTT.Basics HoTT.Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
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_biinv; split.
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}
{g
: IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))) ->
  retract_type ret &
(fun x : retract_type ret => g (s x)) == 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}
{h
: IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))) ->
  retract_type ret &
(fun
   x : IsQuasiIdempotent
         (preidem_idmap (BAut (BAut Bool))) => 
 s (h x)) == 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}
{g
: IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))) ->
  retract_type ret &
(fun x : retract_type ret => g (s x)) == idmap} exists r; 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}
{h
: IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))) ->
  retract_type ret &
(fun
   x : IsQuasiIdempotent
         (preidem_idmap (BAut (BAut Bool))) => s (h x)) ==
idmap} exists (fun q => (oops q).1).
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
q : IsQuasiIdempotent
      (preidem_idmap (BAut (BAut Bool))),
{S
: Splitting_PreIdempotent
    (preidem_idmap (BAut (BAut Bool))) &
s S = q}
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
q : IsQuasiIdempotent
      (preidem_idmap (BAut (BAut Bool))),
{S
: Splitting_PreIdempotent
    (preidem_idmap (BAut (BAut Bool))) &
s S = q}
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
q : IsQuasiIdempotent
      (preidem_idmap (BAut (BAut Bool))),
{S
: Splitting_PreIdempotent
    (preidem_idmap (BAut (BAut Bool))) &
s S = q}
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.