{A B C D} {f : A -> B} {g : C -> D} {h : A -> C} {k : B -> D} (p : k o f == g o h) (b : B) (c : C) (q : k b = g c) : hfiber (pullback_corec p) (b; c; q) <~> hfiber (functor_hfiber p b) (c; q^). Proof. unfold hfiber, functor_hfiber, functor_sigma. refine (equiv_sigma_assoc _ _ oE _). apply equiv_functor_sigma_id; intros a; cbn. refine (_ oE (equiv_path_sigma _ _ _)^-1); cbn. apply equiv_functor_sigma_id; intro p0; cbn. rewrite transport_sigma'; cbn. refine ((equiv_path_sigma _ _ _) oE _ oE (equiv_path_sigma _ _ _)^-1); cbn. apply equiv_functor_sigma_id; intro p1; cbn. rewrite !transport_paths_Fr, !transport_paths_Fl. refine (_ oE (equiv_ap (equiv_path_inverse _ _) _ _)); cbn. apply equiv_concat_l. refine (_ @ (inv_pp _ _)^). apply whiskerL. refine (_ @ (inv_pp _ _)^). apply whiskerL. symmetry; apply inv_V. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Homotopy.IdentitySystems Cubical.PathSquare. Require Import Diagrams.CommutativeSquares.