ishprop_path_graph_in_N@{} (A B : Graph) (Arec : in_N@{u} A) : IsHProp (A = B). Proof. apply hprop_inhabited_contr; intros []. apply Arec; try exact _. - apply contr_inhabited_hprop; try exact 1. apply hprop_allpath. equiv_intro (equiv_path_graph graph_zero graph_zero) fe. destruct fe as [f e]. equiv_intro (equiv_path_graph graph_zero graph_zero) fe'. destruct fe' as [f' e']. apply equiv_ap; try exact _. apply path_sigma_hprop, path_equiv@{s s s}, path_arrow. intros []. - try clear B;intros B BC. refine (contr_equiv (B = B) (graph_succ_path_equiv B B)). Qed.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.