{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 : forall b:B, IsEquiv (functor_hfiber p b)) : IsPullback p. Proof. unfold IsPullback. apply isequiv_contr_map; intro x. rapply contr_equiv'. - symmetry; apply hfiber_pullback_corec. - exact _. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Homotopy.IdentitySystems Cubical.PathSquare. Require Import Diagrams.CommutativeSquares.