(* -*- mode: coq; mode: visual-line -*- *)
Require Import HoTT.Basics HoTT.Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Idempotents.
Require Import HoTT.Truncations.Core Spaces.BAut Spaces.Cantor.

Local Open Scope equiv_scope.
Local Open Scope path_scope.

(** * BAut(Cantor) *)

(** ** A pre-idempotent on [BAut Cantor] that does not split *)

(** We go into a non-exported module so that we can use short names for definitions without polluting the global namespace. *)

Module BAut_Cantor_Idempotent.
Section Assumptions.
  Context `{Univalence}.

  Definition f : BAut Cantor -> BAut Cantor.
H: Univalence
BAut Cantor -> BAut Cantor
  Proof.
H: Univalence
BAut Cantor -> BAut Cantor
    intros Z.
H: Univalence
Z: BAut Cantor
BAut Cantor
    (** Here is the important part of this definition. *)
    exists (Z + Cantor)%type.
H: Univalence
Z: BAut Cantor
merely (Z + Cantor = Cantor)
    (** The rest is just a proof that [Z+Cantor] is again equivalent to [Cantor], using [cantor_fold] and the assumption that [Z] is equivalent to [Cantor]. *)
    pose (e := Z.2); simpl in e; clearbody e.
H: Univalence
Z: BAut Cantor
e: Tr (-1) (Z.1 = Cantor)
merely (Z + Cantor = Cantor)
    strip_truncations.
H: Univalence
Z: BAut Cantor
e: Z.1 = Cantor
merely (Z + Cantor = Cantor)
    apply tr.
H: Univalence
Z: BAut Cantor
e: Z.1 = Cantor
Z + Cantor = Cantor
    apply path_universe_uncurried.
H: Univalence
Z: BAut Cantor
e: Z.1 = Cantor
Z + Cantor <~> Cantor
    refine (equiv_cantor_fold oE _).
H: Univalence
Z: BAut Cantor
e: Z.1 = Cantor
Z + Cantor <~> Cantor + Cantor
    refine (equiv_path _ _ e +E 1).
  Defined.

  (** For the pre-idempotence of [f], the main point is again the existence of the equivalence [fold_cantor]. *)
  Definition preidem_f : IsPreIdempotent f.
H: Univalence
IsPreIdempotent f
  Proof.
H: Univalence
IsPreIdempotent f
    intros Z.
H: Univalence
Z: BAut Cantor
f (f Z) = f Z
    apply path_baut.
H: Univalence
Z: BAut Cantor
f (f Z) <~> f Z
    unfold f; simpl.
H: Univalence
Z: BAut Cantor
Z + Cantor + Cantor <~> Z + Cantor
    refine (_ oE equiv_sum_assoc Z Cantor Cantor).
H: Univalence
Z: BAut Cantor
Z + (Cantor + Cantor) <~> Z + Cantor
    apply (1 +E equiv_cantor_fold).
  Defined.

  (** We record how the action of [f] and [f o f] on paths corresponds to an action on equivalences. *)
  Definition ap_f {Z Z' : BAut Cantor} (p : Z = Z')
  : equiv_path _ _ (ap f p)..1
    = equiv_path Z Z' p..1 +E 1.
H: Univalence
Z, Z': BAut Cantor
p: Z = Z'
equiv_path (f Z).1 (f Z').1 (ap f p) ..1 =
equiv_path Z Z' p ..1 +E 1
  Proof.
H: Univalence
Z, Z': BAut Cantor
p: Z = Z'
equiv_path (f Z).1 (f Z').1 (ap f p) ..1 =
equiv_path Z Z' p ..1 +E 1
    destruct p.
H: Univalence
Z: BAut Cantor
equiv_path (f Z).1 (f Z).1 (ap f 1) ..1 =
equiv_path Z Z 1 ..1 +E 1 apply path_equiv, path_arrow.
H: Univalence
Z: BAut Cantor
equiv_path (f Z).1 (f Z).1 (ap f 1) ..1 ==
equiv_path Z Z 1 ..1 +E 1
    intros [z|a]; reflexivity.
  Defined.

  Definition ap_ff {Z Z' : BAut Cantor} (p : Z = Z')
  : equiv_path _ _ (ap (f o f) p)..1
    = equiv_path Z Z' p..1 +E 1 +E 1.
H: Univalence
Z, Z': BAut Cantor
p: Z = Z'
equiv_path (f (f Z)).1 (f (f Z')).1 (ap (f o f) p) ..1 =
equiv_path Z Z' p ..1 +E 1 +E 1
  Proof.
H: Univalence
Z, Z': BAut Cantor
p: Z = Z'
equiv_path (f (f Z)).1 (f (f Z')).1 (ap (f o f) p) ..1 =
equiv_path Z Z' p ..1 +E 1 +E 1
    destruct p.
H: Univalence
Z: BAut Cantor
equiv_path (f (f Z)).1 (f (f Z)).1
  (ap (fun x : BAut Cantor => f (f x)) 1) ..1 =
equiv_path Z Z 1 ..1 +E 1 +E 1 apply path_equiv, path_arrow.
H: Univalence
Z: BAut Cantor
equiv_path (f (f Z)).1 (f (f Z)).1
  (ap (fun x : BAut Cantor => f (f x)) 1) ..1 ==
equiv_path Z Z 1 ..1 +E 1 +E 1
    intros [[z|a]|a]; reflexivity.
  Defined.

  (** Now let's assume [f] is quasi-idempotent, but not necessarily using the same witness of pre-idempotency. *)
  Context (Ip : IsPreIdempotent f) (Jp : @IsQuasiIdempotent _ f Ip).

  Definition I (Z : BAut Cantor)
  : (Z + Cantor) + Cantor <~> Z + Cantor
    := equiv_path _ _ (Ip Z)..1.

  Definition I0
  : Cantor + Cantor + Cantor + Cantor <~> Cantor + Cantor + Cantor
    := I (f (point (BAut Cantor))).

  (** We don't know much about [I0], but we can show that it maps the rightmost two summands to the rightmost one, using the naturality of [I].  Here is the naturality. *)
  Definition Inat (Z Z' : BAut Cantor) (e : Z <~> Z')
  : I Z' oE (e +E 1 +E 1)
    = (e +E 1) oE I Z.
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
Z, Z': BAut Cantor
e: Z <~> Z'
I Z' oE (e +E 1 +E 1) = (e +E 1) oE I Z
  Proof.
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
Z, Z': BAut Cantor
e: Z <~> Z'
I Z' oE (e +E 1 +E 1) = (e +E 1) oE I Z
    revert e; equiv_intro (equiv_path Z Z') q.
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
Z, Z': BAut Cantor
q: Z = Z'
I Z' oE (equiv_path Z Z' q +E 1 +E 1) =
(equiv_path Z Z' q +E 1) oE I Z
    revert q; equiv_intro ((equiv_path_sigma_hprop Z Z')^-1) p.
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
Z, Z': BAut Cantor
p: Z = Z'
I Z'
oE (equiv_path Z Z'
      ((equiv_path_sigma_hprop Z Z')^-1 p) +E 1 +E 1) =
(equiv_path Z Z' ((equiv_path_sigma_hprop Z Z')^-1 p) +E
 1) oE I Z
    simpl.
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
Z, Z': BAut Cantor
p: Z = Z'
I Z' oE (equiv_path Z Z' p ..1 +E 1 +E 1) =
(equiv_path Z Z' p ..1 +E 1) oE I Z rewrite <- ap_ff, <- ap_f.
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
Z, Z': BAut Cantor
p: Z = Z'
I Z'
oE equiv_path (f (f Z)).1 (f (f Z')).1
     (ap (fun x : BAut Cantor => f (f x)) p) ..1 =
equiv_path (f Z).1 (f Z').1 (ap f p) ..1 oE I Z
    unfold I.
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
Z, Z': BAut Cantor
p: Z = Z'
equiv_path (f (f Z')).1 (f Z').1 (Ip Z') ..1
oE equiv_path (f (f Z)).1 (f (f Z')).1
     (ap (fun x : BAut Cantor => f (f x)) p) ..1 =
equiv_path (f Z).1 (f Z').1 (ap f p) ..1
oE equiv_path (f (f Z)).1 (f Z).1 (Ip Z) ..1 refine ((equiv_path_pp _ _)^ @ _ @ (equiv_path_pp _ _)).
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
Z, Z': BAut Cantor
p: Z = Z'
equiv_path (Z + Cantor + Cantor) (Z' + Cantor)
  ((ap (fun x : BAut Cantor => f (f x)) p) ..1 @
   (Ip Z') ..1) =
equiv_path (Z + Cantor + Cantor) (Z' + Cantor)
  ((Ip Z) ..1 @ (ap f p) ..1)
    apply ap.
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
Z, Z': BAut Cantor
p: Z = Z'
(ap (fun x : BAut Cantor => f (f x)) p) ..1 @
(Ip Z') ..1 = (Ip Z) ..1 @ (ap f p) ..1
    refine ((pr1_path_pp (ap (f o f) p) (Ip Z'))^ @ _ @ pr1_path_pp _ _).
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
Z, Z': BAut Cantor
p: Z = Z'
(ap (fun x : BAut Cantor => f (f x)) p @ Ip Z') ..1 =
(Ip Z @ ap f p) ..1
    apply ap.
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
Z, Z': BAut Cantor
p: Z = Z'
ap (fun x : BAut Cantor => f (f x)) p @ Ip Z' =
Ip Z @ ap f p apply (concat_Ap Ip).
  Qed.

  (** To show our claim about the action of [I0], we will apply this naturality to the flip automorphism of [Cantor + Cantor].  Here are the images of that automorphism under [f] and [f o f]. *)
  Definition f_flip :=
    equiv_sum_symm Cantor Cantor +E equiv_idmap Cantor.
  Definition ff_flip :=
    (equiv_sum_symm Cantor Cantor +E equiv_idmap Cantor) +E (equiv_idmap Cantor).

  (** The naturality of [I] implies that [I0] commutes with these images of the flip. *)
  Definition I0nat_flip
        (x : ((Cantor + Cantor) + Cantor) + Cantor)
  : I0 (ff_flip x) = f_flip (I0 x)
    := ap10_equiv
         (Inat (f (point (BAut Cantor))) (f (point (BAut Cantor)))
               (equiv_sum_symm Cantor Cantor))
         x.

  (** The value of this is that we can detect which summand an element is in depending on whether or not it is fixed by [f_flip] or [ff_flip]. *)
  Definition f_flip_fixed_iff_inr (x : Cantor + Cantor + Cantor)
  : (f_flip x = x) <-> is_inr x.
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
x: Cantor + Cantor + Cantor
f_flip x = x <-> is_inr x
  Proof.
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
x: Cantor + Cantor + Cantor
f_flip x = x <-> is_inr x
    split; intros p; destruct x as [[c|c]|c]; simpl in p.
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
c: Cantor
p: inl (inr c) = inl (inl c)
is_inr (inl (inl c))
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
c: Cantor
p: inl (inl c) = inl (inr c)
is_inr (inl (inr c))
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
c: Cantor
p: inr c = inr c
is_inr (inr c)
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
c: Cantor
p: Empty
f_flip (inl (inl c)) = inl (inl c)
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
c: Cantor
p: Empty
f_flip (inl (inr c)) = inl (inr c)
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
c: Cantor
p: Unit
f_flip (inr c) = inr c
    -
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
c: Cantor
p: inl (inr c) = inl (inl c)
is_inr (inl (inl c)) apply path_sum_inl in p.
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
c: Cantor
p: inr c = inl c
is_inr (inl (inl c))
      elim (inl_ne_inr _ _ p^).
    -
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
c: Cantor
p: inl (inl c) = inl (inr c)
is_inr (inl (inr c)) apply path_sum_inl in p.
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
c: Cantor
p: inl c = inr c
is_inr (inl (inr c))
      elim (inl_ne_inr _ _ p).
    -
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
c: Cantor
p: inr c = inr c
is_inr (inr c) exact tt.
    -
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
c: Cantor
p: Empty
f_flip (inl (inl c)) = inl (inl c) elim p.
    -
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
c: Cantor
p: Empty
f_flip (inl (inr c)) = inl (inr c) elim p.
    -
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
c: Cantor
p: Unit
f_flip (inr c) = inr c reflexivity.
  Defined.

  Definition ff_flip_fixed_iff_inr
        (x : Cantor + Cantor + Cantor + Cantor)
  : (ff_flip x = x) <-> (is_inr x + is_inl_and is_inr x).
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
x: Cantor + Cantor + Cantor + Cantor
ff_flip x = x <-> is_inr x + is_inl_and is_inr x
  Proof.
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
x: Cantor + Cantor + Cantor + Cantor
ff_flip x = x <-> is_inr x + is_inl_and is_inr x
    split; intros p; destruct x as [[[c|c]|c]|c]; simpl in p.
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
c: Cantor
p: inl (inl (inr c)) = inl (inl (inl c))
is_inr (inl (inl (inl c))) +
is_inl_and is_inr (inl (inl (inl c)))
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
c: Cantor
p: inl (inl (inl c)) = inl (inl (inr c))
is_inr (inl (inl (inr c))) +
is_inl_and is_inr (inl (inl (inr c)))
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
c: Cantor
p: inl (inr c) = inl (inr c)
is_inr (inl (inr c)) + is_inl_and is_inr (inl (inr c))
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
c: Cantor
p: inr c = inr c
is_inr (inr c) + is_inl_and is_inr (inr c)
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
c: Cantor
p: Empty + Empty
ff_flip (inl (inl (inl c))) = inl (inl (inl c))
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
c: Cantor
p: Empty + Empty
ff_flip (inl (inl (inr c))) = inl (inl (inr c))
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
c: Cantor
p: Empty + Unit
ff_flip (inl (inr c)) = inl (inr c)
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
c: Cantor
p: Unit + Empty
ff_flip (inr c) = inr c
    -
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
c: Cantor
p: inl (inl (inr c)) = inl (inl (inl c))
is_inr (inl (inl (inl c))) +
is_inl_and is_inr (inl (inl (inl c))) do 2 apply path_sum_inl in p.
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
c: Cantor
p: inr c = inl c
is_inr (inl (inl (inl c))) +
is_inl_and is_inr (inl (inl (inl c)))
      elim (inl_ne_inr _ _ p^).
    -
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
c: Cantor
p: inl (inl (inl c)) = inl (inl (inr c))
is_inr (inl (inl (inr c))) +
is_inl_and is_inr (inl (inl (inr c))) do 2 apply path_sum_inl in p.
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
c: Cantor
p: inl c = inr c
is_inr (inl (inl (inr c))) +
is_inl_and is_inr (inl (inl (inr c)))
      elim (inl_ne_inr _ _ p).
    -
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
c: Cantor
p: inl (inr c) = inl (inr c)
is_inr (inl (inr c)) + is_inl_and is_inr (inl (inr c)) exact (inr tt).
    -
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
c: Cantor
p: inr c = inr c
is_inr (inr c) + is_inl_and is_inr (inr c) exact (inl tt).
    -
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
c: Cantor
p: Empty + Empty
ff_flip (inl (inl (inl c))) = inl (inl (inl c)) destruct p as [e|e]; elim e.
    -
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
c: Cantor
p: Empty + Empty
ff_flip (inl (inl (inr c))) = inl (inl (inr c)) destruct p as [e|e]; elim e.
    -
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
c: Cantor
p: Empty + Unit
ff_flip (inl (inr c)) = inl (inr c) destruct p as [e|_]; [ elim e | reflexivity ].
    -
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
c: Cantor
p: Unit + Empty
ff_flip (inr c) = inr c destruct p as [_|e]; [ reflexivity | elim e ].
  Defined.

  (** And the naturality guarantees that [I0] preserves fixed points. *)
  Definition I0_fixed_iff_fixed
        (x : Cantor + Cantor + Cantor + Cantor)
  : (ff_flip x = x) <-> (f_flip (I0 x) = I0 x).
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
x: Cantor + Cantor + Cantor + Cantor
ff_flip x = x <-> f_flip (I0 x) = I0 x
  Proof.
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
x: Cantor + Cantor + Cantor + Cantor
ff_flip x = x <-> f_flip (I0 x) = I0 x
    split; intros p.
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
x: Cantor + Cantor + Cantor + Cantor
p: ff_flip x = x
f_flip (I0 x) = I0 x
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
x: Cantor + Cantor + Cantor + Cantor
p: f_flip (I0 x) = I0 x
ff_flip x = x
    -
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
x: Cantor + Cantor + Cantor + Cantor
p: ff_flip x = x
f_flip (I0 x) = I0 x refine ((I0nat_flip x)^ @ ap I0 p).
    -
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
x: Cantor + Cantor + Cantor + Cantor
p: f_flip (I0 x) = I0 x
ff_flip x = x apply (equiv_inj I0).
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
x: Cantor + Cantor + Cantor + Cantor
p: f_flip (I0 x) = I0 x
I0 (ff_flip x) = I0 x
      refine (I0nat_flip x @ p).
  Defined.

  (** Putting it all together, here is the proof of our claim about [I0]. *)
  Definition I0_preserves_inr
        (x : Cantor + Cantor + Cantor + Cantor)
  : (is_inr x + is_inl_and is_inr x) <-> is_inr (I0 x).
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
x: Cantor + Cantor + Cantor + Cantor
is_inr x + is_inl_and is_inr x <-> is_inr (I0 x)
  Proof.
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
x: Cantor + Cantor + Cantor + Cantor
is_inr x + is_inl_and is_inr x <-> is_inr (I0 x)
    refine (iff_compose _ (f_flip_fixed_iff_inr (I0 x))).
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
x: Cantor + Cantor + Cantor + Cantor
is_inr x + is_inl_and is_inr x <->
f_flip (I0 x) = I0 x
    refine (iff_compose _ (I0_fixed_iff_fixed x)).
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
x: Cantor + Cantor + Cantor + Cantor
is_inr x + is_inl_and is_inr x <-> ff_flip x = x
    apply iff_inverse, ff_flip_fixed_iff_inr.
  Defined.

  (** Now we bring quasi-idempotence into play. *)
  Definition J (Z : BAut Cantor)
  : I Z +E 1
    = I (f Z).
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
Z: BAut Cantor
I Z +E 1 = I (f Z)
  Proof.
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
Z: BAut Cantor
I Z +E 1 = I (f Z)
    unfold I; simpl.
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
Z: BAut Cantor
equiv_path (Z + Cantor + Cantor) (Z + Cantor)
  (Ip Z) ..1 +E 1 =
equiv_path (Z + Cantor + Cantor + Cantor)
  (Z + Cantor + Cantor) (Ip (f Z)) ..1
    refine ((ap_f (Ip Z))^ @ _).
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
Z: BAut Cantor
equiv_path (f (f (f Z))).1 (f (f Z)).1
  (ap f (Ip Z)) ..1 =
equiv_path (Z + Cantor + Cantor + Cantor)
  (Z + Cantor + Cantor) (Ip (f Z)) ..1
    do 2 apply ap.
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
Z: BAut Cantor
ap f (Ip Z) = Ip (f Z)
    apply Jp.
  Defined.

  (** We reach a contradiction by showing that the two maps which [J] claims are equal send elements of the third summand of the domain into different summands of the codomain. *)
  Definition impossible : Empty.
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
Empty
  Proof.
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
Empty
    pose (x := inl (inr (fun n => true))
               : ((f (point (BAut Cantor))) + Cantor) + Cantor).
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
x:= inl (inr (fun _ : nat => true))
:
f (point (BAut Cantor)) + Cantor + Cantor: f (point (BAut Cantor)) + Cantor + Cantor
Empty
    apply (not_is_inl_and_inr' (I (f (point (BAut Cantor))) x)).
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
x:= inl (inr (fun _ : nat => true))
:
f (point (BAut Cantor)) + Cantor + Cantor: f (point (BAut Cantor)) + Cantor + Cantor
is_inl (I (f (point (BAut Cantor))) x)
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
x:= inl (inr (fun _ : nat => true))
:
f (point (BAut Cantor)) + Cantor + Cantor: f (point (BAut Cantor)) + Cantor + Cantor
is_inr (I (f (point (BAut Cantor))) x)
    -
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
x:= inl (inr (fun _ : nat => true))
:
f (point (BAut Cantor)) + Cantor + Cantor: f (point (BAut Cantor)) + Cantor + Cantor
is_inl (I (f (point (BAut Cantor))) x) exact (transport is_inl
                       (ap10_equiv (J (point (BAut Cantor))) x) tt).
    -
H: Univalence
Ip: IsPreIdempotent f
Jp: IsQuasiIdempotent f
x:= inl (inr (fun _ : nat => true))
:
f (point (BAut Cantor)) + Cantor + Cantor: f (point (BAut Cantor)) + Cantor + Cantor
is_inr (I (f (point (BAut Cantor))) x) exact (fst (I0_preserves_inr x) (inr tt)).
  Defined.

End Assumptions.
End BAut_Cantor_Idempotent.

(** Let's make the important conclusions available globally. *)

Definition baut_cantor_idem `{Univalence}
: BAut Cantor -> BAut Cantor
  := BAut_Cantor_Idempotent.f.

Definition preidem_baut_cantor_idem `{Univalence}
: IsPreIdempotent baut_cantor_idem
  := BAut_Cantor_Idempotent.preidem_f.

Definition not_qidem_baut_cantor_idem `{Univalence}
: ~ { I : IsPreIdempotent baut_cantor_idem
        & IsQuasiIdempotent baut_cantor_idem }
  := fun IJ => BAut_Cantor_Idempotent.impossible IJ.1 IJ.2.