Timings for Cantor.v
(* -*- mode: coq; mode: visual-line -*- *)
Require Import HoTT.Basics HoTT.Types.
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.
Definition f : BAut Cantor -> BAut Cantor.
(** Here is the important part of this definition. *)
exists (Z + Cantor)%type.
(** 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.
apply path_universe_uncurried.
refine (equiv_cantor_fold oE _).
refine (equiv_path _ _ e +E 1).
(** For the pre-idempotence of [f], the main point is again the existence of the equivalence [fold_cantor]. *)
Definition preidem_f : IsPreIdempotent f.
refine (_ oE equiv_sum_assoc Z Cantor Cantor).
apply (1 +E equiv_cantor_fold).
(** 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.
apply path_equiv, path_arrow.
intros [z|a]; reflexivity.
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.
apply path_equiv, path_arrow.
intros [[z|a]|a]; reflexivity.
(** 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.
revert e; equiv_intro (equiv_path Z Z') q.
revert q; equiv_intro ((equiv_path_sigma_hprop Z Z')^-1) p.
rewrite <- ap_ff, <- ap_f.
refine ((equiv_path_pp _ _)^ @ _ @ (equiv_path_pp _ _)).
refine ((pr1_path_pp (ap (f o f) p) (Ip Z'))^ @ _ @ pr1_path_pp _ _).
(** 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.
split; intros p; destruct x as [[c|c]|c]; simpl in p.
elim (inl_ne_inr _ _ p^).
Definition ff_flip_fixed_iff_inr
(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.
do 2 apply path_sum_inl in p.
elim (inl_ne_inr _ _ p^).
do 2 apply path_sum_inl in p.
destruct p as [e|e]; elim e.
destruct p as [e|e]; elim e.
destruct p as [e|_]; [ elim e | reflexivity ].
destruct p as [_|e]; [ reflexivity | elim e ].
(** 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).
refine ((I0nat_flip x)^ @ ap I0 p).
refine (I0nat_flip x @ p).
(** 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).
refine (iff_compose _ (f_flip_fixed_iff_inr (I0 x))).
refine (iff_compose _ (I0_fixed_iff_fixed x)).
apply iff_inverse, ff_flip_fixed_iff_inr.
(** Now we bring quasi-idempotence into play. *)
Definition J (Z : BAut Cantor)
: I Z +E 1
= I (f Z).
refine ((ap_f (Ip Z))^ @ _).
(** 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.
pose (x := inl (inr (fun n => true))
: ((f (point (BAut Cantor))) + Cantor) + Cantor).
apply (not_is_inl_and_inr' (I (f (point (BAut Cantor))) x)).
exact (transport is_inl
(ap10_equiv (J (point (BAut Cantor))) x) tt).
exact (fst (I0_preserves_inr x) (inr tt)).
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.