fact: Definition quotient_kernel_factor_general@{|} := Eval unfold quotient_kernel_factor_internal in quotient_kernel_factor_internal@{ar' ar abr abr ab}.
imports: Basics Types HSet TruncType Colimits.GraphQuotient Truncations.Core PropResizing