Timings for Bool.v
(* -*- mode: coq; mode: visual-line -*- *)
Require Import HoTT.Basics HoTT.Types.
Require Import HoTT.Truncations.Core HoTT.Truncations.Connectedness.
Require Import Spaces.BAut.
Require Import Pointed.Core.
Local Open Scope trunc_scope.
Local Open Scope path_scope.
Local Open Scope pointed_scope.
Section AssumeUnivalence.
(** ** Nontrivial central homotopy *)
(** The equivalence [Bool <~> (Bool <~> Bool)], and particularly its consequence [abelian_aut_bool], implies that [BAut Bool] has a nontrivial center. *)
Definition negb_center_baut_bool
: forall (Z:BAut Bool), Z = Z.
apply center_baut; try exact _.
intros g; apply abelian_aut_bool.
Definition nontrivial_negb_center_baut_bool
: negb_center_baut_bool <> (fun Z => idpath Z).
pose (p := ap10_equiv
((ap (center_baut Bool))^-1
(oops @ (id_center_baut Bool)^))..1 true).
(** In particular, every element of [BAut Bool] has a canonical flip automorphism. *)
Definition negb_baut_bool (Z : BAut Bool) : Z <~> Z
:= equiv_path Z Z (negb_center_baut_bool Z)..1.
Definition negb_baut_bool_ne_idmap (Z : BAut Bool)
: negb_baut_bool Z <> equiv_idmap Z.
apply nontrivial_negb_center_baut_bool.
apply path_forall; intros Z'.
pose (p := merely_path_component Z Z').
unfold negb_baut_bool in oops.
apply moveL_equiv_V in oops.
refine (_ @ ap (equiv_path_sigma_hprop _ _)
(oops @ path_universe_1) @ _).
refine (eisretr (equiv_path_sigma_hprop Z Z) _).
apply moveR_equiv_M; reflexivity.
(** If [Z] is [Bool], then the flip is the usual one. *)
Definition negb_baut_bool_bool_negb
: negb_baut_bool pt = equiv_negb.
pose (c := aut_bool_idmap_or_negb (negb_baut_bool pt)).
pose (negb_baut_bool_ne_idmap pt p).
Definition ap_pr1_negb_baut_bool_bool
: (negb_center_baut_bool pt)..1 = path_universe negb.
apply negb_baut_bool_bool_negb.
(** Moreover, we can show that every automorphism of a [Z : BAut Bool] must be either the flip or the identity. *)
Definition aut_baut_bool_idmap_or_negb (Z : BAut Bool) (e : Z <~> Z)
: (e = equiv_idmap Z) + (e = negb_baut_bool Z).
assert (IsHProp ((e = equiv_idmap Z) + (e = negb_baut_bool Z))).
apply ishprop_sum; try exact _.
intros p q; exact (negb_baut_bool_ne_idmap Z (q^ @ p)).
case (aut_bool_idmap_or_negb e).
exact (q @ negb_baut_bool_bool_negb^).
Global Instance isminusoneconnected_baut_bool `{Funext} (Z : BAut Bool)
: IsConnected (-1) Z.
apply contr_inhabited_hprop; try exact _.
Definition merely_inhab_baut_bool `{Funext} (Z : BAut Bool)
: merely Z
:= center (merely Z).
(** ** Equivalence types *)
(** As soon as an element of [BAut Bool] is inhabited, it is (purely) equivalent to [Bool]. (Of course, every element of [BAut Bool] is *merely* inhabited, since [Bool] is.) In fact, it is equivalent in two canonical ways.
First we define the function that will be the equivalence. *)
Definition inhab_baut_bool_from_bool (t : Bool)
(Z : BAut Bool) (z : Z)
: Bool -> Z
:= fun b => if t then
if b then z else negb_baut_bool Z z
else
if b then negb_baut_bool Z z else z.
(** We compute this in the case when [Z] is [Bool]. *)
Definition inhab_baut_bool_from_bool_bool (t : Bool)
: inhab_baut_bool_from_bool t pt =
fun (z : point (BAut Bool)) (b : Bool) =>
if t then
if b then z else negb z
else
if b then negb z else z.
apply path_forall; intros z'; simpl in z'.
apply path_forall; intros b.
destruct z', b, t; simpl;
try reflexivity;
try apply (ap10_equiv negb_baut_bool_bool_negb).
(** Now we show that it is an equivalence. *)
Global Instance isequiv_inhab_baut_bool_from_bool (t : Bool)
(Z : BAut Bool) (z : Z)
: IsEquiv (inhab_baut_bool_from_bool t Z z).
refine (transport IsEquiv (ap10 (inhab_baut_bool_from_bool_bool t)^ z) _).
simpl in z; destruct z, t; simpl.
refine (isequiv_homotopic idmap _); intros []; reflexivity.
refine (isequiv_homotopic idmap _); intros []; reflexivity.
Definition equiv_inhab_baut_bool_bool (t : Bool)
(Z : BAut Bool) (z : Z)
: Bool <~> Z
:= Build_Equiv _ _ (inhab_baut_bool_from_bool t Z z) _.
Definition path_baut_bool_inhab (Z : BAut Bool) (z : Z)
: (point (BAut Bool)) = Z.
exact (equiv_inhab_baut_bool_bool true Z z).
(** [true] is a choice! *)
(** In fact, the map sending [z:Z] to this equivalence [Bool <~> Z] is also an equivalence. To assist with computing the result when [Z] is [Bool], we prove it with an extra parameter first. *)
Definition isequiv_equiv_inhab_baut_bool_bool_lemma
(t : Bool) (Z : BAut Bool) (m : merely (pt = Z))
: IsEquiv (equiv_inhab_baut_bool_bool t Z).
refine (isequiv_adjointify _ (fun (e : Bool <~> Bool) => e t) _ _).
refine (ap10 (inhab_baut_bool_from_bool_bool t) (e t) @ _).
apply path_arrow; intros []; destruct t.
refine (abelian_aut_bool equiv_negb e false).
refine (abelian_aut_bool equiv_negb e true).
refine (ap10 (ap10 (inhab_baut_bool_from_bool_bool t) z) t @ _).
Global Instance isequiv_equiv_inhab_baut_bool_bool
(t : Bool) (Z : BAut Bool)
: IsEquiv (equiv_inhab_baut_bool_bool t Z).
exact (isequiv_equiv_inhab_baut_bool_bool_lemma t Z
(merely_path_component _ _)).
(** The names are getting pretty ridiculous; below we suggest a better name for this. *)
Definition equiv_equiv_inhab_baut_bool_bool (t : Bool)
(Z : BAut Bool)
: Z <~> (Bool <~> Z)
:= Build_Equiv _ _ (equiv_inhab_baut_bool_bool t Z) _.
(** We compute its inverse in the case of [Bool]. *)
Definition equiv_equiv_inhab_baut_bool_bool_bool_inv (t : Bool)
(e : Bool <~> Bool)
: equiv_inverse (equiv_equiv_inhab_baut_bool_bool t pt) e = e t.
pose (alt := Build_Equiv _ _ (equiv_inhab_baut_bool_bool t pt)
(isequiv_equiv_inhab_baut_bool_bool_lemma
t pt (tr 1))).
assert (p : equiv_equiv_inhab_baut_bool_bool t pt = alt).
apply (ap (fun i => Build_Equiv _ _ _ i)).
apply (ap (isequiv_equiv_inhab_baut_bool_bool_lemma t pt)).
exact (ap10_equiv (ap equiv_inverse p) e).
(** ** Group structure *)
(** Homotopically, [BAut Bool] is a [K(Z/2,1)]. In particular, it has a (coherent) abelian group structure induced from that of [Z/2]. With our definition of [BAut Bool], we can construct this operation as follows. *)
Definition baut_bool_pairing : BAut Bool -> BAut Bool -> BAut Bool.
exact (path_universe equiv_bool_aut_bool).
Declare Scope baut_bool_scope.
Notation "Z ** W" := (baut_bool_pairing Z W) : baut_bool_scope.
Local Open Scope baut_bool_scope.
(** Now [equiv_equiv_inhab_baut_bool_bool] is revealed as simply the left unit law of this pairing. *)
Definition baut_bool_pairing_1Z Z : pt ** Z = Z.
apply path_baut, equiv_inverse, equiv_equiv_inhab_baut_bool_bool.
(** The pairing is obviously symmetric. *)
Definition baut_bool_pairing_symm Z W : Z ** W = W ** Z.
apply path_baut, equiv_equiv_inverse.
(** Whence we get the right unit law as well. *)
Definition baut_bool_pairing_Z1 Z : Z ** pt = Z
:= baut_bool_pairing_symm Z pt @ baut_bool_pairing_1Z Z.
(** Every element is its own inverse. *)
Definition baut_bool_pairing_ZZ Z : Z ** Z = pt.
apply symmetry, path_baut_bool_inhab.
(** A choice! Could be the flip. *)
(** Associativity is easiest to think about in terms of "curried 2-variable equivalences". We start with some auxiliary lemmas. *)
Definition baut_bool_pairing_ZZ_Z_symm_part1 {Y Z W}
(e : Y ** (Z ** W)) (z : Z)
: Y ** W.
simple refine (equiv_adjointify _ _ _ _).
destruct (path_baut_bool_inhab W w).
destruct (path_baut_bool_inhab Z z).
(** It might be tempting to just say [e^-1 (equiv_idmap _)] here, but for the rest of the proof to work, we actually need to choose between [idmap] and [negb] based on whether [z] and [w] are equal or not. *)
exact (e^-1 (equiv_idmap _)).
destruct (path_baut_bool_inhab W w).
destruct (path_baut_bool_inhab Z z).
destruct z,w; simpl; refine (ap10_equiv (eisretr e _) _).
destruct (path_baut_bool_inhab Y y).
destruct (path_baut_bool_inhab Z z).
destruct (path_baut_bool_inhab W (e y z)).
case (dec (z = e y z)); intros p; apply moveR_equiv_V;
destruct (aut_bool_idmap_or_negb (e y)) as [q|q].
case (not_fixed_negb z (p @ ap10_equiv q z)^).
case (p (ap10_equiv q z)^).
Definition baut_bool_pairing_ZZ_Z_symm_lemma {Y Z W}
(e : Y ** (Z ** W)) (f : Y ** W)
: merely Y -> Z.
pose (k := (fun y => (e y)^-1 (f y))).
refine (merely_rec_hset k); intros y1 y2.
destruct (path_baut_bool_inhab Y y1).
destruct (path_baut_bool_inhab W (f y1)).
destruct (path_baut_bool_inhab Z (k y1)).
destruct (aut_bool_idmap_or_negb f) as [p|p];
refine (ap (e y1)^-1 (ap10_equiv p y1) @ _);
refine (_ @ (ap (e y2)^-1 (ap10_equiv p y2))^);
clear p f k; simpl.
destruct (dec (y1=y2)) as [p|p].
exact (ap (fun y => (e y)^-1 y) p).
destruct (aut_bool_idmap_or_negb (e y1)) as [q1|q1];
destruct (aut_bool_idmap_or_negb (e y2)) as [q2|q2].
case (p ((ap e)^-1 (q1 @ q2^))).
exact (negb_ne (fun r => p r^)).
case (p ((ap e)^-1 (q1 @ q2^))).
destruct (dec (y1=y2)) as [p|p].
exact (ap (fun y => (e y)^-1 (negb y)) p).
destruct (aut_bool_idmap_or_negb (e y1)) as [q1|q1];
destruct (aut_bool_idmap_or_negb (e y2)) as [q2|q2].
case (p ((ap e)^-1 (q1 @ q2^))).
exact (negb_ne (fun r => p ((ap negb)^-1 r))).
exact (negb_ne (fun r => p ((ap negb)^-1 r)^)).
case (p ((ap e)^-1 (q1 @ q2^))).
Definition baut_bool_pairing_ZZ_Z_symm_map Y Z W
: Y ** (Z ** W) -> Z ** (Y ** W).
simple refine (equiv_adjointify (baut_bool_pairing_ZZ_Z_symm_part1 e)
_ _ _).
exact (baut_bool_pairing_ZZ_Z_symm_lemma e f
(merely_inhab_baut_bool Y)).
apply path_equiv, path_arrow; intros y.
change ((e y)
(baut_bool_pairing_ZZ_Z_symm_lemma e f
(merely_inhab_baut_bool Y)) = f y).
refine (ap (e y o baut_bool_pairing_ZZ_Z_symm_lemma e f)
(path_ishprop _ (tr y)) @ _).
assert (IsHSet Z) by exact _.
refine (Trunc_rec _ (merely_inhab_baut_bool Y)); intros y.
refine (ap (baut_bool_pairing_ZZ_Z_symm_lemma e _)
(path_ishprop _ (tr y)) @ _).
Definition baut_bool_pairing_ZZ_Z_symm_inv Y Z W
: baut_bool_pairing_ZZ_Z_symm_map Y Z W
o baut_bool_pairing_ZZ_Z_symm_map Z Y W
== idmap.
apply path_equiv, path_arrow; intros z.
apply path_equiv, path_arrow; intros y.
Definition baut_bool_pairing_ZZ_Z_symm Y Z W
: Y ** (Z ** W) <~> Z ** (Y ** W).
refine (equiv_adjointify
(baut_bool_pairing_ZZ_Z_symm_map Y Z W)
(baut_bool_pairing_ZZ_Z_symm_map Z Y W)
(baut_bool_pairing_ZZ_Z_symm_inv Y Z W)
(baut_bool_pairing_ZZ_Z_symm_inv Z Y W)).
(** Finally, we can prove associativity. *)
Definition baut_bool_pairing_ZZ_Z Z W Y
: (Z ** W) ** Y = Z ** (W ** Y).
refine (baut_bool_pairing_symm (Z ** W) Y @ _).
refine (_ @ ap (fun X => Z ** X) (baut_bool_pairing_symm Y W)).
apply path_baut, baut_bool_pairing_ZZ_Z_symm.
(** Since [BAut Bool] is not a set, we ought to have some coherence for these operations too, but we'll leave that for another time. *)
(** ** Automorphisms of [BAut Bool] *)
(** Interestingly, like [Bool] itself, [BAut Bool] is equivalent to its own automorphism group. *)
(** An initial lemma: every automorphism of [BAut Bool] and its inverse are "adjoint" with respect to the pairing. *)
Definition aut_baut_bool_moveR_pairing_V
(e : BAut Bool <~> BAut Bool) (Z W : BAut Bool)
: (e^-1 Z ** W) = (Z ** e W).
refine ((equiv_equiv_path _ _) oE _ oE (equiv_equiv_path _ _)^-1).
refine (_ oE (@equiv_moveL_equiv_M _ _ e _ W Z) oE _).
apply equiv_inverse, equiv_path_sigma_hprop.
apply equiv_path_sigma_hprop.
Definition equiv_baut_bool_aut_baut_bool
: BAut Bool <~> (BAut Bool <~> BAut Bool).
simple refine (equiv_adjointify _ _ _ _).
refine (equiv_involution (fun W => Z ** W) _).
refine ((baut_bool_pairing_ZZ_Z Z Z W)^ @ _).
refine (_ @ baut_bool_pairing_1Z W).
apply (ap (fun Y => Y ** W)).
apply baut_bool_pairing_ZZ.
apply path_equiv, path_arrow; intros Z; simpl.
refine (aut_baut_bool_moveR_pairing_V e pt Z @ _).
apply baut_bool_pairing_1Z.
apply baut_bool_pairing_Z1.
(** ** [BAut (BAut Bool)] *)
(** Putting all of this together, we can construct a nontrivial 2-central element of [BAut (BAut Bool)]. *)
Definition center_baut_bool_central
(g : BAut Bool <~> BAut Bool) (W : BAut Bool)
: ap g (negb_center_baut_bool W) = negb_center_baut_bool (g W).
revert g; equiv_intro equiv_baut_bool_aut_baut_bool Z.
refine (_ @ apD negb_center_baut_bool (baut_bool_pairing_1Z pt)^).
rewrite transport_paths_lr, inv_V.
exact (concat_A1p baut_bool_pairing_1Z (negb_center_baut_bool pt)).
Definition negb_center2_baut_baut_bool
: forall B : BAut (BAut Bool), (idpath B) = (idpath B).
refine (center2_baut (BAut Bool) _).
exists negb_center_baut_bool.
apply center_baut_bool_central.
Definition nontrivial_negb_center_baut_baut_bool
: negb_center2_baut_baut_bool <> (fun Z => idpath (idpath Z)).
exact (nontrivial_negb_center_baut_bool
(((ap (center2_baut (BAut Bool)))^-1
(oops @ (id_center2_baut (BAut Bool))^))..1)).