`{Univalence} {A : Type} `{Contr (BAut A)} : IsRigid A. Proof. unfold IsRigid. equiv_intro ((path_baut (point (BAut A)) (point (BAut A)))^-1) f. equiv_intro ((path_baut (point (BAut A)) (point (BAut A)))^-1) g. apply ap10, ap, ap, path_contr. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber. Require Import Truncations. Require Import Universes.BAut.