fact: Definition baut_bool_pairing_Z1 Z : Z ** pt = Z := baut_bool_pairing_symm Z pt @ baut_bool_pairing_1Z Z.
imports: HoTT.Basics HoTT.Types Constant HoTT.Truncations.Core HoTT.Truncations.Connectedness Spaces.BAut Pointed.Core