make properties direct metadata of spaces about data HOT 6 OPEN

Could be convenient in some cases. Just one thing though. Many properties of spaces can be deduced from other properties via theorems. We don't want to lose that ability, as it's one of the nice features of pi-base, allowing to eliminate duplication in that way. If space X is listed as having property A, and a theorem has A implying B, we still need B. One asserted trait per file may be what makes this work currently?
(And not directly related, but I think there are quite a few traits files that could actually be removed and deduced instead.)

from data.

This proposal would replace the files spaces/Sx/properties/Pm.md and spaces/Sx/properites/Pn.md with the following header metadata in spaces/Sx/README.md (which I'd further lobby to rename to spaces/Sx.md):

properties:
    - id: Pm
      value: [true|false]
    - id: Pn
      value: [true|false]

Then all the current reference metadata and supporting content written each property's markdown file would be incorporated into the main spaces/Sx/README.md (or spaces/Sx.md) file. This better mirrors the pattern of properties/Py.md and theorems/Tz.md files, and should make editing much more streamlined. Particularly in the case of #134 where I have a single reference that defends every asserted property.

This should not change the behavior of automatically deduced properties. We still need to provide tooling to find redundant properties.

from data.

Are you proposing this only for the cases of properties whose justification is entirely contained in the reference mentioned at this top level that defines the space itself, and we would keep the previous scheme for cases where more explanations are provided or different references are used specifically for different properties?

Also I assume the search capabilities by properties would not be affected?

from data.

Ah, let me amend this.

properties:
    -   id: Pm
        value: [true|false]
        refs:
        -    mathse: 123456
    -   id: Pn
        value: [true|false]
        refs:
        -    jstor: 123456

So each assertion should have a reference or two. Then either any further elaboration goes in the main README for the space itself, or we could consider an extra note: "hello world \(x^2+y^2\)" attribute on each property item that contains the content currently stored in the space/property pair markdown file.

from data.

N.B. I'm not proposing any difference in the front-end viewer; it would have essentially the same capabilities (search, automatic deduction, etc). But this would make most contributions significantly more streamlined.

from data.

I am starting to like this idea. For deploying/testing this, we could:

• do a first pass at a change in the infrastructure to support both old and new scheme
• pick a representative space X with multiple property files with a variety of things like proofs, comments we want to preserve, etc
• introduce a parallel space "TEST X" using the new scheme
• see the result and compare how spaces X and TEST X look like in the front end viewer
• tweak/iterate as necessary until we are satisfied with the result

from data.