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