Quotient_ind_beta_qglue@{i j k l} {A : Type@{i}} (R : Relation@{i j} A) (P : Quotient@{i j k} R -> Type@{l}) {sP : forall x, IsHSet (P x)} (pclass : forall a, P (class_of R a)) (peq : forall a b (H : R a b), qglue H # pclass a = pclass b) (a b : A) (p : R a b) : apD (Quotient_ind@{i j k l} R P pclass peq) (qglue p) = peq a b p. Proof. lhs nrapply apD_compose'. unfold Quotient_ind. nrefine (ap _ (GraphQuotient_ind_beta_gqglue _ pclass (fun a b p0 => transport_compose P tr _ _ @ peq a b p0) _ _ _) @ _). rapply concat_V_pp. Defined.
Require Import Basics. Require Import Types. Require Import HSet. Require Import TruncType. Require Import Colimits.GraphQuotient. Require Import Truncations.Core.