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