proposition: Lemma hexists_open_neighborhood (p : carrier (⋃ A)): ∃ U : A, pr1 U (pr1 p).
proof: Proof. induction p as [p Hp]. simpl in Hp. use (hinhuniv _ Hp); intro Hu. induction Hu as [u Hu]. induction Hu as [Hu Hup]. use (hinhfun _ Hu); intro H. induction H as [H HUu]. exists (make_carrier _ _ HUu). exact Hup. Qed.
imports: UniMath.MoreFoundations.Subtypes UniMath.Topology.Topology