Lemma precgraph_weq_pregraph : precgraph ≃ pregraph. 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.
Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.PartD. Require Import UniMath.Combinatorics.Graph.