graph_succ_path_equiv@{} (A B : Graph) : (A = B) <~> (graph_succ A = graph_succ B). Proof. refine ((equiv_path_graph _ _) oE _). refine (_ oE (equiv_path_graph _ _)^-1). srefine (equiv_adjointify _ _ _ _). - intros [f e]. exists (f +E 1). intros x y. destruct x as [x|x]; destruct y as [y|y]; cbn. + apply e. + split; apply idmap. + split; apply idmap. + split; apply idmap. - intros [f e]. exists (graph_unsucc_equiv_vert f e). exact (graph_unsucc_equiv_edge f e). - intros [f e]. apply path_sigma_hprop; cbn. apply path_equiv, path_arrow; intros [x|[]]; cbn. + apply unfunctor_sum_l_beta. + symmetry; apply graph_succ_equiv_inr, e. - intros [f e]. apply path_sigma_hprop; cbn. apply path_equiv, path_arrow; intros x; reflexivity. Defined.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.