doc: improve universe chapter (leanprover#5)

Many needed documentation operators are implemented, and math rendering
now works.

Main.lean

@@ -11,5 +11,8 @@ def main :=
 where
   config := {
     extraFiles := [("static", "static")],
-    extraCss := ["/static/theme.css", "/static/inter/inter.css", "/static/firacode/fira_code.css"]
+    extraCss := ["/static/theme.css", "/static/inter/inter.css", "/static/firacode/fira_code.css", "/static/katex/katex.min.css"],
+    extraJs := ["/static/katex/katex.min.js", "/static/math.js"]
+    emitTeX := false
+    emitHtmlSingle := false
   }

Manual/Language.lean

@@ -44,39 +44,53 @@ Propositions have the following properties:
 
 Types are classified by _universes_. {index}[universe]
 Each universe has a {deftech (key:="universe level")}[_level_], {index subterm := "of universe"}[level] which is a natural number.
-The `Sort` operator constructs a universe from a given level. {index}[`Sort`]
+The {lean}`Sort` operator constructs a universe from a given level. {index}[`Sort`]
 If the level of a universe is smaller than that of another, the universe itself is said to be smaller.
 With the exception of propositions (described later in this chapter), types in a given universe may only quantify over types in smaller universes.
-`Sort 0` is the type of propositions, while each `Sort (u + 1)` is a type that describes data.
+{lean}`Sort 0` is the type of propositions, while each `Sort (u + 1)` is a type that describes data.
 
-Every universe is an element of every strictly larger universe, so `Sort 5` includes `Sort 4`.
+Every universe is an element of every strictly larger universe, so {lean}`Sort 5` includes {lean}`Sort 4`.
 This means that the following examples are accepted:
 ```lean
 example : Sort 5 := Sort 4
 example : Sort 2 := Sort 1
 ```
 
 On the other hand, `Sort 3` is not an element of `Sort 5`:
-```lean error := true name := sort3
+```lean (error := true) (name := sort3)
 example : Sort 5 := Sort 3
 ```
 
-TODO show output
+```leanOutput sort3
+type mismatch
+  Type 2
+has type
+  Type 3 : Type 4
+but is expected to have type
+  Type 4 : Type 5
+```
 
 Similarly, because `Unit` is in `Sort 1`, it is not in `Sort 2`:
 ```lean
 example : Sort 1 := Unit
 ```
-```lean error := true
+```lean error := true name := unit1
 example : Sort 2 := Unit
 ```
 
-TODO show output
+```leanOutput unit1
+type mismatch
+  Unit
+has type
+  Type : Type 1
+but is expected to have type
+  Type 1 : Type 2
+```
 
-Because propositions and data are used differently and are governed by different rules, the abbreviations `Type` and `Prop` are provided to make the distinction more convenient.  {index}[`Type`] {index}[`Prop`]
-`Type u` is an abbreviation for `Sort (u + 1)`, so `Type 0` is `Sort 1` and `Type 3` is `Sort 4`.
-`Type 0` can also be abbreviated `Type`, so `Unit : Type` and `Type : Type 1`.
-`Prop` is an abbreviation for `Sort 0`.
+Because propositions and data are used differently and are governed by different rules, the abbreviations {lean}`Type` and {lean}`Prop` are provided to make the distinction more convenient.  {index}[`Type`] {index}[`Prop`]
+`Type u` is an abbreviation for `Sort (u + 1)`, so {lean}`Type 0` is {lean}`Sort 1` and {lean}`Type 3` is {lean}`Sort 4`.
+{lean}`Type 0` can also be abbreviated {lean}`Type`, so `Unit : Type` and `Type : Type 1`.
+{lean}`Prop` is an abbreviation for `Sort 0`.
 
 ### Predicativity
 
@@ -113,29 +127,77 @@ example (α : Type 2) (β : Type 1) : Type 3 := α → β
 Lean supports _universe polymorphism_, {index subterm:="universe"}[polymorphism] {index}[universe polymorphism] which means that constants defined in the Lean environment can take 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`:
-```lean
-def identity.{u} {α : Sort u} (x : α) : α := x
+When fully explicit, the identity function takes a universe parameter `u`. Its signature is:
+```signature
+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
+  type : Type u
+  encode : Array UInt32 → type → Array UInt32
+  decode : Array UInt32 → Nat → Option (type × Nat)
 ```
 
-TODO port signature macro from blog genre
+Lean automatically infers most level parameters.
+In the following example, it is not necessary to annotate the type as {lean}`Codec.{0}`, because {lean}`Char`'s type is {lean}`Type 0`, so `u` must be `0`:
+```lean (keep := true)
+def Codec.char : Codec where
+  type := Char
+  encode buf ch := buf.push ch.val
+  decode buf i := do
+    let v ← buf[i]?
+    if h : v.isValidChar then
+      let ch : Char := ⟨v, h⟩
+      return (ch, i + 1)
+    else
+      failure
+```
 
+Auto-bound implicit arguments are as universe-polymorphic as possible.
+Defining the identity function as follows:
+```lean
+def id' (x : α) := x
+```
+results in the signature:
+```signature
+id'.{u} {α : Sort u} (x : α) : α
+```
+On the other hand, because {name}`Nat` is in universe {lean}`Type 0`, this function automatically ends up with a concrete universe level for `α`, because `m` is applied to both {name}`Nat` and `α`, so both must have the same type and thus be in the same universe:
 ```lean
-#check id
+partial def count [Monad m] (p : α → Bool) (act : m α) : m Nat := do
+  if p (← act) then
+    return 1 + (← count p act)
+  else
+    return 0
 ```
 
-This means that `id` can be applied to types in _any_ universe.
-Conceptually speaking, `id` is a schematic definition that defines a family of identity functions, one for each universe.
+```lean (show := false)
+/-- info: Nat : Type -/
+#guard_msgs in
+#check Nat
+
+/--
+info: count.{u_1} {m : Type → Type u_1} {α : Type} [Monad m] (p : α → Bool) (act : m α) : m Nat
+-/
+#guard_msgs in
+#check count
+```
 
 #### Level Expressions
 
-Levels that occur in a definition are not restricted to just variables.
+Levels that occur in a definition are not restricted to just variables and addition of constants.
 More complex relationships between universes can be defined using level expressions.
 
-
 ````
-Level ::= n                -- Concrete levels
+Level ::= 0 | 1 | 2 | ...  -- Concrete levels
         | u, v             -- Variables
         | Level + n        -- Addition of constants
         | max Level Level  -- Least upper bound
@@ -145,18 +207,26 @@ Level ::= n                -- Concrete levels
 Given an assignment of level variables to concrete numbers, evaluating these expressions follows the usual rules of arithmetic.
 The `imax` operation is defined as follows:
 
-$``\mathtt{imax}\ u\ v = \begin{cases}{cl}0 & \mathrm{when }v = 0\\\mathtt{max}\ u\ v&\mathrm{otherwise}\end{cases}``
+$$``\mathtt{imax}\ u\ v = \begin{cases}0 & \mathrm{when\ }v = 0\\\mathtt{max}\ u\ v&\mathrm{otherwise}\end{cases}``
 
-TODO examples
+`imax` is used to implement impredicative quantification for {lean}`Prop`.
+In particular, if `A : Sort u` and `B : Sort v`, then `(x : A) → B : Sort (imax u v)`.
+If `B : Prop`, then the function type is itself a `Prop`; otherwise, the function type's level is the maximum of `u` and `v`.
 
 #### Universe Variable Bindings
 
-TODO `universe` command, local universe vars, auto-implicits
-
-#### Unification
+Universe-polymorphic definitions bind universe variables.
 
-TODO injectivity, (defaulting?)
+:::TODO
+ * `universe` command
+ * exact rules for binding universe vars
+:::
 
+#### Universe Unification
 
+:::TODO
+ * Rules for unification, properties of algorithm
+ * Lack of injectivity
+:::
 
 ## Inductive Types