(t : Bool) (e : Bool <~> Bool) : equiv_inverse (equiv_equiv_inhab_baut_bool_bool t pt) e = e t. Proof. pose (alt := Build_Equiv _ _ (equiv_inhab_baut_bool_bool t pt) (isequiv_equiv_inhab_baut_bool_bool_lemma t pt (tr 1))). assert (p : equiv_equiv_inhab_baut_bool_bool t pt = alt). { apply (ap (fun i => Build_Equiv _ _ _ i)). apply (ap (isequiv_equiv_inhab_baut_bool_bool_lemma t pt)). apply path_ishprop. } exact (ap10_equiv (ap equiv_inverse p) e). 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.