{A} (P Q : A -> Type) (g : forall a, P a -> Q a) (b : A) (v : Q b) : (hfiber (functor_sigma idmap g) (b; v)) <~> hfiber (g b) v. Proof. refine (_ oE hfiber_functor_sigma P Q idmap g b v). exact (equiv_contr_sigma (fun (w:hfiber idmap b) => hfiber (g w.1) (transport Q (w.2)^ v))). Defined.
Require Import HoTT.Basics. Require Import Types.Arrow Types.Paths.