equiv_path_graph@{} (A B : Graph) : { f : vert A <~> vert B & forall x y, edge A x y <-> edge B (f x) (f y) } <~> (A = B). Proof. srefine (equiv_path_sigma _ A B oE _). srefine (equiv_functor_sigma' (equiv_path_universe (vert A) (vert B)) _). intros f; cbn. rewrite transport_sigma. srefine (equiv_path_sigma_hprop _ _ oE _). cbn. srefine (equiv_path_forall _ _ oE _). srefine (equiv_functor_forall' (f^-1) _). intros x. srefine (equiv_path_forall _ _ oE _). srefine (equiv_functor_forall' (f^-1) _). intros y. cbn. rewrite transport_arrow. rewrite transport_arrow_toconst. rewrite !transport_path_universe_V. rewrite !eisretr. srefine (equiv_path_universe _ _ oE _). srefine (equiv_equiv_iff_hprop _ _). Qed.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.