@{i j k l} {A : Type@{i}} (R : Relation@{i j} A) (P : Type@{l}) `{IsHSet P} (pclass : A -> P) (peq : forall a b, R a b -> pclass a = pclass b) (a b : A) (p : R a b) : ap (Quotient_rec@{i j k l} R P pclass peq) (qglue p) = peq a b p. Proof. lhs_V nrapply (ap_compose tr). snrapply GraphQuotient_rec_beta_gqglue. Defined.
Require Import Basics. Require Import Types. Require Import HSet. Require Import TruncType. Require Import Colimits.GraphQuotient. Require Import Truncations.Core.