`{Univalence} X `{IsTrunc 1 X} : { f : forall x:X, x=x & forall (g:X<~>X) (x:X), ap g (f x) = f (g x) } <~> (forall Z:BAut X, (idpath Z) = (idpath Z)). Proof. refine ((equiv_functor_forall_id (fun Z => (equiv_concat_lr _ _) oE (equiv_ap (equiv_path_sigma_hprop Z Z) 1%path 1%path))) oE _). { symmetry; apply path_sigma_hprop_1. } { apply path_sigma_hprop_1. } assert (forall Z:BAut X, IsHSet (idpath Z.1 = idpath Z.1)) by exact _. refine (baut_ind_hset X (fun Z => idpath Z = idpath Z) oE _). simple refine (equiv_functor_sigma' _ _). { refine (_ oE equiv_path2_universe 1 1). apply equiv_concat_lr. - symmetry; apply path_universe_1. - apply path_universe_1. } intros f. apply equiv_functor_forall_id; intros g. refine (_ oE equiv_path3_universe _ _). refine (dpath_paths2 (path_universe g) _ _ oE _). cbn. change (equiv_idmap X == equiv_idmap X) in f. refine (equiv_concat_lr _ _). - refine (_ @ (path2_universe_postcompose_idmap f g)^). abstract (rewrite !whiskerR_pp, !concat_pp_p; reflexivity). - refine (path2_universe_precompose_idmap f g @ _). abstract (rewrite !whiskerL_pp, !concat_pp_p; reflexivity). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Constant. Require Import HoTT.Truncations. Require Import ObjectClassifier Homotopy.ExactSequence Pointed.