hfiber_pullback_along' {A B C} (g : C -> A) (f : B -> A) (c:C) : hfiber (g ^*' f) c <~> hfiber f (g c). Proof. make_equiv_contr_basedpaths. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Homotopy.IdentitySystems Cubical.PathSquare. Require Import Diagrams.CommutativeSquares.