`{Univalence} {Y F : pType@{u}} : (Y ->* [Type@{u}, F]) <~> { X : pType@{u} & FiberSeq F X Y }. Proof. refine (_ oE _). { do 2 (rapply equiv_functor_sigma_id; intro). apply equiv_pequiv_inverse. } exact ((equiv_sigma_assoc _ _)^-1 oE equiv_sigma_pfibration). Defined.
Require Import Basics Types. Require Import SuccessorStructure. Require Import WildCat. Require Import Pointed. Require Import Modalities.Identity Modalities.Descent. Require Import Truncations. Require Import HFiber. Require Import ObjectClassifier.