`{Univalence} X `{IsHSet X} : center_baut X (exist (fun (f:X<~>X) => forall (g:X<~>X), g o f == f o g) (equiv_idmap X) (fun (g:X<~>X) (x:X) => idpath (g x))) = fun Z => idpath Z. Proof. apply path_forall; intros Z. assert (IsHSet (Z.1 = Z.1)) by exact _. baut_reduce. exact (ap (path_sigma_hprop _ _) path_universe_1 @ path_sigma_hprop_1 _). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Constant. Require Import HoTT.Truncations. Require Import ObjectClassifier Homotopy.ExactSequence Pointed.