Pullback f g <~> Pullback f' g'. Proof. unfold Pullback. apply (equiv_functor_sigma' eB); intro b. apply (equiv_functor_sigma' eC); intro c. refine (equiv_concat_l (p _) _ oE _). refine (equiv_concat_r (q _)^ _ oE _). refine (equiv_ap' eA _ _). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Homotopy.IdentitySystems Cubical.PathSquare. Require Import Diagrams.CommutativeSquares.