fact: Definition coeq_flatten_fam : Coeq f g -> Type := Coeq_rec Type F (fun x => path_universe (e x)).
imports: Basics Types.Paths Types.Arrow Types.Sigma Types.Forall Types.Universe Types.Prod Cubical.DPath Colimits.GraphQuotient