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