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