fact: Definition Quotient_rec_beta_qglue @{i j k l} {A : Type@{i}} (R : Relation@{i j} A) (P : Type@{l}) `{IsHSet P} (pclass : A -> P) (peq : forall x y, R x y -> pclass x = pclass y) (x y : A) (p : R x y) : ap (Quotient_rec@{i j k l} R P pclass peq) (qglue p) = peq x y p.
imports: Basics Types HSet TruncType Colimits.GraphQuotient Truncations.Core PropResizing