(Z : BAut Bool) : negb_baut_bool Z <> equiv_idmap Z. Proof. intros oops. apply nontrivial_negb_center_baut_bool. apply path_forall; intros Z'. pose (p := merely_path_component Z Z'). clearbody p. strip_truncations. destruct p. unfold negb_baut_bool in oops. apply moveL_equiv_V in oops. refine (_ @ ap (equiv_path_sigma_hprop _ _) (oops @ path_universe_1) @ _). - symmetry. refine (eisretr (equiv_path_sigma_hprop Z Z) _). - apply moveR_equiv_M; 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.