`{Univalence} X (P : Type -> Type) `{forall (Z : BAut X), IsHSet (P Z)} : { e : P (point (BAut X)) & forall g : X <~> X, transport P (path_universe g) e = e } <~> (forall (Z:BAut X), P Z). Proof. refine (equiv_sig_ind _ oE _). refine ((equiv_functor_forall' (P := fun Z => { f : (Z=X) -> P Z & WeaklyConstant f }) 1 (fun Z => equiv_merely_rec_hset_if_domain _ _)) oE _); simpl. { intros p. change (IsHSet (P (BAut_pr1 X (Z ; tr p)))). exact _. } unfold WeaklyConstant. refine (equiv_sig_coind _ _ oE _). srapply equiv_functor_sigma'. 1:apply (equiv_paths_ind_r X (fun x _ => P x)). intros p; cbn. refine (equiv_paths_ind_r X _ oE _). srapply equiv_functor_forall'. 1:apply equiv_equiv_path. intros e; cbn. refine (_ oE equiv_moveL_transport_V _ _ _ _). apply equiv_concat_r. rewrite path_universe_transport_idmap, paths_ind_r_transport. reflexivity. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Constant. Require Import HoTT.Truncations. Require Import ObjectClassifier Homotopy.ExactSequence Pointed.