{A} `{IsHProp A} (ma : merely A) : Contr A. Proof. refine (@contr_trunc_conn (Tr (-1)) A _ _); try assumption. refine (contr_inhabited_hprop _ ma). Defined.
Require Import Basics Types WildCat.Core WildCat.Universe HFiber. Require Import Modalities.Modality.