90bfd84a07
In the standard library, we should use explicit universe variables for universe polymorphic definitions. Users that want to declare universe polymorphic definitions but do not want to provide universe level parameters should use Type _ or Type*
27 lines
644 B
Text
27 lines
644 B
Text
namespace S1
|
|
axiom I : Type*
|
|
definition F (X : Type*) : Type* := (X → Prop) → Prop
|
|
axiom {u} unfoldd : I.{u} → F I.{u}
|
|
axiom {l} foldd : F I.{l} → I.{l}
|
|
axiom iso1 : ∀x, foldd (unfoldd x) = x
|
|
end S1
|
|
|
|
namespace S2
|
|
universe u
|
|
axiom I : Type.{u}
|
|
definition F (X : Type*) : Type* := (X → Prop) → Prop
|
|
axiom unfoldd : I → F I
|
|
axiom foldd : F I → I
|
|
axiom iso1 : ∀x, foldd (unfoldd x) = x
|
|
end S2
|
|
|
|
|
|
namespace S3
|
|
section
|
|
hypothesis I : Type*
|
|
definition F (X : Type*) : Type* := (X → Prop) → Prop
|
|
hypothesis unfoldd : I → F I
|
|
hypothesis foldd : F I → I
|
|
hypothesis iso1 : ∀x, foldd (unfoldd x) = x
|
|
end
|
|
end S3
|