fact: Definition Coeq_rec2_beta (a : A) (a' : A') : Coeq_rec2 (coeq a) (coeq a') = coeq' a a' := 1.
imports: Basics Types.Paths Types.Arrow Types.Sigma Types.Forall Types.Universe Types.Prod Cubical.DPath Colimits.GraphQuotient