`{Univalence} {X : Type} (x : X) (P : X -> Type) `{forall x, IsHProp (P x)} (Px : P x) : comp (sig P) (tr (x; Px)) <~> comp X (tr x). Proof. unfold comp, O_cover, hfiber. simpl. refine (_ oE (equiv_sigma_assoc _ _)^-1). apply equiv_functor_sigma_id; intro y. apply equiv_iff_hprop. - intros [py q]. exact (ap (Trunc_functor _ pr1) q). - refine (equiv_ind (equiv_path_Tr _ _) _ _). apply Trunc_rec; intros p; induction p. exact (Px; idpath). Defined.
Require Import Basics Types HFiber Truncations.Core Truncations.SeparatedTrunc Pointed