IsPullback (comm_square_comp' H K) -> IsPullback H. Proof. intro e2. apply ispullback_isequiv_functor_hfiber. intro b. pose (e1' := isequiv_functor_hfiber_ispullback _ e1 (i b)). pose (e2' := isequiv_functor_hfiber_ispullback _ e2 b). snrapply isequiv_commsq'. 7: apply isequiv_idmap. 4: apply (functor_hfiber_compose H K b). 1,2: exact _. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Homotopy.IdentitySystems Cubical.PathSquare. Require Import Diagrams.CommutativeSquares.