Universe proofreading

Manual/Language.lean

@@ -98,36 +98,53 @@ Each universe contains dependent function types, which additionally represent un
 A function type's universe is determined by the universes of its argument and return types.
 The specific rules depend on whether the return type of the function is a proposition.
 
-Functions that return propositions (that is, where the result type of the function is some type in `Prop`) may have argument types in any universe whatsoever, and the function type itself is in `Prop`.
-In other words, propositions feature _impredicative_ {index}[impredicative]{index subterm := "impredicative"}[quantification] quantification, because propositions can themselves be statements about all propositions.
+Predicates, which are functions that return propositions (that is, where the result type of the function is some type in `Prop`) may have argument types in any universe whatsoever, but the function type itself remains in `Prop`.
+In other words, propositions feature {deftech}[_impredicative_] {index}[impredicative]{index subterm := "impredicative"}[quantification] quantification, because propositions can themselves be statements about all propositions.
 For example, proof irrelevance can be written as a proposition that quantifies over all propositions:
 ```lean
 example : Prop := ∀ (P : Prop) (p1 p2 : P), p1 = p2
 ```
 
 For universes at {tech key:="universe level"}[level] `1` and higher (that is, the `Type u` hierarchy), quantification is {deftech}[_predicative_]. {index}[predicative]{index subterm := "predicative"}[quantification]
-For these universes, the universe of a function type is the greater of the argument and return types' universes.
+For these universes, the universe of a function type is the least upper bound of the argument and return types' universes.
 
 ```lean
 example (α : Type 1) (β : Type 2) : Type 2 := α → β
 example (α : Type 2) (β : Type 1) : Type 2 := α → β
 ```
 
 This example is not accepted, because `α`'s level is greater than `1`. In other words, the annotated universe is smaller than the function type's universe:
-```lean error := true
+```lean error := true name:=toosmall
 example (α : Type 2) (β : Type 1) : Type 1 := α → β
 ```
+```leanOutput toosmall
+type mismatch
+  α → β
+has type
+  Type 2 : Type 3
+but is expected to have type
+  Type 1 : Type 2
+```
+
+Lean's universes are not cumulative; a type in `Type u` is not automatically also in `Type (u + 1)`.
 This example is not accepted because the annotated universe is larger than the function type's universe:
-```lean error := true
+```lean error := true name:=toobig
 example (α : Type 2) (β : Type 1) : Type 3 := α → β
 ```
+```leanOutput toobig
+type mismatch
+  α → β
+has type
+  Type 2 : Type 3
+but is expected to have type
+  Type 3 : Type 4
+```
 
 ### Polymorphism
 
-Lean supports _universe polymorphism_, {index subterm:="universe"}[polymorphism] {index}[universe polymorphism] which means that constants defined in the Lean environment can take universe parameters.
+Lean supports _universe polymorphism_, {index subterm:="universe"}[polymorphism] {index}[universe polymorphism] which means that constants defined in the Lean environment can take {deftech}[universe parameters].
 These parameters can then be instantiated with universe levels when the constant is used.
 Universe parameters are written in curly braces following a dot after a constant name.
-Universe-polymorphic definitions in fact create a _schematic definition_ that can be instantiated at a variety of levels.
 
 When fully explicit, the identity function takes a universe parameter `u`. Its signature is:
 ```signature
@@ -137,7 +154,6 @@ id.{u} {α : Sort u} (x : α) : α
 Universe variables may additionally occur in universe level expressions, which provide specific universe levels in definitions.
 When the polymorphic definition is instantiated with concrete levels, these universe level expressions are also evaluated to yield concrete levels.
 
-
 In this example, a structure is in a universe that is one greater than the universe of the type it contains:
 ```lean (keep := true)
 structure Codec.{u} : Type (u + 1) where
@@ -161,6 +177,34 @@ def Codec.char : Codec where
       failure
 ```
 
+Universe-polymorphic definitions in fact create a _schematic definition_ that can be instantiated at a variety of levels, and different instantiations of universes create incompatible values.
+This can be seen in the following example, in which `T` is a gratuitously-universe-polymorphic definition that always returns the constructor of the unit type.
+Both instantiations of `T` have the same value, and both have the same type, but their differing universe instantiations make them incompatible:
+```lean (error := true) (name := uniIncomp) (keep := false)
+abbrev T.{u} : Unit := (fun (α : Sort u) => ()) PUnit.{u}
+
+set_option pp.universes true
+
+def test.{u, v} : T.{u} = T.{v} := rfl
+```
+```leanOutput uniIncomp
+type mismatch
+  rfl.{1}
+has type
+  Eq.{1} T.{u} T.{u} : Prop
+but is expected to have type
+  Eq.{1} T.{u} T.{v} : Prop
+```
+
+```lean (error := false) (name := uniIncomp) (keep := false)
+-- check that the above statement stays true
+abbrev T : Unit := (fun (α : Type) => ()) Unit
+
+set_option pp.universes true
+
+def test : T = T := rfl
+```
+
 Auto-bound implicit arguments are as universe-polymorphic as possible.
 Defining the identity function as follows:
 ```lean
@@ -219,7 +263,7 @@ Universe-polymorphic definitions bind universe variables.
 These bindings may be either explicit or implicit.
 Explicit universe variable binding and instantiaion occurs as a suffix to the definition's name, as in the following declaration of `map`, which declares two universe parameters (`u` and `v`) and instantiates the polymorphic `List` with each in turn:
 ```lean (keep := false)
-def map.{u} {α : Type u} {β : Type v} (f : α → β) : List.{u} α → List.{v} β
+def map.{u, v} {α : Type u} {β : Type v} (f : α → β) : List.{u} α → List.{v} β
   | [] => []
   | x :: xs => f x :: map f xs
 ```