proposition: Proposition equiv_baut_typeO `{Univalence} {F : Type} : BAut F <~> Type_ (subuniverse_merely_equiv F).
proof: Proof. srapply equiv_functor_sigma_id; intro X; cbn. rapply Trunc_functor_equiv. exact (equiv_path_universe _ _)^-1%equiv. Defined.
imports: HoTT.Basics HoTT.Types Constant HoTT.Truncations ObjectClassifier Homotopy.ExactSequence Pointed