proposition: Theorem pullback3x3 : Pullback fX1 fX3 <~> Pullback f1X f3X.
proof: 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.
imports: HoTT.Basics HoTT.Types HFiber PathAny Cubical.PathSquare Diagrams.CommutativeSquares