See comment https://github.com/HoTT/HoTT-Agda/commit/f62afb07dfeecc19c3844d229dcf36d25e9be224#r31023192 I think providing a `Bool` defined as GADT and provide conversion to `⊤ ⊔ ⊤` will be better.