{p : Pullback f g & Pullback (transport A p.2.2 o r p.1) (s p.2.1)} <~> Pullback (functor_sigma f r) (functor_sigma g s). Proof. refine (equiv_functor_sigma_id (fun _ => equiv_functor_sigma_id _) oE _). - intros; rapply equiv_path_sigma. - make_equiv. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Homotopy.IdentitySystems Cubical.PathSquare. Require Import Diagrams.CommutativeSquares.