Z : Z ** Z = pt. Proof. apply symmetry, path_baut_bool_inhab. apply equiv_idmap. Defined.
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.