{A B C} (f : B -> A) (g : C -> A) (b:B) : hfiber (f ^* g) b <~> hfiber g (f b). Proof. refine (equiv_functor_sigma_id (fun c => equiv_path_inverse _ _) oE _). make_equiv_contr_basedpaths. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Homotopy.IdentitySystems Cubical.PathSquare. Require Import Diagrams.CommutativeSquares.