proposition: Lemma umap_equiv_sigma (A B : Type@{i}) (R : A -> B -> Type@{i}) : IsUMap R <~> { map : A -> B | { mR : forall (a : A) (b : B), map a = b -> R a b | { Rm : forall (a : A) (b : B), R a b -> map a = b | forall (a : A) (b : B), mR a b o Rm a b == idmap } } }.
proof: Proof. by symmetry; issig. Defined.
imports: elpi(elpi) Coq(ssreflect) HoTT(HoTT) HoTT_additions Hierarchy