{D : Type} (P Q : D -> Type) : {d:D & P d * Q d} <~> Pullback (@pr1 D P) (@pr1 D Q) := Build_Equiv _ _ _ (ispullback_sigprod P Q).
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Homotopy.IdentitySystems Cubical.PathSquare. Require Import Diagrams.CommutativeSquares.