Build_Graph@{} (vert : Type@{s}) (edge : vert -> vert -> Type@{s}) (ishprop_edge : forall x y, IsHProp (edge x y)) : Graph := @exist@{u u} Type@{s} (fun V => @sig@{u u} (V -> V -> Type@{s}) (fun E => forall x y, IsHProp (E x y))) vert (@exist@{u u} (vert -> vert -> Type@{s}) (fun E => forall x y, IsHProp (E x y)) edge ishprop_edge).
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.