Definition make_downward_closed_subtype (f : hsubtype X) (H : is_downward_closed f) : downward_closed_subtype := f ,, H.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All.