fact: Definition topologydirprod := λ (z : U × V) (A : U × V → hProp), (∃ (Ax : U → hProp) (Ay : V → hProp), (Ax (pr1 z) × isOpen Ax) × (Ay (pr2 z) × isOpen Ay) × (∏ x y, Ax x → Ay y → A (x,,y))).
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Topology.Filters UniMath.Algebra.Groups UniMath.Algebra.DivisionRig UniMath.Algebra.ConstructiveStructures