{X Y : Type} (f : X -> Y) := forall Z : HSet, forall g0 g1 : Y -> Z, g0 o f == g1 o f -> g0 == g1.
Require Import Basics. Require Import Types. Require Import TruncType. Require Import ReflectiveSubuniverse. Require Import Colimits.Pushout Truncations.Core HIT.SetCone.