{A B C D} {f : A -> B} {g : C -> D} {h : A -> C} {k : B -> D} (p : k o f == g o h) (ip : IsPullback p) : A <~> Pullback k g := Build_Equiv _ _ (pullback_corec p) ip.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Homotopy.IdentitySystems Cubical.PathSquare. Require Import Diagrams.CommutativeSquares.