`{Univalence} {X} {Z Z' : BAut X} (f : Z <~> Z') (z : Z) : transport (fun (W:BAut X) => W) (path_baut Z Z' f) z = f z. Proof. refine (transport_compose idmap (BAut_pr1 X) _ _ @ _). refine (_ @ transport_path_universe f z). apply ap10, ap, ap_pr1_path_baut. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Constant. Require Import HoTT.Truncations. Require Import ObjectClassifier Homotopy.ExactSequence Pointed.