~ (forall q : IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))), { S : Splitting_PreIdempotent (preidem_idmap _) & s S = q }). Proof. intros oops. assert (IsEquiv s). { apply isequiv_biinv; split. - exists r; exact issect. - exists (fun q => (oops q).1). exact (fun q => (oops q).2). } apply splitting_preidem_notequiv_qidem_baut_baut_bool; intros q. refine (ap s (ap r (eisretr s q)^) @ _). refine (ap s (issect (s^-1 q)) @ _). apply eisretr. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Equiv.BiInv Idempotents. Require Import Universes.BAut Spaces.BAut.Bool.