{A B C} {c : C} {a : A} (g : C -> A) (f : B -> A) (p : g c = a) : hfiber (g ^*' f) c <~> hfiber f a. Proof. refine (_ oE hfiber_pullback_along' _ _ _); cbn. srapply (equiv_functor_hfiber2 (h:=equiv_idmap) (k:=equiv_idmap)). - reflexivity. - assumption. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Homotopy.IdentitySystems Cubical.PathSquare. Require Import Diagrams.CommutativeSquares.