{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). Proof. intros [f [h p]]. exact (pullback_corec p). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Homotopy.IdentitySystems Cubical.PathSquare. Require Import Diagrams.CommutativeSquares.