proposition: Lemma map_graph_equiv_sigma (A B : Type@{i}) (R : A -> B -> Type@{i}) : map_graph 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: Coq(ssreflect) HoTT(HoTT) HoTT_additions