{A B} (f : A -> B) `{IsSurjection f} `{IsEmbedding f} : IsEquiv f. Proof. apply (@isequiv_conn_ino_map (Tr (-1))); assumption. Defined.
Require Import Basics Types WildCat.Core WildCat.Universe HFiber. Require Import Modalities.Modality.