{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)). Proof. unfold functor_prod. snrefine (equiv_adjointify _ _ _ _). - exact (fun x => ((fst x.1; ap fst x.2), (snd x.1; ap snd x.2))). - refine (fun xs => (((fst xs).1, (snd xs).1); _)). apply Prod.path_prod;simpl. + exact (fst xs).2. + exact (snd xs).2. - destruct y as [y1 y2]; intros [[x1 p1] [x2 p2]]. simpl in *. destruct p1,p2. reflexivity. - intros [[x1 x2] p]. destruct p;cbn. reflexivity. Defined.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids Require Import Types.Empty.