{F X Y} (i : F ->* X) (f : X ->* Y) `{IsExact purely F X Y i f} : FiberSeq (loops Y) F X. Proof. exists i. exact (((pfiber2_loops f) o*E (pequiv_pfiber _ _ (square_pfib_pequiv_cxfib i f)))^-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.