{F X Y} (i : F ->* X) (f : X ->* Y) `{IsExact purely F X Y i f} : loops Y ->* F := i_fiberseq (connect_fiberseq i f). Global Instance isexact_connect_R {F X Y} (i : F ->* X) (f : X ->* Y) `{IsExact purely F X Y i f} : IsExact purely (fmap loops f) ( i f). Proof. refine (isexact_equiv_i (Y := F) purely (pfib (pfib i)) (fmap loops f) (((loops_inv X) o*E (pfiber2_loops (pfib f)) o*E (pequiv_pfiber _ _ (square_pequiv_pfiber _ _ (square_pfib_pequiv_cxfib i f))))^-1*) (((pfiber2_loops f) o*E (pequiv_pfiber _ _ (square_pfib_pequiv_cxfib i f)))^-1*) _ (pfib i)). refine (vinverse ((loops_inv X) o*E (pfiber2_loops (pfib f)) o*E (pequiv_pfiber _ _ (square_pequiv_pfiber _ _ (square_pfib_pequiv_cxfib i f)))) ((pfiber2_loops f) o*E (pequiv_pfiber _ _ (square_pfib_pequiv_cxfib i f))) _). refine (vconcat (f03 := loops_inv X o* pfiber2_loops (pfib f)) (f01 := pequiv_pfiber _ _ (square_pequiv_pfiber _ _ (square_pfib_pequiv_cxfib i f))) (f23 := pfiber2_loops f) (f21 := pequiv_pfiber _ _ (square_pfib_pequiv_cxfib i f)) _ _). - exact (square_pequiv_pfiber _ _ (square_pequiv_pfiber _ _ (square_pfib_pequiv_cxfib i f))). - exact (pfiber2_fmap_loops f). 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.