N_add@{} (n m : N) : N. Proof. exists (graph_add n.1 m.1). intros P PH P0 Ps. apply m.2. - intros; apply PH. - apply (transport P (graph_add_zero_r n.1)^). exact (n.2 P PH P0 Ps). - intros A PA. apply (transport P (graph_add_succ n.1 A)^). apply Ps, PA. Defined.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.