(Z : BAut Bool) (z : Z) : (point (BAut Bool)) = Z. Proof. apply path_baut. exact (equiv_inhab_baut_bool_bool true Z z). 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.