BAut Bool <~> (BAut Bool <~> BAut Bool). Proof. simple refine (equiv_adjointify _ _ _ _). - intros Z. refine (equiv_involution (fun W => Z ** W) _). intros 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. - intros e. exact (e^-1 pt). - intros e. apply path_equiv, path_arrow; intros Z; simpl. refine (aut_baut_bool_moveR_pairing_V e pt Z @ _). apply baut_bool_pairing_1Z. - intros Z. apply baut_bool_pairing_Z1. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Constant. Require Import HoTT.Truncations.Core HoTT.Truncations.Connectedness. Require Import Universes.BAut. Require Import Pointed.Core.