{O : Modality} {F X Y : pType} (i : F ->* X) (f : X ->* Y) `{IsExact purely _ _ _ i f} : IsExact O i f. Proof. srapply Build_IsExact. 1: apply cx_isexact. 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.