{A B C} (f : B -> A) (g : C -> A) : f o pullback_pr1 == g o pullback_pr2 := (fun z => z.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Homotopy.IdentitySystems Cubical.PathSquare. Require Import Diagrams.CommutativeSquares.