{F X Y} (fs : FiberSeq F X Y) : FiberSeq (loops F) (loops X) (loops Y). Proof. refine (fmap loops fs.1; _). refine (_ o*E emap loops fs.2). exact (pfiber_fmap_loops fs.1)^-1*. Defined.
Require Import Basics Types. Require Import SuccessorStructure. Require Import WildCat. Require Import Pointed. Require Import Modalities.Identity Modalities.Descent. Require Import Truncations. Require Import HFiber. Require Import ObjectClassifier.