(f : LocalGenerators@{a}) : LocalGenerators@{a}. Proof. econstructor; intros i. exact (functor_susp (f i)). Defined.
Require Import HoTT.Basics HoTT.Types HoTT.Cubical.DPath. Require Import HFiber Extensions Factorization Limits.Pullback. Require Import Modality Accessible Descent. Require Import Truncations.Core. Require Import Homotopy.Suspension.