`{Univalence} (X A : Type) (n : trunc_index) `{IsTrunc n.+1 X} `{IsRigid A} `{IsConnected n.+1 A} : BAut X <~> BAut (X * A). Proof. refine (Build_Equiv _ _ (baut_prod_r X A) _). apply isequiv_surj_emb. { apply BuildIsSurjection; intros Z. baut_reduce. refine (tr (point _ ; _)). apply path_sigma_hprop; reflexivity. } { apply isembedding_isequiv_ap. intros Z W. pose (L := fun e : Z <~> W => equiv_functor_prod_r (B := A) e). refine (isequiv_commsq L (ap (baut_prod_r X A)) (path_baut Z W) (path_baut (baut_prod_r X A Z) (baut_prod_r X A W)) (fun e => (ap_baut_prod_r X A e)^)). refine ((isconnected_elim (Tr (-1)) (A := A) _ _).1). { apply contr_inhabited_hprop; [ exact _ | refine (merely_isconnected n A) ]. } intros a0. baut_reduce. pose (M := fun f:X*A -> X*A => fun x => fst (f (x,a0))). assert (MH : forall (a:A) (f:X*A -> X*A) (x:X), fst (f (x,a)) = fst (f (x,a0))). { refine (conn_map_elim (Tr n) (unit_name a0) _ _). intros; reflexivity. } assert (MC : forall (f g :X*A -> X*A), M (g o f) == M g o M f). { intros f g x; unfold M. transitivity (fst (g (fst (f (x,a0)), snd (f (x,a0))))). - reflexivity. - apply MH. } pose (M' := aut_homomorphism_end M (fun x => 1) MC). assert (Mker : forall f, M' f == 1%equiv -> f == 1%equiv). { unfold M', M; cbn. intros f p. pose (fh := fun x a => (MH a f x) @ p x). pose (g := fun x a => snd (f (x,a))). assert (ge : forall x, IsEquiv (g x)). { apply isequiv_from_functor_sigma. refine (isequiv_commsq' _ f (equiv_sigma_prod0 X A) (equiv_sigma_prod0 X A) _). intros [x a]; cbn. apply path_prod; [ apply fh | reflexivity ]. } intros [x a]. pose (gisid := path_aut_rigid (Build_Equiv _ _ (g x) (ge x)) 1). apply path_prod. - apply fh. - apply gisid. } assert (Minj : forall f g, M' f == M' g -> f == g). { intros f g p z. apply moveL_equiv_M. revert z. refine (Mker (g^-1 oE f) _). intros x. refine (MC f g^-1 x @ _). change ((M' g)^-1 (M f x) = x). apply moveR_equiv_V, p. } refine (isequiv_adjointify L M' _ _); intros e; apply path_equiv, path_arrow; try apply Minj; intros x; reflexivity. } Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber. Require Import Truncations. Require Import Universes.BAut.