Z : Z ** pt = Z := baut_bool_pairing_symm Z pt @ baut_bool_pairing_1Z Z.
Require Import HoTT.Basics HoTT.Types. Require Import Constant. Require Import HoTT.Truncations.Core HoTT.Truncations.Connectedness. Require Import Universes.BAut. Require Import Pointed.Core.