(t : Bool) (Z : BAut Bool) (z : Z) : Bool <~> Z := Build_Equiv _ _ (inhab_baut_bool_from_bool t Z 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.