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