`{Univalence} (X A : Type) {Z W : BAut X} (e : Z <~> W) : ap (baut_prod_r X A) (path_baut Z W e) = path_baut (baut_prod_r X A Z) (baut_prod_r X A W) (equiv_functor_prod_r e). Proof. cbn. apply moveL_equiv_M; cbn; unfold pr1_path. rewrite <- (ap_compose (baut_prod_r X A) pr1 (path_sigma_hprop Z W _)). rewrite <- ((ap_compose pr1 (fun Z => Z * A) (path_sigma_hprop Z W _))^). rewrite ap_pr1_path_sigma_hprop. apply moveL_equiv_M; cbn. apply ap_prod_r_path_universe. Qed.
Require Import HoTT.Basics HoTT.Types. Require Import Constant. Require Import HoTT.Truncations. Require Import ObjectClassifier Homotopy.ExactSequence Pointed.