(X Y : pType) : pfst o* loops_prod X Y ==* fmap loops pfst. Proof. snrapply Build_pHomotopy. - intro p; simpl. rhs nrapply concat_1p. symmetry; apply concat_p1. - reflexivity. 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.