fact: Definition merely_inhab_baut_bool `{Funext} (Z : BAut Bool) : merely Z := center (merely Z).
imports: HoTT.Basics HoTT.Types Constant HoTT.Truncations.Core HoTT.Truncations.Connectedness Spaces.BAut Pointed.Core