`{Univalence} {Y : pType@{u}} {F : Type@{u}} `{IsConnected 0 Y} : (Y ->* pBAut F) <~> (Y ->* [Type@{u}, F]). Proof. refine (_ oE pequiv_pequiv_postcompose pequiv_pbaut_typeOp). rapply equiv_pmap_typeO_type_connected. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Constant. Require Import HoTT.Truncations. Require Import ObjectClassifier Homotopy.ExactSequence Pointed.