{F X Y} (fs : FiberSeq F X Y) : F ->* X := pfib fs.1 o* fs.2. Global Instance isexact_purely_fiberseq {F X Y : pType} (fs : FiberSeq F X Y) : IsExact purely ( fs) fs.1. Proof. srapply Build_IsExact; [ srapply Build_pHomotopy | ]. - intros u; cbn. exact ((fs.2 u).2). - apply moveL_pV. cbn. refine (concat_p1 _ @ _). apply moveL_Mp. refine (_ @ (point_eq fs.2)..2). refine (_ @ (transport_paths_Fl _ _)^). apply whiskerR, inverse2, ap, concat_p1. - intros [x p]. apply contr_map_isequiv. change (IsEquiv fs.2); 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.