proposition: Lemma qglue_forall (f g : forall i, A i) (r : forall i, R i (f i) (g i)) : (fun i => class_of (R i) (f i)) = (fun i => class_of (R i) (g i)).
proof: Proof. funext s. by apply qglue. Defined.
imports: HoTT.Basics HoTT.Types HoTT.HSet HoTT.Truncations.Core HoTT.Colimits.Quotient HoTT.Projective