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
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_fibrationis 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