`{Funext} (A B B' : pType) (f : psusp A ->* B) (g : B ->* B') : loop_susp_adjoint A B' (g o* f) ==* fmap loops g o* loop_susp_adjoint A B f. Proof. cbn. refine (_ @* pmap_compose_assoc _ _ _). apply pmap_prewhisker. refine (fmap_comp loops f g). 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.