`{Funext} {A B C D} (k : B -> D) (g : C -> D) : { f : A -> B & { h : A -> C & k o f == g o h }} <~> @Pullback (A -> D) (A -> B) (A -> C) (fun f => k o f) (fun h => g o h). Proof. apply equiv_functor_sigma_id; intro f. apply equiv_functor_sigma_id; intro h. apply equiv_path_forall. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Homotopy.IdentitySystems Cubical.PathSquare. Require Import Diagrams.CommutativeSquares.