graph_add@{} (A B : Graph) : Graph. Proof. exists (vert A + vert B). exists (fun ab ab' => match ab, ab' return Type@{s} with | inl a, inl a' => edge A a a' | inl a, inr b => Unit | inr b, inl a => Empty | inr b, inr b' => edge B b b' end). intros [a|b] [a'|b']; exact _. Defined.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.