(X Y : pType) {n} : pfst o* iterated_loops_prod X Y ==* fmap (iterated_loops n) pfst. Proof. induction n as [|n IHn]. - reflexivity. - change (_ ==* ?R) with (pfst o* (loops_prod _ _ o* fmap loops (iterated_loops_prod _ _)) ==* R). refine ((pmap_compose_assoc _ _ _)^* @* _). refine (pmap_prewhisker _ (pfst_loops_prod _ _) @* _). refine ((fmap_comp loops _ _)^* @* _). change (?L ==* _) with (L ==* fmap loops (fmap (iterated_loops n) pfst)). rapply (fmap2 loops); simpl. exact IHn. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Factorization Truncations.Core Truncations.Connectedness HProp. Require Import Pointed.Core Pointed.pEquiv. Require Import WildCat. Require Import Spaces.Nat.Core.