`{Funext} (A A' B : pType) (f : A ->* loops B) (g : A' ->* A) : (loop_susp_adjoint A' B)^-1 (f o* g) ==* (loop_susp_adjoint A B)^-1 f o* fmap psusp g. Proof. cbn. refine (_ @* (pmap_compose_assoc _ _ _)^*). apply pmap_postwhisker. exact (fmap_comp psusp g f). Defined.
Require Import Basics. Require Import Types. Require Import Pointed.Core. Require Import Pointed.Loops. Require Import Pointed.pTrunc. Require Import Pointed.pEquiv. Require Import Homotopy.Suspension. Require Import Homotopy.Freudenthal. Require Import Truncations. Require Import WildCat.