fix: docs

doc/autobound.md

@@ -5,7 +5,7 @@ However, functions such as `compose` are still quite verbose to define. Note tha
 polymorphic `compose` is even more verbose than the one previously defined.
 
 ```lean
-universes u v w
+universe u v w
 def compose {α : Type u} {β : Type v} {γ : Type w}
             (g : β → γ) (f : α → β) (x : α) : γ :=
   g (f x)

doc/dep.md

@@ -44,7 +44,7 @@ dependent Cartesian product types ``(a : α) × β a`` generalize the Cartesian
 called *sigma* types, and you can also write them as `Σ a : α, β a`. You can use `⟨a, b⟩` or `Sigma.mk a b` to create a dependent pair.
 
 ```lean
-universes u v
+universe u v
 
 def f (α : Type u) (β : α → Type v) (a : α) (b : β a) : (a : α) × β a :=
   ⟨a, b⟩

doc/highlight.js

@@ -1111,7 +1111,7 @@ hljs.registerLanguage("lean", function(hljs) {
       'axiom constant ' +
       'partial unsafe private protected ' +
       'if then else ' +
-      'universe universes variable variables ' +
+      'universe variable variables ' +
       'import open export theory prelude renaming hiding exposing ' +
       'calc  match with do by let extends ' +
       'for in unless try catch finally mutual mut return continue break where rec ' +