proposition: Corollary equiv_map_baut_fibration `{Univalence} {Y : pType} {F : Type} : (Y -> BAut F) <~> { p : Slice Y & forall y:Y, merely (hfiber p.2 y <~> F) }.
proof: 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.
imports: HoTT.Basics HoTT.Types Constant HoTT.Truncations ObjectClassifier Homotopy.ExactSequence Pointed