(n : Modality) {F X Y : pType} (i : F ->* X) (f : X ->* Y) : _ <~> IsExact n i f := ltac:(issig). Global Instance ishprop_isexact_hset `{Univalence} {F X Y : pType} `{IsHSet Y} (n : Modality) (i : F ->* X) (f : X ->* Y) : IsHProp (IsExact n i f). Proof. rapply (transport (fun A => IsHProp A) (x := { cx : IsComplex i f & IsConnMap n (cxfib cx) })). 2: exact _. apply path_universe_uncurried; issig. 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.