Naming: structure vs property

[benediktahrens]

In Fibrations.v, it reads "We make the cloven version the default, so is_fibration etc are the cloven notions, and call the mere-existence versions un-cloven." So is_fibration is actually a structure, but its name sounds like it is a property.

We had a discussion in UniMath about that [1], where I asked not to do any renaming.

But maybe new notions could observe the convention suggested there?

[1] https://github.com/UniMath/UniMath/issues/214