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