fact: Definition hfiber_functor_sigma_idmap {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.
imports: HoTT.Basics Types.Arrow Types.Paths