Pullback fX1 fX3 <~> Pullback f1X f3X. Proof. refine (_ oE _ oE _). 1,3:do 2 (rapply equiv_functor_sigma_id; intro). 1:apply equiv_path_pullback. 1:symmetry; apply equiv_path_pullback. refine (_ oE _). { do 4 (rapply equiv_functor_sigma_id; intro). refine (sq_tr oE _). refine (sq_move_14^-1 oE _). refine (sq_move_31 oE _). refine (sq_move_24^-1 oE _). refine (sq_move_23^-1 oE _). rewrite 2 inv_V. reflexivity. } make_equiv. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Homotopy.IdentitySystems Cubical.PathSquare. Require Import Diagrams.CommutativeSquares.