fact: Definition hfiber_functor_prod {A B C D : Type} (f : A -> B) (g : C -> D) y : hfiber (functor_prod f g) y <~> (hfiber f (fst y) * hfiber g (snd y)).
imports: Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics Basics.Trunc Basics.Decidable Types.Empty