proposition: Lemma umap_isprop `{Funext} {A B : Type@{i}} (R : A -> B -> Type@{i}) : IsHProp (IsUMap R).
proof: Proof. apply (istrunc_equiv_istrunc (IsFun R)); last exact: isfun_isprop. apply symmetric_equiv; apply umap_equiv_isfun. Qed.
imports: elpi(elpi) Coq(ssreflect) HoTT(HoTT) HoTT_additions Hierarchy