{A B} (P : A -> Type) (Q : B -> Type) (f : A -> B) (g : forall a, P a -> Q (f a)) (b : B) (v : Q b) : (hfiber (functor_sigma f g) (b; v)) <~> {w : hfiber f b & hfiber (g w.1) ((w.2)^ # v)}. Proof. unfold hfiber, functor_sigma. refine (_ oE equiv_functor_sigma_id _). 2:intros; symmetry; apply equiv_path_sigma. transitivity {w : {x : A & f x = b} & {x : P w.1 & (w.2) # (g w.1 x) = v}}. 1:make_equiv. apply equiv_functor_sigma_id; intros [a p]; simpl. apply equiv_functor_sigma_id; intros u; simpl. apply equiv_moveL_transport_V. Defined.
Require Import HoTT.Basics. Require Import Types.Arrow Types.Paths.