Definition is_downward_closed (f : hsubtype X) : UU := ∏ (x : f) (y : down_type P (pr1carrier _ x)), f (pr1carrier _ y).
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All.