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