{A B C D : Type} {f : A -> B} {g : C -> D} {h : A -> C} {k : B -> D} (p : k o f == g o h) (e : IsPullback p) : forall b:B, IsEquiv (functor_hfiber p b). Proof. apply isequiv_from_functor_sigma. unfold IsPullback in e. snrapply isequiv_commsq'. 4: exact (equiv_fibration_replacement f)^-1%equiv. 1: exact (Pullback k g). 1: exact (pullback_corec p). { apply (functor_sigma idmap); intro b. apply (functor_sigma idmap); intro c. apply inverse. } { intros [x [y q]]. destruct q. apply (path_sigma' _ idpath). apply (path_sigma' _ idpath). simpl. refine (_^ @ (inv_Vp _ _)^). apply concat_1p. } all: exact _. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Homotopy.IdentitySystems Cubical.PathSquare. Require Import Diagrams.CommutativeSquares.