fact: Definition inhab_baut_bool_from_bool (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.
imports: HoTT.Basics HoTT.Types Constant HoTT.Truncations.Core HoTT.Truncations.Connectedness Spaces.BAut Pointed.Core