(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. Proof. apply path_forall; intros z'; simpl in z'. apply path_forall; intros b. destruct z', b, t; simpl; try reflexivity; try apply (ap10_equiv 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.