`{Univalence} {Y F : pType} `{IsConnected 0 Y} : (Y ->* pBAut F) <~> { X : pType & FiberSeq F X Y } := classify_fiberseq oE equiv_pmap_pbaut_type_p.
Require Import HoTT.Basics HoTT.Types. Require Import Constant. Require Import HoTT.Truncations. Require Import ObjectClassifier Homotopy.ExactSequence Pointed.