Definition downward_closure_hsubtype : hsubtype X. Proof. intro y. refine (∃ (z : f), P y (pr1carrier _ z)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All.