proposition: Lemma precgraph_weq_pregraph : precgraph ≃ pregraph.
proof: Proof. unfold pregraph, precgraph. apply weqfibtototal. intro X. apply (weqcomp (Y := ∑ E : UU, E → X × X)). - apply weqfibtototal. intro Y. apply invweq, weqfuntoprodtoprod. - apply (weqcomp (Y := X × X → UU)). + set (A := X × X). apply display_weq. + apply weqfunfromdirprod. Defined.
imports: UniMath.MoreFoundations.Propositions UniMath.MoreFoundations.PartD UniMath.Combinatorics.Graph