{A B : pType} (f : A ->* B) : pfiber2_loops f o* pfib (pfib (pfib f)) ==* fmap loops f o* (loops_inv _ o* pfiber2_loops (pfib f)). Proof. pointed_reduce. simple refine (Build_pHomotopy _ _). - intros [[[x p] q] r]. simpl in *. move q before x; revert dependent x; refine (paths_ind_r _ _ _); intros p r; cbn. rewrite !concat_1p, concat_p1. rewrite paths_ind_r_transport. rewrite transport_arrow_toconst, transport_paths_Fl. rewrite concat_p1, inv_V, ap_V. refine (((r^)..2)^ @ _). rewrite transport_paths_Fl; cbn. rewrite pr1_path_V, !ap_V, !inv_V. apply concat_p1. - reflexivity. Qed.
Require Import Basics Types WildCat. Require Import HFiber. Require Import Pointed.Core. Require Import Pointed.pEquiv. Require Import Pointed.Loops.