Require Import HoTT.Basics HoTT.Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Truncations.
Require Import Universes.BAut.
Require Import Pointed.Core.

Local Open Scope trunc_scope.
Local Open Scope path_scope.
Local Open Scope pointed_scope.

(** * BAut(Bool) *)

Section AssumeUnivalence.
  Context `{Univalence}.

  (** ** 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.
H: Univalence
forall Z : BAut Bool, Z = Z
  Proof.
H: Univalence
forall Z : BAut Bool, Z = Z
    apply center_baut; try exact _.
H: Univalence
{f : Bool <~> Bool &
forall g : Bool <~> Bool,
(fun x : Bool => g (f x)) == (fun x : Bool => f (g x))}
    exists equiv_negb.
H: Univalence
forall g : Bool <~> Bool,
(fun x : Bool => g (equiv_negb x)) ==
(fun x : Bool => equiv_negb (g x))
    intros g; apply abelian_aut_bool.
  Defined.

  Definition nontrivial_negb_center_baut_bool
  : negb_center_baut_bool <> (fun Z => idpath Z).
H: Univalence
negb_center_baut_bool <> (fun Z : BAut Bool => 1)
  Proof.
H: Univalence
negb_center_baut_bool <> (fun Z : BAut Bool => 1)
    intros oops.
H: Univalence
oops: negb_center_baut_bool =
(fun Z : BAut Bool => 1)
Empty
    pose (p := ap10_equiv
                 ((ap (center_baut Bool))^-1
                  (oops @ (id_center_baut Bool)^))..1 true).
H: Univalence
oops: negb_center_baut_bool =
(fun Z : BAut Bool => 1)
p:= ap10_equiv
  ((ap (center_baut Bool))^-1
     (oops @ (id_center_baut Bool)^)) ..1 true: (equiv_negb;
fun g : Bool <~> Bool =>
abelian_aut_bool g equiv_negb).1 true =
(1%equiv; fun (g : Bool <~> Bool) (x : Bool) => 1).1
  true
Empty
    exact (false_ne_true p).
  Defined.

  (** 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.
H: Univalence
Z: BAut Bool
negb_baut_bool Z <> 1%equiv
  Proof.
H: Univalence
Z: BAut Bool
negb_baut_bool Z <> 1%equiv
    intros oops.
H: Univalence
Z: BAut Bool
oops: negb_baut_bool Z = 1%equiv
Empty
    apply nontrivial_negb_center_baut_bool.
H: Univalence
Z: BAut Bool
oops: negb_baut_bool Z = 1%equiv
negb_center_baut_bool = (fun Z : BAut Bool => 1)
    apply path_forall; intros Z'.
H: Univalence
Z: BAut Bool
oops: negb_baut_bool Z = 1%equiv
Z': BAut Bool
negb_center_baut_bool Z' = 1
    pose (p := merely_path_component Z Z').
H: Univalence
Z: BAut Bool
oops: negb_baut_bool Z = 1%equiv
Z': BAut Bool
p:= merely_path_component Z Z': merely (Z = Z')
negb_center_baut_bool Z' = 1
    clearbody p.
H: Univalence
Z: BAut Bool
oops: negb_baut_bool Z = 1%equiv
Z': BAut Bool
p: merely (Z = Z')
negb_center_baut_bool Z' = 1 strip_truncations.
H: Univalence
Z: BAut Bool
oops: negb_baut_bool Z = 1%equiv
Z': BAut Bool
p: Z = Z'
negb_center_baut_bool Z' = 1
    destruct p.
H: Univalence
Z: BAut Bool
oops: negb_baut_bool Z = 1%equiv
negb_center_baut_bool Z = 1
    unfold negb_baut_bool in oops.
H: Univalence
Z: BAut Bool
oops: equiv_path Z Z (negb_center_baut_bool Z) ..1 =
1%equiv
negb_center_baut_bool Z = 1
    apply moveL_equiv_V in oops.
H: Univalence
Z: BAut Bool
oops: (negb_center_baut_bool Z) ..1 =
(equiv_path Z Z)^-1 1%equiv
negb_center_baut_bool Z = 1
    refine (_ @ ap (equiv_path_sigma_hprop _ _)
                   (oops @ path_universe_1) @ _).
H: Univalence
Z: BAut Bool
oops: (negb_center_baut_bool Z) ..1 =
(equiv_path Z Z)^-1 1%equiv
negb_center_baut_bool Z =
equiv_path_sigma_hprop Z Z
  (negb_center_baut_bool Z) ..1
H: Univalence
Z: BAut Bool
oops: (negb_center_baut_bool Z) ..1 =
(equiv_path Z Z)^-1 1%equiv
equiv_path_sigma_hprop Z Z 1 = 1
    -
H: Univalence
Z: BAut Bool
oops: (negb_center_baut_bool Z) ..1 =
(equiv_path Z Z)^-1 1%equiv
negb_center_baut_bool Z =
equiv_path_sigma_hprop Z Z
  (negb_center_baut_bool Z) ..1 symmetry.
H: Univalence
Z: BAut Bool
oops: (negb_center_baut_bool Z) ..1 =
(equiv_path Z Z)^-1 1%equiv
equiv_path_sigma_hprop Z Z
  (negb_center_baut_bool Z) ..1 =
negb_center_baut_bool Z
      exact (eisretr (equiv_path_sigma_hprop Z Z) _).
    -
H: Univalence
Z: BAut Bool
oops: (negb_center_baut_bool Z) ..1 =
(equiv_path Z Z)^-1 1%equiv
equiv_path_sigma_hprop Z Z 1 = 1 apply moveR_equiv_M; reflexivity.
  Defined.

  (** If [Z] is [Bool], then the flip is the usual one. *)
  Definition negb_baut_bool_bool_negb
  : negb_baut_bool pt = equiv_negb.
H: Univalence
negb_baut_bool pt = equiv_negb
  Proof.
H: Univalence
negb_baut_bool pt = equiv_negb
    pose (c := aut_bool_idmap_or_negb (negb_baut_bool pt)).
H: Univalence
c:= aut_bool_idmap_or_negb (negb_baut_bool pt): (negb_baut_bool pt = 1%equiv) +
(negb_baut_bool pt = equiv_negb)
negb_baut_bool pt = equiv_negb
    destruct c.
H: Univalence
p: negb_baut_bool pt = 1%equiv
negb_baut_bool pt = equiv_negb
H: Univalence
p: negb_baut_bool pt = equiv_negb
negb_baut_bool pt = equiv_negb
    -
H: Univalence
p: negb_baut_bool pt = 1%equiv
negb_baut_bool pt = equiv_negb pose (negb_baut_bool_ne_idmap pt p).
H: Univalence
p: negb_baut_bool pt = 1%equiv
e:= negb_baut_bool_ne_idmap pt p: Empty
negb_baut_bool pt = equiv_negb
      contradiction.
    -
H: Univalence
p: negb_baut_bool pt = equiv_negb
negb_baut_bool pt = equiv_negb assumption.
  Defined.

  Definition ap_pr1_negb_baut_bool_bool
  : (negb_center_baut_bool pt)..1 = path_universe negb.
H: Univalence
(negb_center_baut_bool pt) ..1 = path_universe negb
  Proof.
H: Univalence
(negb_center_baut_bool pt) ..1 = path_universe negb
    apply moveL_equiv_V.
H: Univalence
equiv_path Bool Bool (negb_center_baut_bool pt) ..1 =
{| equiv_fun := negb; equiv_isequiv := isequiv_negb |}
    exact negb_baut_bool_bool_negb.
  Defined.

  (** 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).
H: Univalence
Z: BAut Bool
e: Z <~> Z
(e = 1%equiv) + (e = negb_baut_bool Z)
  Proof.
H: Univalence
Z: BAut Bool
e: Z <~> Z
(e = 1%equiv) + (e = negb_baut_bool Z)
    assert (IsHProp ((e = equiv_idmap Z) + (e = negb_baut_bool Z))).
H: Univalence
Z: BAut Bool
e: Z <~> Z
IsHProp ((e = 1%equiv) + (e = negb_baut_bool Z))
H: Univalence
Z: BAut Bool
e: Z <~> Z
X: IsHProp ((e = 1%equiv) + (e = negb_baut_bool Z))
(e = 1%equiv) + (e = negb_baut_bool Z)
    {
H: Univalence
Z: BAut Bool
e: Z <~> Z
IsHProp ((e = 1%equiv) + (e = negb_baut_bool Z)) apply ishprop_sum; try exact _.
H: Univalence
Z: BAut Bool
e: Z <~> Z
e = 1%equiv -> e = negb_baut_bool Z -> Empty
      intros p q; exact (negb_baut_bool_ne_idmap Z (q^ @ p)). }
H: Univalence
Z: BAut Bool
e: Z <~> Z
X: IsHProp ((e = 1%equiv) + (e = negb_baut_bool Z))
(e = 1%equiv) + (e = negb_baut_bool Z)
    baut_reduce.
H: Univalence
e: pt <~> pt
X: IsHProp ((e = 1%equiv) + (e = negb_baut_bool pt))
(e = 1%equiv) + (e = negb_baut_bool pt)
    case (aut_bool_idmap_or_negb e).
H: Univalence
e: pt <~> pt
X: IsHProp ((e = 1%equiv) + (e = negb_baut_bool pt))
e = 1%equiv -> (e = 1%equiv) + (e = negb_baut_bool pt)
H: Univalence
e: pt <~> pt
X: IsHProp ((e = 1%equiv) + (e = negb_baut_bool pt))
e = equiv_negb ->
(e = 1%equiv) + (e = negb_baut_bool pt)
    -
H: Univalence
e: pt <~> pt
X: IsHProp ((e = 1%equiv) + (e = negb_baut_bool pt))
e = 1%equiv -> (e = 1%equiv) + (e = negb_baut_bool pt) intros p; exact (inl p).
    -
H: Univalence
e: pt <~> pt
X: IsHProp ((e = 1%equiv) + (e = negb_baut_bool pt))
e = equiv_negb ->
(e = 1%equiv) + (e = negb_baut_bool pt) intros q; apply inr.
H: Univalence
e: pt <~> pt
X: IsHProp ((e = 1%equiv) + (e = negb_baut_bool pt))
q: e = equiv_negb
e = negb_baut_bool pt
      exact (q @ negb_baut_bool_bool_negb^).
  Defined.

  (** ** Connectedness *)

  #[export] Instance isminusoneconnected_baut_bool `{Funext} (Z : BAut Bool)
  : IsConnected (-1) Z.
H: Univalence
H0: Funext
Z: BAut Bool
IsConnected (Tr (-1)) Z
  Proof.
H: Univalence
H0: Funext
Z: BAut Bool
IsConnected (Tr (-1)) Z
    baut_reduce.
H: Univalence
H0: Funext
IsConnected (Tr (-1)) pt
    rapply contr_inhabited_hprop.
H: Univalence
H0: Funext
Tr (-1) pt
    exact (tr true).
  Defined.

  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.
H: Univalence
t: Bool
inhab_baut_bool_from_bool t pt =
(fun (z : pt) (b : Bool) =>
 if t
 then if b then z else negb z
 else if b then negb z else z)
  Proof.
H: Univalence
t: Bool
inhab_baut_bool_from_bool t pt =
(fun (z : pt) (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'.
H: Univalence
t, z': Bool
inhab_baut_bool_from_bool t pt z' =
(fun b : Bool =>
 if t
 then if b then z' else negb z'
 else if b then negb z' else z')
    apply path_forall; intros b.
H: Univalence
t, z', b: Bool
inhab_baut_bool_from_bool t pt z' b =
(if t
 then if b then z' else negb z'
 else if b then negb z' else z')
    destruct z', b, t; simpl;
    try reflexivity;
    try apply (ap10_equiv negb_baut_bool_bool_negb).
  Defined.

  (** Now we show that it is an equivalence. *)
  #[export] Instance isequiv_inhab_baut_bool_from_bool (t : Bool)
         (Z : BAut Bool) (z : Z)
  : IsEquiv (inhab_baut_bool_from_bool t Z z).
H: Univalence
t: Bool
Z: BAut Bool
z: Z
IsEquiv (inhab_baut_bool_from_bool t Z z)
  Proof.
H: Univalence
t: Bool
Z: BAut Bool
z: Z
IsEquiv (inhab_baut_bool_from_bool t Z z)
    baut_reduce.
H: Univalence
t: Bool
z: pt
IsEquiv (inhab_baut_bool_from_bool t pt z)
    refine (transport IsEquiv (ap10 (inhab_baut_bool_from_bool_bool t)^ z) _).
H: Univalence
t: Bool
z: pt
IsEquiv
  (fun b : Bool =>
   if t
   then if b then z else negb z
   else if b then negb z else z)
    simpl in z; destruct z, t; simpl.
H: Univalence
IsEquiv (fun b : Bool => if b then true else false)
H: Univalence
IsEquiv (fun b : Bool => if b then false else true)
H: Univalence
IsEquiv (fun b : Bool => if b then false else true)
H: Univalence
IsEquiv (fun b : Bool => if b then true else false)
    -
H: Univalence
IsEquiv (fun b : Bool => if b then true else false) refine (isequiv_homotopic idmap _); intros []; reflexivity.
    -
H: Univalence
IsEquiv (fun b : Bool => if b then false else true) exact isequiv_negb.
    -
H: Univalence
IsEquiv (fun b : Bool => if b then false else true) exact isequiv_negb.
    -
H: Univalence
IsEquiv (fun b : Bool => if b then true else false) refine (isequiv_homotopic idmap _); intros []; reflexivity.
  Defined.

  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.
H: Univalence
Z: BAut Bool
z: Z
pt = Z
  Proof.
H: Univalence
Z: BAut Bool
z: Z
pt = Z
    apply path_baut.
H: Univalence
Z: BAut Bool
z: Z
pt <~> Z
    exact (equiv_inhab_baut_bool_bool true Z z). (** [true] is a choice! *)
  Defined.

  (** 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).
H: Univalence
t: Bool
Z: BAut Bool
m: merely (pt = Z)
IsEquiv (equiv_inhab_baut_bool_bool t Z)
  Proof.
H: Univalence
t: Bool
Z: BAut Bool
m: merely (pt = Z)
IsEquiv (equiv_inhab_baut_bool_bool t Z)
    strip_truncations.
H: Univalence
t: Bool
Z: BAut Bool
m: pt = Z
IsEquiv (equiv_inhab_baut_bool_bool t Z) destruct m.
H: Univalence
t: Bool
IsEquiv (equiv_inhab_baut_bool_bool t pt)
    refine (isequiv_adjointify _ (fun (e : Bool <~> Bool) => e t) _ _).
H: Univalence
t: Bool
(fun x : Bool <~> Bool =>
 equiv_inhab_baut_bool_bool t pt (x t)) == idmap
H: Univalence
t: Bool
(fun x : Bool => equiv_inhab_baut_bool_bool t pt x t) ==
idmap
    +
H: Univalence
t: Bool
(fun x : Bool <~> Bool =>
 equiv_inhab_baut_bool_bool t pt (x t)) == idmap intros e.
H: Univalence
t: Bool
e: Bool <~> Bool
equiv_inhab_baut_bool_bool t pt (e t) = e
      apply path_equiv.
H: Univalence
t: Bool
e: Bool <~> Bool
equiv_inhab_baut_bool_bool t pt (e t) = e
      refine (ap10 (inhab_baut_bool_from_bool_bool t) (e t) @ _).
H: Univalence
t: Bool
e: Bool <~> Bool
(fun b : Bool =>
 if t
 then if b then e t else negb (e t)
 else if b then negb (e t) else e t) = e
      apply path_arrow; intros []; destruct t.
H: Univalence
e: Bool <~> Bool
e true = e true
H: Univalence
e: Bool <~> Bool
negb (e false) = e true
H: Univalence
e: Bool <~> Bool
negb (e true) = e false
H: Univalence
e: Bool <~> Bool
e false = e false
      *
H: Univalence
e: Bool <~> Bool
e true = e true reflexivity.
      *
H: Univalence
e: Bool <~> Bool
negb (e false) = e true exact (abelian_aut_bool equiv_negb e false).
      *
H: Univalence
e: Bool <~> Bool
negb (e true) = e false exact (abelian_aut_bool equiv_negb e true).
      *
H: Univalence
e: Bool <~> Bool
e false = e false reflexivity.
    +
H: Univalence
t: Bool
(fun x : Bool => equiv_inhab_baut_bool_bool t pt x t) ==
idmap intros z.
H: Univalence
t, z: Bool
equiv_inhab_baut_bool_bool t pt z t = z
      refine (ap10 (ap10 (inhab_baut_bool_from_bool_bool t) z) t @ _).
H: Univalence
t, z: Bool
(if t
 then if t then z else negb z
 else if t then negb z else z) = z
      destruct t; reflexivity.
  Defined.

  #[export] Instance isequiv_equiv_inhab_baut_bool_bool
         (t : Bool) (Z : BAut Bool)
  : IsEquiv (equiv_inhab_baut_bool_bool t Z).
H: Univalence
t: Bool
Z: BAut Bool
IsEquiv (equiv_inhab_baut_bool_bool t Z)
  Proof.
H: Univalence
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 _ _)).
  Defined.

  (** 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.
H: Univalence
t: Bool
e: Bool <~> Bool
(equiv_equiv_inhab_baut_bool_bool t pt)^-1%equiv e =
e t
  Proof.
H: Univalence
t: Bool
e: Bool <~> Bool
(equiv_equiv_inhab_baut_bool_bool t pt)^-1%equiv 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))).
H: Univalence
t: Bool
e: Bool <~> Bool
alt:= {|
  equiv_fun := equiv_inhab_baut_bool_bool t pt;
  equiv_isequiv :=
    isequiv_equiv_inhab_baut_bool_bool_lemma t pt
      (tr 1)
|}: pt <~> (Bool <~> pt)
(equiv_equiv_inhab_baut_bool_bool t pt)^-1%equiv e =
e t
    assert (p : equiv_equiv_inhab_baut_bool_bool t pt = alt).
H: Univalence
t: Bool
e: Bool <~> Bool
alt:= {|
  equiv_fun := equiv_inhab_baut_bool_bool t pt;
  equiv_isequiv :=
    isequiv_equiv_inhab_baut_bool_bool_lemma t pt
      (tr 1)
|}: pt <~> (Bool <~> pt)
equiv_equiv_inhab_baut_bool_bool t pt = alt
H: Univalence
t: Bool
e: Bool <~> Bool
alt:= {|
  equiv_fun := equiv_inhab_baut_bool_bool t pt;
  equiv_isequiv :=
    isequiv_equiv_inhab_baut_bool_bool_lemma t pt
      (tr 1)
|}: pt <~> (Bool <~> pt)
p: equiv_equiv_inhab_baut_bool_bool t pt = alt
(equiv_equiv_inhab_baut_bool_bool t pt)^-1%equiv e =
e t
    {
H: Univalence
t: Bool
e: Bool <~> Bool
alt:= {|
  equiv_fun := equiv_inhab_baut_bool_bool t pt;
  equiv_isequiv :=
    isequiv_equiv_inhab_baut_bool_bool_lemma t pt
      (tr 1)
|}: pt <~> (Bool <~> pt)
equiv_equiv_inhab_baut_bool_bool t pt = alt apply (ap (fun i => Build_Equiv _ _ _ i)).
H: Univalence
t: Bool
e: Bool <~> Bool
alt:= {|
  equiv_fun := equiv_inhab_baut_bool_bool t pt;
  equiv_isequiv :=
    isequiv_equiv_inhab_baut_bool_bool_lemma t pt
      (tr 1)
|}: pt <~> (Bool <~> pt)
isequiv_equiv_inhab_baut_bool_bool t pt =
isequiv_equiv_inhab_baut_bool_bool_lemma t pt (tr 1)
      apply (ap (isequiv_equiv_inhab_baut_bool_bool_lemma t pt)).
H: Univalence
t: Bool
e: Bool <~> Bool
alt:= {|
  equiv_fun := equiv_inhab_baut_bool_bool t pt;
  equiv_isequiv :=
    isequiv_equiv_inhab_baut_bool_bool_lemma t pt
      (tr 1)
|}: pt <~> (Bool <~> pt)
merely_path_component pt pt = tr 1
      apply path_ishprop. }
H: Univalence
t: Bool
e: Bool <~> Bool
alt:= {|
  equiv_fun := equiv_inhab_baut_bool_bool t pt;
  equiv_isequiv :=
    isequiv_equiv_inhab_baut_bool_bool_lemma t pt
      (tr 1)
|}: pt <~> (Bool <~> pt)
p: equiv_equiv_inhab_baut_bool_bool t pt = alt
(equiv_equiv_inhab_baut_bool_bool t pt)^-1%equiv e =
e t
    exact (ap10_equiv (ap equiv_inverse p) e).
  Defined.

  (** ** 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.
H: Univalence
BAut Bool -> BAut Bool -> BAut Bool
  Proof.
H: Univalence
BAut Bool -> BAut Bool -> BAut Bool
    intros Z W.
H: Univalence
Z, W: BAut Bool
BAut Bool
    exists (Z <~> W).
H: Univalence
Z, W: BAut Bool
merely ((Z <~> W) = Bool)
    baut_reduce; simpl.
H: Univalence
Tr (-1) ((Bool <~> Bool) = Bool)
    apply tr, symmetry.
H: Univalence
Bool = (Bool <~> Bool)
    exact (path_universe equiv_bool_aut_bool).
  Defined.

  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.
H: Univalence
Z: BAut Bool
pt ** Z = Z
  Proof.
H: Univalence
Z: BAut Bool
pt ** Z = Z
    apply path_baut, equiv_inverse, equiv_equiv_inhab_baut_bool_bool.
H: Univalence
Z: BAut Bool
Bool
    exact true.                   (** This is a choice! *)
  Defined.

  (** The pairing is obviously symmetric. *)
  Definition baut_bool_pairing_symm Z W : Z ** W = W ** Z.
H: Univalence
Z, W: BAut Bool
Z ** W = W ** Z
  Proof.
H: Univalence
Z, W: BAut Bool
Z ** W = W ** Z
    apply path_baut, equiv_equiv_inverse.
  Defined.

  (** 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.
H: Univalence
Z: BAut Bool
Z ** Z = pt
  Proof.
H: Univalence
Z: BAut Bool
Z ** Z = pt
    apply symmetry, path_baut_bool_inhab.
H: Univalence
Z: BAut Bool
Z ** Z
    exact equiv_idmap.            (** A choice!  Could be the flip. *)
  Defined.

  (** 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.
H: Univalence
Y, Z, W: BAut Bool
e: Y ** Z ** W
z: Z
Y ** W
  Proof.
H: Univalence
Y, Z, W: BAut Bool
e: Y ** Z ** W
z: Z
Y ** W
    simple refine (equiv_adjointify _ _ _ _).
H: Univalence
Y, Z, W: BAut Bool
e: Y ** Z ** W
z: Z
Y -> W
H: Univalence
Y, Z, W: BAut Bool
e: Y ** Z ** W
z: Z
W -> Y
H: Univalence
Y, Z, W: BAut Bool
e: Y ** Z ** W
z: Z
?f o ?g == idmap
H: Univalence
Y, Z, W: BAut Bool
e: Y ** Z ** W
z: Z
?g o ?f == idmap
    +
H: Univalence
Y, Z, W: BAut Bool
e: Y ** Z ** W
z: Z
Y -> W exact (fun y => e y z).
    +
H: Univalence
Y, Z, W: BAut Bool
e: Y ** Z ** W
z: Z
W -> Y intros w.
H: Univalence
Y, Z, W: BAut Bool
e: Y ** Z ** W
z: Z
w: W
Y
      destruct (path_baut_bool_inhab W w).
H: Univalence
Y, Z: BAut Bool
e: Y ** Z ** pt
z: Z
w: pt
Y
      destruct (path_baut_bool_inhab Z z).
H: Univalence
Y: BAut Bool
e: Y ** pt ** pt
z, w: pt
Y
      (** 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. *)
      destruct (dec (z=w)).
H: Univalence
Y: BAut Bool
e: Y ** pt ** pt
z, w: pt
p: z = w
Y
H: Univalence
Y: BAut Bool
e: Y ** pt ** pt
z, w: pt
n: z <> w
Y
      *
H: Univalence
Y: BAut Bool
e: Y ** pt ** pt
z, w: pt
p: z = w
Y exact (e^-1 (equiv_idmap _)).
      *
H: Univalence
Y: BAut Bool
e: Y ** pt ** pt
z, w: pt
n: z <> w
Y exact (e^-1 equiv_negb).
    +
H: Univalence
Y, Z, W: BAut Bool
e: Y ** Z ** W
z: Z
(fun y : Y => e y z)
o (fun w : W =>
   let p := path_baut_bool_inhab W w in
   match
     p in (_ = b) return (Y ** Z ** b -> b -> Y)
   with
   | 1 =>
       fun (e : Y ** Z ** pt) (w0 : pt) =>
       let p0 := path_baut_bool_inhab Z z in
       match
         p0 in (_ = b) return (Y ** b ** pt -> b -> Y)
       with
       | 1 =>
           fun (e0 : Y ** pt ** pt) (z : pt) =>
           let s := dec (z = w0) in
           match s with
           | inl p1 =>
               (fun _ : z = w0 => e0^-1 1%equiv) p1
           | inr n =>
               (fun _ : z <> w0 => e0^-1 equiv_negb) n
           end
       end e z
   end e w) == idmap intros w.
H: Univalence
Y, Z, W: BAut Bool
e: Y ** Z ** W
z: Z
w: W
e
  (let p := path_baut_bool_inhab W w in
   match
     p in (_ = b) return (Y ** Z ** b -> b -> Y)
   with
   | 1 =>
       fun (e : Y ** Z ** pt) (w : pt) =>
       let p0 := path_baut_bool_inhab Z z in
       match
         p0 in (_ = b) return (Y ** b ** pt -> b -> Y)
       with
       | 1 =>
           fun (e0 : Y ** pt ** pt) (z : pt) =>
           let s := dec (z = w) in
           match s with
           | inl _ => e0^-1 1%equiv
           | inr _ => e0^-1 equiv_negb
           end
       end e z
   end e w) z = w
      destruct (path_baut_bool_inhab W w).
H: Univalence
Y, Z: BAut Bool
e: Y ** Z ** pt
z: Z
w: pt
e
  (let p := 1 in
   match
     p in (_ = b) return (Y ** Z ** b -> b -> Y)
   with
   | 1 =>
       fun (e : Y ** Z ** pt) (w : pt) =>
       let p0 := path_baut_bool_inhab Z z in
       match
         p0 in (_ = b) return (Y ** b ** pt -> b -> Y)
       with
       | 1 =>
           fun (e0 : Y ** pt ** pt) (z : pt) =>
           let s := dec (z = w) in
           match s with
           | inl _ => e0^-1 1%equiv
           | inr _ => e0^-1 equiv_negb
           end
       end e z
   end e w) z = w
      destruct (path_baut_bool_inhab Z z).
H: Univalence
Y: BAut Bool
e: Y ** pt ** pt
z, w: pt
e
  (let p := 1 in
   match
     p in (_ = b) return (Y ** pt ** b -> b -> Y)
   with
   | 1 =>
       fun (e : Y ** pt ** pt) (w : pt) =>
       let p0 := 1 in
       match
         p0 in (_ = b) return (Y ** b ** pt -> b -> Y)
       with
       | 1 =>
           fun (e0 : Y ** pt ** pt) (z : pt) =>
           let s := dec (z = w) in
           match s with
           | inl _ => e0^-1 1%equiv
           | inr _ => e0^-1 equiv_negb
           end
       end e z
   end e w) z = w
      simpl.
H: Univalence
Y: BAut Bool
e: Y ** pt ** pt
z, w: pt
e
  match dec (z = w) with
  | inl _ => e^-1 1%equiv
  | inr _ => e^-1 equiv_negb
  end z = w
      destruct z,w; simpl; exact (ap10_equiv (eisretr e _) _).
    +
H: Univalence
Y, Z, W: BAut Bool
e: Y ** Z ** W
z: Z
(fun w : W =>
 let p := path_baut_bool_inhab W w in
 match
   p in (_ = b) return (Y ** Z ** b -> b -> Y)
 with
 | 1 =>
     fun (e : Y ** Z ** pt) (w0 : pt) =>
     let p0 := path_baut_bool_inhab Z z in
     match
       p0 in (_ = b) return (Y ** b ** pt -> b -> Y)
     with
     | 1 =>
         fun (e0 : Y ** pt ** pt) (z : pt) =>
         let s := dec (z = w0) in
         match s with
         | inl p1 =>
             (fun _ : z = w0 => e0^-1 1%equiv) p1
         | inr n =>
             (fun _ : z <> w0 => e0^-1 equiv_negb) n
         end
     end e z
 end e w) o (fun y : Y => e y z) == idmap intros y.
H: Univalence
Y, Z, W: BAut Bool
e: Y ** Z ** W
z: Z
y: Y
(let p := path_baut_bool_inhab W (e y z) in
 match
   p in (_ = b) return (Y ** Z ** b -> b -> Y)
 with
 | 1 =>
     fun (e : Y ** Z ** pt) (w : pt) =>
     let p0 := path_baut_bool_inhab Z z in
     match
       p0 in (_ = b) return (Y ** b ** pt -> b -> Y)
     with
     | 1 =>
         fun (e0 : Y ** pt ** pt) (z : pt) =>
         let s := dec (z = w) in
         match s with
         | inl _ => e0^-1 1%equiv
         | inr _ => e0^-1 equiv_negb
         end
     end e z
 end e (e y z)) = y
      destruct (path_baut_bool_inhab Y y).
H: Univalence
Z, W: BAut Bool
e: pt ** Z ** W
z: Z
y: pt
(let p := path_baut_bool_inhab W (e y z) in
 match
   p in (_ = b) return (pt ** Z ** b -> b -> pt)
 with
 | 1 =>
     fun (e : pt ** Z ** pt) (w : pt) =>
     let p0 := path_baut_bool_inhab Z z in
     match
       p0 in (_ = b) return (pt ** b ** pt -> b -> pt)
     with
     | 1 =>
         fun (e0 : pt ** pt ** pt) (z : pt) =>
         let s := dec (z = w) in
         match s with
         | inl _ => e0^-1 1%equiv
         | inr _ => e0^-1 equiv_negb
         end
     end e z
 end e (e y z)) = y
      destruct (path_baut_bool_inhab Z z).
H: Univalence
W: BAut Bool
e: pt ** pt ** W
z, y: pt
(let p := path_baut_bool_inhab W (e y z) in
 match
   p in (_ = b) return (pt ** pt ** b -> b -> pt)
 with
 | 1 =>
     fun (e : pt ** pt ** pt) (w : pt) =>
     let p0 := 1 in
     match
       p0 in (_ = b) return (pt ** b ** pt -> b -> pt)
     with
     | 1 =>
         fun (e0 : pt ** pt ** pt) (z : pt) =>
         let s := dec (z = w) in
         match s with
         | inl _ => e0^-1 1%equiv
         | inr _ => e0^-1 equiv_negb
         end
     end e z
 end e (e y z)) = y
      destruct (path_baut_bool_inhab W (e y z)).
H: Univalence
e: pt ** pt ** pt
z, y: pt
(let p := 1 in
 match
   p in (_ = b) return (pt ** pt ** b -> b -> pt)
 with
 | 1 =>
     fun (e : pt ** pt ** pt) (w : pt) =>
     let p0 := 1 in
     match
       p0 in (_ = b) return (pt ** b ** pt -> b -> pt)
     with
     | 1 =>
         fun (e0 : pt ** pt ** pt) (z : pt) =>
         let s := dec (z = w) in
         match s with
         | inl _ => e0^-1 1%equiv
         | inr _ => e0^-1 equiv_negb
         end
     end e z
 end e (e y z)) = y
      simpl.
H: Univalence
e: pt ** pt ** pt
z, y: pt
match dec (z = e y z) with
| inl _ => e^-1 1%equiv
| inr _ => e^-1 equiv_negb
end = y
      case (dec (z = e y z)); intros p; apply moveR_equiv_V;
      destruct (aut_bool_idmap_or_negb (e y)) as [q|q].
H: Univalence
e: pt ** pt ** pt
z, y: pt
p: z = e y z
q: e y = 1%equiv
1%equiv = e y
H: Univalence
e: pt ** pt ** pt
z, y: pt
p: z = e y z
q: e y = equiv_negb
1%equiv = e y
H: Univalence
e: pt ** pt ** pt
z, y: pt
p: z <> e y z
q: e y = 1%equiv
equiv_negb = e y
H: Univalence
e: pt ** pt ** pt
z, y: pt
p: z <> e y z
q: e y = equiv_negb
equiv_negb = e y
      *
H: Univalence
e: pt ** pt ** pt
z, y: pt
p: z = e y z
q: e y = 1%equiv
1%equiv = e y symmetry; assumption.
      *
H: Univalence
e: pt ** pt ** pt
z, y: pt
p: z = e y z
q: e y = equiv_negb
1%equiv = e y case (not_fixed_negb z (p @ ap10_equiv q z)^).
      *
H: Univalence
e: pt ** pt ** pt
z, y: pt
p: z <> e y z
q: e y = 1%equiv
equiv_negb = e y case (p (ap10_equiv q z)^).
      *
H: Univalence
e: pt ** pt ** pt
z, y: pt
p: z <> e y z
q: e y = equiv_negb
equiv_negb = e y symmetry; assumption.
  Defined.

  Definition baut_bool_pairing_ZZ_Z_symm_lemma {Y Z W}
             (e : Y ** (Z ** W)) (f : Y ** W)
  : merely Y -> Z.
H: Univalence
Y, Z, W: BAut Bool
e: Y ** Z ** W
f: Y ** W
merely Y -> Z
  Proof.
H: Univalence
Y, Z, W: BAut Bool
e: Y ** Z ** W
f: Y ** W
merely Y -> Z
    pose (k := (fun y => (e y)^-1 (f y))).
H: Univalence
Y, Z, W: BAut Bool
e: Y ** Z ** W
f: Y ** W
k:= fun y : Y => (e y)^-1 (f y): Y -> Z
merely Y -> Z
    refine (merely_rec_hset k); intros y1 y2.
H: Univalence
Y, Z, W: BAut Bool
e: Y ** Z ** W
f: Y ** W
k:= fun y : Y => (e y)^-1 (f y): Y -> Z
y1, y2: Y
k y1 = k y2
    destruct (path_baut_bool_inhab Y y1).
H: Univalence
Z, W: BAut Bool
e: pt ** Z ** W
f: pt ** W
k:= fun y : pt => (e y)^-1 (f y): pt -> Z
y1, y2: pt
k y1 = k y2
    destruct (path_baut_bool_inhab W (f y1)).
H: Univalence
Z: BAut Bool
e: pt ** Z ** pt
f: pt ** pt
k:= fun y : pt => (e y)^-1 (f y): pt -> Z
y1, y2: pt
k y1 = k y2
    destruct (path_baut_bool_inhab Z (k y1)).
H: Univalence
e: pt ** pt ** pt
f: pt ** pt
k:= fun y : pt => (e y)^-1 (f y): pt -> pt
y1, y2: pt
k y1 = k y2
    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.
H: Univalence
e: pt ** pt ** pt
y1, y2: pt
(e y1)^-1 y1 = (e y2)^-1 y2
H: Univalence
e: pt ** pt ** pt
y1, y2: pt
(e y1)^-1 (negb y1) = (e y2)^-1 (negb y2)
    +
H: Univalence
e: pt ** pt ** pt
y1, y2: pt
(e y1)^-1 y1 = (e y2)^-1 y2 destruct (dec (y1=y2)) as [p|p].
H: Univalence
e: pt ** pt ** pt
y1, y2: pt
p: y1 = y2
(e y1)^-1 y1 = (e y2)^-1 y2
H: Univalence
e: pt ** pt ** pt
y1, y2: pt
p: y1 <> y2
(e y1)^-1 y1 = (e y2)^-1 y2
      {
H: Univalence
e: pt ** pt ** pt
y1, y2: pt
p: y1 = y2
(e y1)^-1 y1 = (e y2)^-1 y2 exact (ap (fun y => (e y)^-1 y) p). }
H: Univalence
e: pt ** pt ** pt
y1, y2: pt
p: y1 <> y2
(e y1)^-1 y1 = (e y2)^-1 y2
      destruct (aut_bool_idmap_or_negb (e y1)) as [q1|q1];
        destruct (aut_bool_idmap_or_negb (e y2)) as [q2|q2].
H: Univalence
e: pt ** pt ** pt
y1, y2: pt
p: y1 <> y2
q1: e y1 = 1%equiv
q2: e y2 = 1%equiv
(e y1)^-1 y1 = (e y2)^-1 y2
H: Univalence
e: pt ** pt ** pt
y1, y2: pt
p: y1 <> y2
q1: e y1 = 1%equiv
q2: e y2 = equiv_negb
(e y1)^-1 y1 = (e y2)^-1 y2
H: Univalence
e: pt ** pt ** pt
y1, y2: pt
p: y1 <> y2
q1: e y1 = equiv_negb
q2: e y2 = 1%equiv
(e y1)^-1 y1 = (e y2)^-1 y2
H: Univalence
e: pt ** pt ** pt
y1, y2: pt
p: y1 <> y2
q1: e y1 = equiv_negb
q2: e y2 = equiv_negb
(e y1)^-1 y1 = (e y2)^-1 y2
      *
H: Univalence
e: pt ** pt ** pt
y1, y2: pt
p: y1 <> y2
q1: e y1 = 1%equiv
q2: e y2 = 1%equiv
(e y1)^-1 y1 = (e y2)^-1 y2 case (p ((ap e)^-1 (q1 @ q2^))).
      *
H: Univalence
e: pt ** pt ** pt
y1, y2: pt
p: y1 <> y2
q1: e y1 = 1%equiv
q2: e y2 = equiv_negb
(e y1)^-1 y1 = (e y2)^-1 y2 rewrite q1, q2.
H: Univalence
e: pt ** pt ** pt
y1, y2: pt
p: y1 <> y2
q1: e y1 = 1%equiv
q2: e y2 = equiv_negb
(1%equiv)^-1 y1 = equiv_negb^-1 y2 exact (negb_ne p).
      *
H: Univalence
e: pt ** pt ** pt
y1, y2: pt
p: y1 <> y2
q1: e y1 = equiv_negb
q2: e y2 = 1%equiv
(e y1)^-1 y1 = (e y2)^-1 y2 rewrite q1, q2.
H: Univalence
e: pt ** pt ** pt
y1, y2: pt
p: y1 <> y2
q1: e y1 = equiv_negb
q2: e y2 = 1%equiv
equiv_negb^-1 y1 = (1%equiv)^-1 y2 symmetry.
H: Univalence
e: pt ** pt ** pt
y1, y2: pt
p: y1 <> y2
q1: e y1 = equiv_negb
q2: e y2 = 1%equiv
(1%equiv)^-1 y2 = equiv_negb^-1 y1 exact (negb_ne (fun r => p r^)).
      *
H: Univalence
e: pt ** pt ** pt
y1, y2: pt
p: y1 <> y2
q1: e y1 = equiv_negb
q2: e y2 = equiv_negb
(e y1)^-1 y1 = (e y2)^-1 y2 case (p ((ap e)^-1 (q1 @ q2^))).
    +
H: Univalence
e: pt ** pt ** pt
y1, y2: pt
(e y1)^-1 (negb y1) = (e y2)^-1 (negb y2) destruct (dec (y1=y2)) as [p|p].
H: Univalence
e: pt ** pt ** pt
y1, y2: pt
p: y1 = y2
(e y1)^-1 (negb y1) = (e y2)^-1 (negb y2)
H: Univalence
e: pt ** pt ** pt
y1, y2: pt
p: y1 <> y2
(e y1)^-1 (negb y1) = (e y2)^-1 (negb y2)
      {
H: Univalence
e: pt ** pt ** pt
y1, y2: pt
p: y1 = y2
(e y1)^-1 (negb y1) = (e y2)^-1 (negb y2) exact (ap (fun y => (e y)^-1 (negb y)) p). }
H: Univalence
e: pt ** pt ** pt
y1, y2: pt
p: y1 <> y2
(e y1)^-1 (negb y1) = (e y2)^-1 (negb y2)
      destruct (aut_bool_idmap_or_negb (e y1)) as [q1|q1];
        destruct (aut_bool_idmap_or_negb (e y2)) as [q2|q2].
H: Univalence
e: pt ** pt ** pt
y1, y2: pt
p: y1 <> y2
q1: e y1 = 1%equiv
q2: e y2 = 1%equiv
(e y1)^-1 (negb y1) = (e y2)^-1 (negb y2)
H: Univalence
e: pt ** pt ** pt
y1, y2: pt
p: y1 <> y2
q1: e y1 = 1%equiv
q2: e y2 = equiv_negb
(e y1)^-1 (negb y1) = (e y2)^-1 (negb y2)
H: Univalence
e: pt ** pt ** pt
y1, y2: pt
p: y1 <> y2
q1: e y1 = equiv_negb
q2: e y2 = 1%equiv
(e y1)^-1 (negb y1) = (e y2)^-1 (negb y2)
H: Univalence
e: pt ** pt ** pt
y1, y2: pt
p: y1 <> y2
q1: e y1 = equiv_negb
q2: e y2 = equiv_negb
(e y1)^-1 (negb y1) = (e y2)^-1 (negb y2)
      *
H: Univalence
e: pt ** pt ** pt
y1, y2: pt
p: y1 <> y2
q1: e y1 = 1%equiv
q2: e y2 = 1%equiv
(e y1)^-1 (negb y1) = (e y2)^-1 (negb y2) case (p ((ap e)^-1 (q1 @ q2^))).
      *
H: Univalence
e: pt ** pt ** pt
y1, y2: pt
p: y1 <> y2
q1: e y1 = 1%equiv
q2: e y2 = equiv_negb
(e y1)^-1 (negb y1) = (e y2)^-1 (negb y2) rewrite q1, q2.
H: Univalence
e: pt ** pt ** pt
y1, y2: pt
p: y1 <> y2
q1: e y1 = 1%equiv
q2: e y2 = equiv_negb
(1%equiv)^-1 (negb y1) = equiv_negb^-1 (negb y2)
        exact (negb_ne (fun r => p ((ap negb)^-1 r))).
      *
H: Univalence
e: pt ** pt ** pt
y1, y2: pt
p: y1 <> y2
q1: e y1 = equiv_negb
q2: e y2 = 1%equiv
(e y1)^-1 (negb y1) = (e y2)^-1 (negb y2) rewrite q1, q2.
H: Univalence
e: pt ** pt ** pt
y1, y2: pt
p: y1 <> y2
q1: e y1 = equiv_negb
q2: e y2 = 1%equiv
equiv_negb^-1 (negb y1) = (1%equiv)^-1 (negb y2) symmetry.
H: Univalence
e: pt ** pt ** pt
y1, y2: pt
p: y1 <> y2
q1: e y1 = equiv_negb
q2: e y2 = 1%equiv
(1%equiv)^-1 (negb y2) = equiv_negb^-1 (negb y1)
        exact (negb_ne (fun r => p ((ap negb)^-1 r)^)).
      *
H: Univalence
e: pt ** pt ** pt
y1, y2: pt
p: y1 <> y2
q1: e y1 = equiv_negb
q2: e y2 = equiv_negb
(e y1)^-1 (negb y1) = (e y2)^-1 (negb y2) case (p ((ap e)^-1 (q1 @ q2^))).
  Defined.

  Definition baut_bool_pairing_ZZ_Z_symm_map Y Z W
  : Y ** (Z ** W) -> Z ** (Y ** W).
H: Univalence
Y, Z, W: BAut Bool
Y ** Z ** W -> Z ** Y ** W
  Proof.
H: Univalence
Y, Z, W: BAut Bool
Y ** Z ** W -> Z ** Y ** W
    intros e.
H: Univalence
Y, Z, W: BAut Bool
e: Y ** Z ** W
Z ** Y ** W
    simple refine (equiv_adjointify (baut_bool_pairing_ZZ_Z_symm_part1 e)
                             _ _ _).
H: Univalence
Y, Z, W: BAut Bool
e: Y ** Z ** W
Y ** W -> Z
H: Univalence
Y, Z, W: BAut Bool
e: Y ** Z ** W
baut_bool_pairing_ZZ_Z_symm_part1 e o ?g == idmap
H: Univalence
Y, Z, W: BAut Bool
e: Y ** Z ** W
?g o baut_bool_pairing_ZZ_Z_symm_part1 e == idmap
    -
H: Univalence
Y, Z, W: BAut Bool
e: Y ** Z ** W
Y ** W -> Z intros f.
H: Univalence
Y, Z, W: BAut Bool
e: Y ** Z ** W
f: Y ** W
Z
      exact (baut_bool_pairing_ZZ_Z_symm_lemma e f
               (merely_inhab_baut_bool Y)).
    -
H: Univalence
Y, Z, W: BAut Bool
e: Y ** Z ** W
baut_bool_pairing_ZZ_Z_symm_part1 e
o (fun f : Y ** W =>
   baut_bool_pairing_ZZ_Z_symm_lemma e f
     (merely_inhab_baut_bool Y)) == idmap intros f.
H: Univalence
Y, Z, W: BAut Bool
e: Y ** Z ** W
f: Y ** W
baut_bool_pairing_ZZ_Z_symm_part1 e
  (baut_bool_pairing_ZZ_Z_symm_lemma e f
     (merely_inhab_baut_bool Y)) = f
      apply path_equiv, path_arrow; intros y.
H: Univalence
Y, Z, W: BAut Bool
e: Y ** Z ** W
f: Y ** W
y: Y
baut_bool_pairing_ZZ_Z_symm_part1 e
  (baut_bool_pairing_ZZ_Z_symm_lemma e f
     (merely_inhab_baut_bool Y)) y = f y
      change ((e y)
                (baut_bool_pairing_ZZ_Z_symm_lemma e f
                  (merely_inhab_baut_bool Y)) = f y).
H: Univalence
Y, Z, W: BAut Bool
e: Y ** Z ** W
f: Y ** W
y: Y
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)) @ _).
H: Univalence
Y, Z, W: BAut Bool
e: Y ** Z ** W
f: Y ** W
y: Y
e y (baut_bool_pairing_ZZ_Z_symm_lemma e f (tr y)) =
f y
      simpl.
H: Univalence
Y, Z, W: BAut Bool
e: Y ** Z ** W
f: Y ** W
y: Y
e y (baut_bool_pairing_ZZ_Z_symm_lemma e f (tr y)) =
f y apply eisretr.
    -
H: Univalence
Y, Z, W: BAut Bool
e: Y ** Z ** W
(fun f : Y ** W =>
 baut_bool_pairing_ZZ_Z_symm_lemma e f
   (merely_inhab_baut_bool Y))
o baut_bool_pairing_ZZ_Z_symm_part1 e == idmap intros z.
H: Univalence
Y, Z, W: BAut Bool
e: Y ** Z ** W
z: Z
baut_bool_pairing_ZZ_Z_symm_lemma e
  (baut_bool_pairing_ZZ_Z_symm_part1 e z)
  (merely_inhab_baut_bool Y) = z
      assert (IsHSet Z) by exact _.
H: Univalence
Y, Z, W: BAut Bool
e: Y ** Z ** W
z: Z
X: IsHSet Z
baut_bool_pairing_ZZ_Z_symm_lemma e
  (baut_bool_pairing_ZZ_Z_symm_part1 e z)
  (merely_inhab_baut_bool Y) = z
      refine (Trunc_rec _ (merely_inhab_baut_bool Y)); intros y.
H: Univalence
Y, Z, W: BAut Bool
e: Y ** Z ** W
z: Z
X: IsHSet Z
y: Y
baut_bool_pairing_ZZ_Z_symm_lemma e
  (baut_bool_pairing_ZZ_Z_symm_part1 e z)
  (merely_inhab_baut_bool Y) = z
      refine (ap (baut_bool_pairing_ZZ_Z_symm_lemma e _)
                 (path_ishprop _ (tr y)) @ _).
H: Univalence
Y, Z, W: BAut Bool
e: Y ** Z ** W
z: Z
X: IsHSet Z
y: Y
baut_bool_pairing_ZZ_Z_symm_lemma e
  (baut_bool_pairing_ZZ_Z_symm_part1 e z) (tr y) = z
      simpl.
H: Univalence
Y, Z, W: BAut Bool
e: Y ** Z ** W
z: Z
X: IsHSet Z
y: Y
baut_bool_pairing_ZZ_Z_symm_lemma e
  (baut_bool_pairing_ZZ_Z_symm_part1 e z) (tr y) = z exact (eissect _ _).
  Defined.

  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.
H: Univalence
Y, Z, W: BAut Bool
baut_bool_pairing_ZZ_Z_symm_map Y Z W
o baut_bool_pairing_ZZ_Z_symm_map Z Y W == idmap
  Proof.
H: Univalence
Y, Z, W: BAut Bool
baut_bool_pairing_ZZ_Z_symm_map Y Z W
o baut_bool_pairing_ZZ_Z_symm_map Z Y W == idmap
    intros e.
H: Univalence
Y, Z, W: BAut Bool
e: Z ** Y ** W
baut_bool_pairing_ZZ_Z_symm_map Y Z W
  (baut_bool_pairing_ZZ_Z_symm_map Z Y W e) = e
    apply path_equiv, path_arrow; intros z.
H: Univalence
Y, Z, W: BAut Bool
e: Z ** Y ** W
z: Z
baut_bool_pairing_ZZ_Z_symm_map Y Z W
  (baut_bool_pairing_ZZ_Z_symm_map Z Y W e) z = e z
    apply path_equiv, path_arrow; intros y.
H: Univalence
Y, Z, W: BAut Bool
e: Z ** Y ** W
z: Z
y: Y
baut_bool_pairing_ZZ_Z_symm_map Y Z W
  (baut_bool_pairing_ZZ_Z_symm_map Z Y W e) z y =
e z y
    reflexivity.
  Defined.

  Definition baut_bool_pairing_ZZ_Z_symm Y Z W
  : Y ** (Z ** W) <~> Z ** (Y ** W).
H: Univalence
Y, Z, W: BAut Bool
Y ** Z ** W <~> Z ** Y ** W
  Proof.
H: Univalence
Y, Z, W: BAut Bool
Y ** Z ** W <~> Z ** Y ** W
    exact (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)).
  Defined.

  (** Finally, we can prove associativity. *)
  Definition baut_bool_pairing_ZZ_Z Z W Y
  : (Z ** W) ** Y = Z ** (W ** Y).
H: Univalence
Z, W, Y: BAut Bool
(Z ** W) ** Y = Z ** W ** Y
  Proof.
H: Univalence
Z, W, Y: BAut Bool
(Z ** W) ** Y = Z ** W ** Y
    refine (baut_bool_pairing_symm (Z ** W) Y @ _).
H: Univalence
Z, W, Y: BAut Bool
Y ** Z ** W = Z ** W ** Y
    refine (_ @ ap (fun X => Z ** X) (baut_bool_pairing_symm Y W)).
H: Univalence
Z, W, Y: BAut Bool
Y ** Z ** W = Z ** Y ** W
    apply path_baut, baut_bool_pairing_ZZ_Z_symm.
  Defined.

  (** 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).
H: Univalence
e: BAut Bool <~> BAut Bool
Z, W: BAut Bool
e^-1 Z ** W = Z ** e W
  Proof.
H: Univalence
e: BAut Bool <~> BAut Bool
Z, W: BAut Bool
e^-1 Z ** W = Z ** e W
    apply path_baut; simpl.
H: Univalence
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).
H: Univalence
e: BAut Bool <~> BAut Bool
Z, W: BAut Bool
e^-1 Z = W <~> Z = e W
    refine (_ oE (@equiv_moveL_equiv_M _ _ e _ W Z) oE _).
H: Univalence
e: BAut Bool <~> BAut Bool
Z, W: BAut Bool
Z = e W <~> Z = e W
H: Univalence
e: BAut Bool <~> BAut Bool
Z, W: BAut Bool
e^-1 Z = W <~> e^-1 Z = W
    -
H: Univalence
e: BAut Bool <~> BAut Bool
Z, W: BAut Bool
Z = e W <~> Z = e W apply equiv_inverse, equiv_path_sigma_hprop.
    -
H: Univalence
e: BAut Bool <~> BAut Bool
Z, W: BAut Bool
e^-1 Z = W <~> e^-1 Z = W apply equiv_path_sigma_hprop.
  Defined.

  Definition equiv_baut_bool_aut_baut_bool
  : BAut Bool <~> (BAut Bool <~> BAut Bool).
H: Univalence
BAut Bool <~> (BAut Bool <~> BAut Bool)
  Proof.
H: Univalence
BAut Bool <~> (BAut Bool <~> BAut Bool)
    simple refine (equiv_adjointify _ _ _ _).
H: Univalence
BAut Bool -> BAut Bool <~> BAut Bool
H: Univalence
BAut Bool <~> BAut Bool -> BAut Bool
H: Univalence
?f o ?g == idmap
H: Univalence
?g o ?f == idmap
    -
H: Univalence
BAut Bool -> BAut Bool <~> BAut Bool intros Z.
H: Univalence
Z: BAut Bool
BAut Bool <~> BAut Bool
      refine (equiv_involution (fun W => Z ** W) _).
H: Univalence
Z: BAut Bool
(fun x : BAut Bool => Z ** Z ** x) == idmap
      intros W.
H: Univalence
Z, W: BAut Bool
Z ** Z ** W = W
      refine ((baut_bool_pairing_ZZ_Z Z Z W)^ @ _).
H: Univalence
Z, W: BAut Bool
(Z ** Z) ** W = W
      refine (_ @ baut_bool_pairing_1Z W).
H: Univalence
Z, W: BAut Bool
(Z ** Z) ** W = pt ** W
      apply (ap (fun Y => Y ** W)).
H: Univalence
Z, W: BAut Bool
Z ** Z = pt
      apply baut_bool_pairing_ZZ.
    -
H: Univalence
BAut Bool <~> BAut Bool -> BAut Bool intros e.
H: Univalence
e: BAut Bool <~> BAut Bool
BAut Bool
      exact (e^-1 pt).
    -
H: Univalence
(fun Z : BAut Bool =>
 equiv_involution (fun W : BAut Bool => Z ** W)
   ((fun W : BAut Bool =>
     (baut_bool_pairing_ZZ_Z Z Z W)^ @
     (ap (fun Y : BAut Bool => Y ** W)
        (baut_bool_pairing_ZZ Z) @
      baut_bool_pairing_1Z W))
    :
    (fun x : BAut Bool => Z ** Z ** x) == idmap))
o (fun e : BAut Bool <~> BAut Bool => e^-1 pt) ==
idmap intros e.
H: Univalence
e: BAut Bool <~> BAut Bool
equiv_involution (fun W : BAut Bool => e^-1 pt ** W)
  (fun W : BAut Bool =>
   (baut_bool_pairing_ZZ_Z (e^-1 pt) (e^-1 pt) W)^ @
   (ap (fun Y : BAut Bool => Y ** W)
      (baut_bool_pairing_ZZ (e^-1 pt)) @
    baut_bool_pairing_1Z W)) = e
      apply path_equiv, path_arrow; intros Z; simpl.
H: Univalence
e: BAut Bool <~> BAut Bool
Z: BAut Bool
e^-1 pt ** Z = e Z
      refine (aut_baut_bool_moveR_pairing_V e pt Z @ _).
H: Univalence
e: BAut Bool <~> BAut Bool
Z: BAut Bool
pt ** e Z = e Z
      apply baut_bool_pairing_1Z.
    -
H: Univalence
(fun e : BAut Bool <~> BAut Bool => e^-1 pt)
o (fun Z : BAut Bool =>
   equiv_involution (fun W : BAut Bool => Z ** W)
     ((fun W : BAut Bool =>
       (baut_bool_pairing_ZZ_Z Z Z W)^ @
       (ap (fun Y : BAut Bool => Y ** W)
          (baut_bool_pairing_ZZ Z) @
        baut_bool_pairing_1Z W))
      :
      (fun x : BAut Bool => Z ** Z ** x) == idmap)) ==
idmap intros Z.
H: Univalence
Z: BAut Bool
(equiv_involution (fun W : BAut Bool => Z ** W)
   (fun W : BAut Bool =>
    (baut_bool_pairing_ZZ_Z Z Z W)^ @
    (ap (fun Y : BAut Bool => Y ** W)
       (baut_bool_pairing_ZZ Z) @
     baut_bool_pairing_1Z W)))^-1 pt = Z
      apply baut_bool_pairing_Z1.
  Defined.

  (** ** [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).
H: Univalence
g: BAut Bool <~> BAut Bool
W: BAut Bool
ap g (negb_center_baut_bool W) =
negb_center_baut_bool (g W)
  Proof.
H: Univalence
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.
H: Univalence
W, Z: BAut Bool
ap (equiv_baut_bool_aut_baut_bool Z)
  (negb_center_baut_bool W) =
negb_center_baut_bool
  (equiv_baut_bool_aut_baut_bool Z W)
    simpl.
H: Univalence
W, Z: BAut Bool
ap (fun W : BAut Bool => Z ** W)
  (negb_center_baut_bool W) =
negb_center_baut_bool (Z ** W)
    baut_reduce.
H: Univalence
ap (fun W : BAut Bool => pt ** W)
  (negb_center_baut_bool pt) =
negb_center_baut_bool (pt ** pt)
    refine (_ @ apD negb_center_baut_bool (baut_bool_pairing_1Z pt)^).
H: Univalence
ap (fun W : BAut Bool => pt ** W)
  (negb_center_baut_bool pt) =
transport (fun Z : BAut Bool => Z = Z)
  (baut_bool_pairing_1Z pt)^
  (negb_center_baut_bool pt)
    rewrite transport_paths_lr, inv_V.
H: Univalence
ap (fun W : BAut Bool => pt ** W)
  (negb_center_baut_bool pt) =
(baut_bool_pairing_1Z pt @ negb_center_baut_bool pt) @
(baut_bool_pairing_1Z pt)^
    apply moveL_pV.
H: Univalence
ap (fun W : BAut Bool => pt ** W)
  (negb_center_baut_bool pt) @ baut_bool_pairing_1Z pt =
baut_bool_pairing_1Z pt @ negb_center_baut_bool pt
    exact (concat_A1p baut_bool_pairing_1Z (negb_center_baut_bool pt)).
  Qed.

  Definition negb_center2_baut_baut_bool
  : forall B : BAut (BAut Bool), (idpath B) = (idpath B).
H: Univalence
forall B : BAut (BAut Bool), 1 = 1
  Proof.
H: Univalence
forall B : BAut (BAut Bool), 1 = 1
    refine (center2_baut (BAut Bool) _).
H: Univalence
{f : forall x : BAut Bool, x = x &
forall (g : BAut Bool <~> BAut Bool) (x : BAut Bool),
ap g (f x) = f (g x)}
    exists negb_center_baut_bool.
H: Univalence
forall (g : BAut Bool <~> BAut Bool) (x : BAut Bool),
ap g (negb_center_baut_bool x) =
negb_center_baut_bool (g x)
    exact center_baut_bool_central.
  Defined.

  Definition nontrivial_negb_center_baut_baut_bool
  : negb_center2_baut_baut_bool <> (fun Z => idpath (idpath Z)).
H: Univalence
negb_center2_baut_baut_bool <>
(fun Z : BAut (BAut Bool) => 1)
  Proof.
H: Univalence
negb_center2_baut_baut_bool <>
(fun Z : BAut (BAut Bool) => 1)
    intros oops.
H: Univalence
oops: negb_center2_baut_baut_bool =
(fun Z : BAut (BAut Bool) => 1)
Empty
    exact (nontrivial_negb_center_baut_bool
             (((ap (center2_baut (BAut Bool)))^-1
                (oops @ (id_center2_baut (BAut Bool))^))..1)).
  Defined.

End AssumeUnivalence.