fact: Definition isepi' {X Y} `(f : X -> Y) := forall (Z : HSet) (g : Y -> Z), Contr { h : Y -> Z | g o f = h o f }.
imports: Basics Types TruncType ReflectiveSubuniverse Colimits.Pushout Truncations.Core HIT.SetCone