Pullback f1 g1 -> Pullback f2 g2 := functor_sigma k (fun b1 => (functor_sigma l (fun c1 e1 => p b1 @ ap h e1 @ (q c1)^))).
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Homotopy.IdentitySystems Cubical.PathSquare. Require Import Diagrams.CommutativeSquares.