proposition: Lemma total_hsubtype_preserving {X Y : UU} (f : X → Y) : hsubtype_preserving (totalsubtype X) (totalsubtype Y) f.
proof: Proof. exact (λ _ _, tt). Qed.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.Propositions