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