(Z : BAut Bool) (e : Z <~> Z) : (e = equiv_idmap Z) + (e = negb_baut_bool Z). Proof. 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)). } baut_reduce. case (aut_bool_idmap_or_negb e). - intros p; exact (inl p). - intros q; apply inr. exact (q @ negb_baut_bool_bool_negb^). 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.