`{Univalence} X `{IsHSet X} : { f : X <~> X & forall g:X<~>X, g o f == f o g } <~> (forall Z:BAut X, Z = Z). Proof. refine (equiv_functor_forall_id (fun Z => equiv_path_sigma_hprop Z Z) oE _). refine (baut_ind_hset X (fun Z => Z = Z) oE _). simpl. refine (equiv_functor_sigma' (equiv_path_universe X X) _); intros f. apply equiv_functor_forall_id; intros g; simpl. refine (_ oE equiv_path_arrow _ _). refine (_ oE equiv_path_equiv (g oE f) (f oE g)). revert g. equiv_intro (equiv_path X X) g. revert f. equiv_intro (equiv_path X X) f. refine (_ oE equiv_concat_l (equiv_path_pp _ _) _). refine (_ oE equiv_concat_r (equiv_path_pp _ _)^ _). refine (_ oE (equiv_ap (equiv_path X X) _ _)^-1). refine (equiv_concat_l (transport_paths_lr _ _) _ oE _). refine (equiv_concat_l (concat_pp_p _ _ _) _ oE _). refine (equiv_moveR_Vp _ _ _ oE _). refine (equiv_concat_l _ _ oE equiv_concat_r _ _). - apply concat2; apply eissect. - symmetry; apply concat2; apply eissect. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Constant. Require Import HoTT.Truncations. Require Import ObjectClassifier Homotopy.ExactSequence Pointed.