fact: Definition product_point_coordinate (xy : X × Y) : UU := (pr1 xy = Px) ⨿ (pr2 xy = Py).
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Structures.CartesianStructure UniMath.CategoryTheory.DisplayedCats.Structures.StructureLimitsAndColimits