{X Y Z : Type} {f : X -> Y} (i : Y -> Z) `{IsEmbedding i} `{!IsEquiv (i o f)} : IsEquiv f. Proof. rapply (cancelL_isequiv i). refine (isequiv_surj_emb i). rapply (cancelR_issurjection f). Defined.
Require Import Basics Types WildCat.Core WildCat.Universe HFiber. Require Import Modalities.Modality.