{A} {A_stable : Stable A} : Tr (-1) A <-> A. Proof. refine (_, tr). intro ma. apply stable; intro na. revert ma; rapply Trunc_ind; exact na. Defined.
Require Import Basics Types WildCat.Core WildCat.Universe HFiber. Require Import Modalities.Modality.