pequiv_pbaut_typeOp@{u v +} `{Univalence} {F : Type@{u}} : pBAut@{u v} F <~>* [Type_ (subuniverse_merely_equiv F), (F; tr equiv_idmap)]. Proof. snrapply Build_pEquiv'; cbn. 1: exact equiv_baut_typeO. by apply path_sigma_hprop. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Constant. Require Import HoTT.Truncations. Require Import ObjectClassifier Homotopy.ExactSequence Pointed.