(z : Pullback f2 g2) : hfiber functor_pullback z <~> Pullback (transport (hfiber h) z.2.2 o functor_hfiber (k := f2) p z.1) (functor_hfiber q z.2.1). Proof. destruct z as [b2 [c2 e2]]. refine (_ oE hfiber_functor_sigma _ _ _ _ _ _). apply equiv_functor_sigma_id. intros [b1 e1]; simpl. refine (_ oE (equiv_transport _ (transport_sigma' e1^ (c2; e2)))). refine (_ oE hfiber_functor_sigma _ _ _ _ _ _); simpl. apply equiv_functor_sigma_id. intros [c1 e3]; simpl. refine (_ oE (equiv_transport _ (ap (fun e => e3^ # e) (transport_paths_Fl e1^ e2)))). refine (_ oE (equiv_transport _ (transport_paths_Fr e3^ _))). unfold functor_hfiber; simpl. refine (equiv_concat_l (transport_sigma' e2 _) _ oE _); simpl. refine (equiv_path_sigma _ _ _ oE _); simpl. apply equiv_functor_sigma_id; intros e0; simpl. refine (equiv_concat_l (transport_paths_Fl e0 _) _ oE _). refine (equiv_concat_l (whiskerL (ap h e0)^ (transport_paths_r e2 _)) _ oE _). refine (equiv_moveR_Vp _ _ _ oE _). refine (equiv_concat_l (concat_pp_p _ _ _) _ oE _). refine (equiv_moveR_Vp _ _ _ oE _). do 2 refine (equiv_concat_r (concat_pp_p _ _ _) _ oE _). refine (equiv_moveL_pM _ _ _ oE _). abstract (rewrite !ap_V, inv_V; refine (equiv_path_inverse _ _)). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Homotopy.IdentitySystems Cubical.PathSquare. Require Import Diagrams.CommutativeSquares.