{F X Y : pType} (i : F ->* X) (f : X ->* Y) `{IsExact purely F X Y i f} : LongExactSequence purely (N3). Proof. srefine (Build_LongExactSequence purely (N3) (loops_carrier F X Y) _ _). all:intros [n [[[[]|[]]|[]]|[]]]; cbn. { exact (fmap (iterated_loops n) f). } { exact (fmap (iterated_loops n) i). } { exact (connecting_map (fmap (iterated_loops n) i) (fmap (iterated_loops n) f)). } all:exact _. 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.