From c3adf50f0720c912397ff994e3a78c7f71198195 Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@davidchristiansen.dk>
Date: Tue, 19 Nov 2024 11:03:46 +0100
Subject: [PATCH 1/2] fix: incorrect word

---
 Manual/Language/Functions.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Manual/Language/Functions.lean b/Manual/Language/Functions.lean
index 1f3a316..695f70a 100644
--- a/Manual/Language/Functions.lean
+++ b/Manual/Language/Functions.lean
@@ -185,7 +185,7 @@ Implicit parameters come in three varieties:
   : Strict implicit parameters
 
     Strict implicit parameters are identical to ordinary implicit parameters, except Lean will only attempt to find argument values when subsequent explicit arguments are provided at a call site.
-    Ordinary implicit parameters are written in double curly braces (`⦃` and `⦄`, or `{{` and `}}`).
+    Strict implicit parameters are written in double curly braces (`⦃` and `⦄`, or `{{` and `}}`).
 
   : Instance implicit parameters
 

From 2cd0cef10459e43f4fccbcef972c1516dbd15157 Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@davidchristiansen.dk>
Date: Tue, 19 Nov 2024 11:19:34 +0100
Subject: [PATCH 2/2] fix: dodgy example

This example relied on
https://github.com/leanprover/lean4/issues/6117, and the same point
can be made more cleanly this way.
---
 Manual/Language.lean | 26 +++++++++++---------------
 1 file changed, 11 insertions(+), 15 deletions(-)

diff --git a/Manual/Language.lean b/Manual/Language.lean
index 15d184b..c538e4b 100644
--- a/Manual/Language.lean
+++ b/Manual/Language.lean
@@ -334,33 +334,29 @@ def Codec.char : Codec where
 
 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.
 
-:::Manual.example "Universe polymorphism is not first-class"
+::::keepEnv
+:::Manual.example "Universe polymorphism and definitional equality"
 
-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}
+This can be seen in the following example, in which {lean}`T` is a gratuitously-universe-polymorphic function that always returns {lean}`true`.
+Because it is marked {keywordOf Lean.Parser.Command.declaration}`opaque`, Lean can't check equality by unfolding the definitions.
+Both instantiations of {lean}`T` have the parameters and the same type, but their differing universe instantiations make them incompatible.
+```lean (error := true) (name := uniIncomp)
+opaque T.{u} (_ : Nat) : Bool := (fun (α : Sort u) => true) PUnit.{u}
 
 set_option pp.universes true
 
-def test.{u, v} : T.{u} = T.{v} := rfl
+def test.{u, v} : T.{u} 0 = T.{v} 0 := rfl
 ```
 ```leanOutput uniIncomp
 type mismatch
   rfl.{1}
 has type
-  Eq.{1} T.{u} T.{u} : Prop
+  Eq.{1} (T.{u} 0) (T.{u} 0) : Prop
 but is expected to have type
-  Eq.{1} T.{u} T.{v} : Prop
-```
-
-```lean (error := false) (keep := false) (show := false)
--- check that the above statement stays true
-abbrev T : Unit := (fun (α : Type) => ()) Unit
-
-def test : T = T := rfl
+  Eq.{1} (T.{u} 0) (T.{v} 0) : Prop
 ```
 :::
+::::
 
 Auto-bound implicit arguments are as universe-polymorphic as possible.
 Defining the identity function as follows: