Consider the type called
Prop, whose inhabitants are logical propositions (which are in turn inhabited by proofs). The fact that type
Prop itself does not have type belong to
Prop is an example of unramified -- this means that
Prop exhibits stratification(if
Prop:Prop then the calculus would be unstratified, but also inconsistent).:
However, note that
(forall a:Prop, a):Propa) does have type
Prop. So although
Prop doesn't " does not belong to itself"
Prop, things which quantify over all of
Prop may still belong to
Prop:. So we can be more specific and say that
Prop exhibits unramified stratification.
Set, a)whose inhabitants are datatypes (which are in turn inhabited by computations and the results of computations).
Set does not have type belong to itself, so it too exhibits stratification:
Check Set(assuming you're not using the old deprecated
-impredicative-set"mode).This is an Set : Type
Unlike the previous example, things which quantify over all of
Setdo not belong to
Set. This means that
Setexhibits ramified stratification.