sig DGraphQuotient <~> GraphQuotient (fun a b => {r : R a.1 b.1 & e _ _ r a.2 = b.2}). Proof. snrapply equiv_adjointify. - snrapply flatten_rec. + exact (fun a x => gq (a; x)). + intros a b r x. apply gqglue. exists r. reflexivity. - snrapply GraphQuotient_rec. + exact (fun '(a; x) => (gq a; x)). + intros [a x] [b y] [r p]. simpl in p, r. destruct p. apply flatten_gqglue. - snrapply GraphQuotient_ind. 1: reflexivity. intros [a x] [b y] [r p]. simpl in p, r. destruct p. simpl. lhs nrapply transport_paths_FFlr. rewrite GraphQuotient_rec_beta_gqglue. refine ((_ @@ 1) @ concat_Vp _). lhs nrapply concat_p1. apply inverse2. nrapply flatten_rec_beta_gqglue. - snrapply flatten_ind. 1: reflexivity. intros a b r x. nrapply (transport_paths_FFlr' (g := GraphQuotient_rec _ _)); apply equiv_p1_1q. rewrite flatten_rec_beta_gqglue. exact (GraphQuotient_rec_beta_gqglue _ _ (a; x) (b; e a b r x) (r; 1)). Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Equivalences. Require Import Types.Universe Types.Paths Types.Arrow Types.Sigma Cubical.DPath.