`{Funext} {A : Type} {P Q : A -> Type} (h : forall a, P a -> Q a) (g : forall a, Q a) : hfiber (functor_forall_id h) g <~> (forall a, hfiber (h a) (g a)). Proof. unfold hfiber, functor_forall_id, functor_forall. nrefine (equiv_sig_coind _ _ oE _). apply equiv_functor_sigma_id; intro f. apply equiv_apD10. Defined.
Require Import Basics Types Diagrams.CommutativeSquares HSet.