(n : nat) {X Y : pType} (f : X ->* Y) : (pi_loops n Y) o* (fmap (Pi n.+1) f) ==* (fmap (pPi n o loops) f) o* (pi_loops n X). Proof. destruct n; srapply phomotopy_homotopy_hset; intros x. 1: reflexivity. refine ((O_functor_compose 0 _ _ _)^ @ _ @ (O_functor_compose 0 _ _ _)). apply O_functor_homotopy. exact (pointed_htpy (unfold_iterated_fmap_loops n.+1 f)). Defined.
Require Import Basics Types Pointed HSet. Require Import Modalities.Modality. Require Import Truncations.Core Truncations.SeparatedTrunc. Require Import Algebra.AbGroups. Require Import WildCat.