`{Univalence} {Y : pType} {F : Type} : (Y -> BAut F) <~> { p : Slice Y & forall y:Y, merely (hfiber p.2 y <~> F) }. Proof. refine (_ oE equiv_postcompose' equiv_baut_typeO). refine (_ oE equiv_sigma_fibration_O). snrapply equiv_functor_sigma_id; intro p. rapply equiv_functor_forall_id; intro y. by apply Trunc_functor_equiv. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Constant. Require Import HoTT.Truncations. Require Import ObjectClassifier Homotopy.ExactSequence Pointed.