`{Univalence} {X} {Z Z' : BAut X} (f : Z <~> Z') : ap (BAut_pr1 X) (path_baut Z Z' f) = path_universe f. Proof. unfold path_baut, BAut_pr1; simpl. apply ap_pr1_path_sigma_hprop. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Constant. Require Import HoTT.Truncations. Require Import ObjectClassifier Homotopy.ExactSequence Pointed.