proposition: Lemma is_open_union_open_hsubtype (A : hsubtype Open) : isOpen (union_open_hsubtype A).
proof: Proof. apply isOpen_union. intros U HU. use (hinhuniv _ HU); intros H. exact (pr1 H). Qed.
imports: UniMath.MoreFoundations.Subtypes UniMath.Topology.Topology