(t : Bool) (Z : BAut Bool) (z : Z) : Bool -> Z := fun b => if t then if b then z else negb_baut_bool Z z else if b then negb_baut_bool Z z else z.
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.