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] UniMath/UniMath#214