From 4bd5db3d7a985002bd6a8c5c82f8846578b55bd7 Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@davidchristiansen.dk>
Date: Mon, 27 Jan 2025 15:24:11 +0100
Subject: [PATCH 1/7] feat: Quotients

WIP
---
 Manual.lean           |   2 +
 Manual/Quotients.lean | 301 ++++++++++++++++++++++++++++++++++++++++++
 Manual/Types.lean     |  12 +-
 lake-manifest.json    |  10 +-
 4 files changed, 310 insertions(+), 15 deletions(-)
 create mode 100644 Manual/Quotients.lean

diff --git a/Manual.lean b/Manual.lean
index 7121703b..197a4bd3 100644
--- a/Manual.lean
+++ b/Manual.lean
@@ -279,6 +279,8 @@ Setoid
 Squash
 Subsingleton
 WellFoundedRelation
+Equivalence
+HasEquiv
 ```
 
 ```exceptions
diff --git a/Manual/Quotients.lean b/Manual/Quotients.lean
new file mode 100644
index 00000000..5e0c3f23
--- /dev/null
+++ b/Manual/Quotients.lean
@@ -0,0 +1,301 @@
+/-
+Copyright (c) 2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
+import VersoManual
+
+import Manual.Meta
+
+import Manual.Language.Functions
+import Manual.Language.InductiveTypes
+
+open Verso.Genre Manual
+
+#doc (Manual) "Quotients" =>
+%%%
+tag := "quotients"
+%%%
+
+:::planned 51
+ * Define {deftech}[quotient] type
+ * Show the computation rule
+:::
+
+
+{deftech}_Quotient types_ allow a new type to be formed by decreasing the granularity of an existing type's propositional equality.
+In particular, given an type $`A` and an equivalence relation $`\sim`, the quotient $`A / \sim` contains the same elements as $`A`, but every pair of elements that are related by $`\sim` are considered equal.
+Equality is respected universally; nothing in Lean's logic can observe any difference between two equal terms.
+Thus, quotient types provide a way to build an impenetrable abstraction barrier.
+In particular, all functions from a quotient type must prove that they respect the equivalence relation.
+
+{docstring Quotient}
+
+:::paragraph
+Quotients are widely used in mathematics:
+
+: Integers
+
+  The integers are traditionally defined as a pair of natural numbers $`(n, k)` that encodes the integer $`n - k`.
+  In this encoding, two integers $`(n_1, k_1)` and $`(n_2, k_2)` are equal if $`n_1 + k_2 = n_2 + k_1`.
+
+: Rational Numbers
+
+  The number $`\frac{n}{d}` can be encoded as the pair $`(n, d)`, where $`d \neq 0`.
+  Two rational numbers $`\frac{n_1}{d_1}` and $`\frac{n_2}{d_2}` are equal if $`n_1 d_2 = n_2 d_1`.
+
+: Real Numbers
+
+  The real numbers can be represented as a Cauchy sequence, but this encoding is not unique.
+  Using a quotient type, two Cauchy sequences can be made equal when their difference converges to zero.
+
+:::
+
+:::TODO
+
+Ask colleagues for a couple more good examples here
+
+:::
+
+Quotient types are not widely used in programming.
+
+
+# Setoids
+
+Quotient types are built on setoids.
+A {deftech}_setoid_ is a type paired with a distinguished equivalence relation.
+Unlike a quotient type, the abstraction barrier is not enforced, and proof automation designed around equality cannot be used with the setoid's equivalence relation.
+Setoids are primarily used as a building block for quotient types.
+
+{docstring Setoid}
+
+# Equivalence Relations
+
+An {deftech}_equivalence relation_ is a relation that is reflexive, symmetric, and transitive.
+
+
+:::syntax term (title := "Equivalence Relations")
+Equivalence according to some canonical equivalence relation for a type is written using `≈`, which is overloaded using the {tech}[type class] {name}`HasEquiv`.
+```grammar
+$_ ≈ $_
+```
+:::
+
+{docstring HasEquiv}
+
+```lean (show := false)
+section
+variable (r : α → α → Prop)
+```
+
+The fact that a relation {lean}`r` is actually an equivalence relation is stated {lean}`Equivalence r`.
+
+{docstring Equivalence}
+
+```lean (show := false)
+end
+```
+
+# Quotient API
+
+## Introducing Quotients
+
+The type {lean}`Quotient` expects an instance of {lean}`Setoid` as its explicit parameter.
+A value in the quotient is a value from the setoid's underlying type, wrapped in {lean}`Quotient.mk`.
+
+{docstring Quotient.mk}
+
+{docstring Quotient.mk'}
+
+:::example "The Integers"
+The integers can be defined as pairs of natural numbers where the represented integer is the difference of the two numbers.
+This representation is not unique: both {lean}`(4, 7)` and {lean}`(1, 4)` represent {lean type:="Int"}`-3`.
+Two encoded integers should be considered equal when they are related by {name}`Z.eq`:
+
+```lean
+def Z' : Type := Nat × Nat
+
+def Z.eq (n k : Z') : Prop :=
+  n.1 + k.2 = n.2 + k.1
+```
+
+This relation is an equivalence relation:
+```lean
+def Z.eq.eqv : Equivalence Z.eq where
+  refl := by
+    intro (x, y)
+    simp_arith [eq]
+  symm := by
+    intro (x, y) (x', y') heq
+    simp_all only [eq]
+    omega
+  trans := by
+    intro (x, y) (x', y') (x'', y'')
+    intro heq1 heq2
+    simp_all only [eq]
+    omega
+```
+
+Thus, it can be used as a {name}`Setoid`:
+```lean
+instance Z.instSetoid : Setoid Z'where
+  r := Z.eq
+  iseqv := Z.eq.eqv
+```
+
+The type {lean}`Z` of integers is then the quotient of {lean}`Z'` by the {name}`Setoid` instance:
+
+```lean
+def Z : Type := Quotient Z.instSetoid
+```
+
+The helper {lean}`Z.mk` makes it simpler to create integers without worrying about the choice of {name}`Setoid` instance:
+```lean
+def Z.mk (n : Z') : Z := Quotient.mk _ n
+```
+
+However, numeric literals are even more convenient.
+An {name}`OfNat` instance allows numeric literals to be used for integers:
+```lean
+instance : OfNat Z n where
+  ofNat := .mk _ (n, 0)
+```
+:::
+
+
+
+## Eliminating Quotients
+
+Functions from quotients can be defined based on functions from the underlying type by proving that the function respects the quotient's equivalence relation.
+This is accomplished using {lean}`Quotient.lift`.
+
+{docstring Quotient.lift}
+
+:::example "Integer Negation and Addition"
+
+```lean (show := false)
+def Z' : Type := Nat × Nat
+
+def Z.eq (n k : Z') : Prop :=
+  n.1 + k.2 = n.2 + k.1
+
+def Z.eq.eqv : Equivalence Z.eq where
+  refl := by
+    intro (x, y)
+    simp_arith [eq]
+  symm := by
+    intro (x, y) (x', y') heq
+    simp_all only [eq]
+    omega
+  trans := by
+    intro (x, y) (x', y') (x'', y'')
+    intro heq1 heq2
+    simp_all only [eq]
+    omega
+
+instance Z.instSetoid : Setoid Z' where
+  r := Z.eq
+  iseqv := Z.eq.eqv
+
+def Z : Type := Quotient Z.instSetoid
+
+def Z.mk (n : Z') : Z := Quotient.mk _ n
+```
+
+Given the encoding {lean}`Z` of integers as a quotient of pairs of natural numbers, negation can be implemented by swapping the first and second projections:
+```lean
+def neg' : Z' → Z
+  | (x, y) => .mk (y, x)
+```
+
+This can be transformed into a function from {lean}`Z` to {lean}`Z` by proving that negation respects the equivalence relation:
+```lean
+instance : Neg Z where
+  neg :=
+    Quotient.lift neg' <| by
+      intro n k equiv
+      apply Quotient.sound
+      simp only [instHasEquivOfSetoid, Setoid.r, Z.eq] at *
+      omega
+```
+
+Similarly, {lean}`Quotient.lift₂` is useful for defining binary functions from a quotient type.
+Addition is defined point-wise:
+```lean
+def add' (n k : Nat × Nat) : Z :=
+  .mk (n.1 + k.1, n.2 + k.2)
+```
+
+Lifting it to the quotient requires a proof that addition respects the equivalence relation:
+```lean
+instance : Add Z where
+  add (n : Z) :=
+    n.lift₂ add' <| by
+      intro n k n' k'
+      intro heq heq'
+      apply Quotient.sound
+      simp only [instHasEquivOfSetoid, Setoid.r, Z.eq] at *
+      cases n; cases k; cases n'; cases k'
+      simp_all
+      omega
+```
+:::
+
+## Proofs About Quotients
+
+The fundamental tools for proving properties of elements of quotient types are
+
+{docstring Quotient.sound}
+
+{docstring Quotient.ind}
+
+# Logical Model
+
+Like functions and universes, quotient types are a built-in feature of Lean.
+The fundamental quotient type API consists of {lean}`Quot`, {name}`Quot.mk`, {name}`Quot.lift`, {name}`Quot.ind`, and {name}`Quot.sound`.
+The first four are constants, while {name}`Quot.sound` is an axiom.
+
+{docstring Quot}
+
+{docstring Quot.mk}
+
+{docstring Quot.lift}
+
+{docstring Quot.ind}
+
+{docstring Quot.sound}
+
+```lean (show := false)
+section
+variable
+  (α β : Sort u)
+  (r : α → α → Prop)
+  (f : α → β)
+  (resp : ∀ x y, r x y → f x = f y)
+  (x : α)
+```
+In addition to the above constants, Lean's kernel contains a reduction rule for {name}`Quot.lift` that causes it to reduce when used with {name}`Quot.mk`, analogous to {tech}[ι-reduction] for inductive types.
+Given a relation {lean}`r` over {lean}`α`, a function {lean}`f` from {lean}`α` to {lean}`β`, and a proof {lean}`resp` that {lean}`f` respects {lean}`r`, the term {lean}`Quot.lift f resp (Quot.mk r x)` is {tech key:="definitional equality"}[definitionally equal] to {lean}`f x`.
+
+```lean (show := false)
+end
+```
+
+```lean
+variable
+  (r : α → α → Prop)
+  (f : α → β)
+  (ok : ∀ x y, r x y → f x = f y)
+  (x : α)
+
+example : Quot.lift f ok (Quot.mk r x) = f x := rfl
+```
+
+# Squash Types
+
+{docstring Squash}
+
+{docstring Squash.mk}
+
+{docstring Squash.lift}
diff --git a/Manual/Types.lean b/Manual/Types.lean
index 80ca210d..542deeba 100644
--- a/Manual/Types.lean
+++ b/Manual/Types.lean
@@ -10,6 +10,7 @@ import Manual.Meta
 
 import Manual.Language.Functions
 import Manual.Language.InductiveTypes
+import Manual.Quotients
 
 open Verso.Genre Manual
 
@@ -528,13 +529,4 @@ def L := List (Type 0)
 
 {include 0 Language.InductiveTypes}
 
-
-# Quotients
-%%%
-tag := "quotients"
-%%%
-
-:::planned 51
- * Define {deftech}[quotient] type
- * Show the computation rule
-:::
+{include 0 Manual.Quotients}
diff --git a/lake-manifest.json b/lake-manifest.json
index 34a71e2e..67a1fb7d 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "844b9a53cf7acd71e0e81a3a56608bb28215646d",
+   "rev": "73ee3629d01f3255b23645f56d8e587e1337a01f",
    "name": "subverso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,20 +15,20 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "24823788b8064cc2ff7767207afbfd4ad9083f47",
+   "rev": "bef462ba6d207757d877d1e4488ccd9dfa2c8409",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": false,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/david-christiansen/md4lean",
+  {"url": "https://github.com/acmepjz/md4lean",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "6f0beb756af7de9ebd0bf38044bc9ac34419cacd",
+   "rev": "7cf25ec0edf7a72830379ee227eefdaa96c48cfb",
    "name": "MD4Lean",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "parser",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"}],
  "name": "«verso-manual»",

From 1762d87fcd1843645b12adb390236c4ec6a32303 Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@davidchristiansen.dk>
Date: Wed, 29 Jan 2025 22:42:11 +0100
Subject: [PATCH 2/7] Quotient draft completed

---
 Manual/Language.lean                |   3 +
 Manual/Language/InductiveTypes.lean |   2 +-
 Manual/Quotients.lean               | 342 ++++++++++++++++++++++++++--
 Manual/Types.lean                   |   2 +-
 4 files changed, 324 insertions(+), 25 deletions(-)

diff --git a/Manual/Language.lean b/Manual/Language.lean
index 73e3a4cd..393ea4a3 100644
--- a/Manual/Language.lean
+++ b/Manual/Language.lean
@@ -574,6 +574,9 @@ scoped
 :::
 
 # Axioms
+%%%
+tag := "axioms"
+%%%
 
 :::planned 78
 Describe {deftech}_axioms_ in detail
diff --git a/Manual/Language/InductiveTypes.lean b/Manual/Language/InductiveTypes.lean
index 29a4088c..5b8d07be 100644
--- a/Manual/Language/InductiveTypes.lean
+++ b/Manual/Language/InductiveTypes.lean
@@ -23,7 +23,7 @@ tag := "inductive-types"
 
 
 {deftech}_Inductive types_ are the primary means of introducing new types to Lean.
-While {tech}[universes] and {tech}[functions] are built-in primitives that could not be added by users, every other type in Lean is either an inductive type or defined in terms of universes, functions, and inductive types.
+While {tech}[universes], {tech}[functions], and {tech}[quotient types] are built-in primitives that could not be added by users, every other type in Lean is either an inductive type or defined in terms of universes, functions, and inductive types.
 Inductive types are specified by their {deftech}_type constructors_ {index}[type constructor] and their {deftech}_constructors_; {index}[constructor] their other properties are derived from these.
 Each inductive type has a single type constructor, which may take both {tech}[universe parameters] and ordinary parameters.
 Inductive types may have any number of constructors; these constructors introduce new values whose types are headed by the inductive type's type constructor.
diff --git a/Manual/Quotients.lean b/Manual/Quotients.lean
index 5e0c3f23..ec5eb07e 100644
--- a/Manual/Quotients.lean
+++ b/Manual/Quotients.lean
@@ -18,11 +18,6 @@ open Verso.Genre Manual
 tag := "quotients"
 %%%
 
-:::planned 51
- * Define {deftech}[quotient] type
- * Show the computation rule
-:::
-
 
 {deftech}_Quotient types_ allow a new type to be formed by decreasing the granularity of an existing type's propositional equality.
 In particular, given an type $`A` and an equivalence relation $`\sim`, the quotient $`A / \sim` contains the same elements as $`A`, but every pair of elements that are related by $`\sim` are considered equal.
@@ -33,7 +28,8 @@ In particular, all functions from a quotient type must prove that they respect t
 {docstring Quotient}
 
 :::paragraph
-Quotients are widely used in mathematics:
+Quotient types are not widely used in programming.
+However, they occur regularly in mathematics:
 
 : Integers
 
@@ -50,23 +46,107 @@ Quotients are widely used in mathematics:
   The real numbers can be represented as a Cauchy sequence, but this encoding is not unique.
   Using a quotient type, two Cauchy sequences can be made equal when their difference converges to zero.
 
+: Finite Sets
+
+  Finite sets can be represented as lists of elements.
+  With a quotient types, two finite sets can be made equal if they contain the same elements; this definition does not impose any requirements (such as decidable equality or an ordering relation) on the type of elements.
+
 :::
 
-:::TODO
+One alternative to quotient types would be to reason directly about the equivalence classes introduced by the relation.
+The downside of this approach is that it does not allow _computation_: in addition to knowing _that_ there is an integer that is the sum of 5 and 8, it is useful for $`5 + 8 = 13` to not be a theorem that requires proof.
+Defining functions out of sets of equivalence classes relies on noncomputational classical reasoning principles.
 
-Ask colleagues for a couple more good examples here
+# Alternatives
 
-:::
+Quotient types are not the only way to implement quotients.
+An alternative is to select a canonical representative for each equivalence class induced by the equivalence relation, and then pair an element of the underlying type with a proof that it is such a canonical representative.
+These manually constructed quotients are often much easier to work with than full quotient types, but not all quotients can be implemented this way.
 
-Quotient types are not widely used in programming.
+:::example "Manually Quotiented Integers"
+When implemented as pairs of {lean}`Nat`s, each equivalence class according to the desired equality for integers has a canonical representative in which at least one of the {lean}`Nat`s is zero.
+This can be represented as a Lean structure:
+```lean
+structure Z where
+  a : Nat
+  b : Nat
+  canonical : a = 0 ∨ b = 0
+```
+Due to {tech}[proof irrelevance], every value of this structure type that represents the same integer is _already_ equal.
+Constructing a {lean}`Z` can be made more convenient with a wrapper that uses the fact that subtraction of natural numbers truncates at zero to automate the construction of the proof:
+```lean
+def Z.mk' (n k : Nat) : Z where
+  a := n - k
+  b := k - n
+  canonical := by omega
+```
+
+This construction respects the equality demanded of integers:
+```lean
+theorem Z_mk'_respects_eq :
+    (Z.mk' n k = Z.mk' n' k') ↔ (n + k' = n' + k) := by
+  simp [Z.mk']
+  omega
+```
+
+To use this type in examples, it's convenient to have {name}`Neg`, {name}`OfNat`, and {name}`ToString` instances.
+These instances make it easier to read or write examples.
+
+```lean
+instance : Neg Z where
+  neg n := Z.mk' n.b n.a
+
+instance : OfNat Z n where
+  ofNat := Z.mk' n 0
+
+instance : ToString Z where
+  toString n :=
+    if n.a = 0 then
+      if n.b = 0 then "0"
+      else s!"-{n.b}"
+    else toString n.a
+```
+```lean (name := intFive)
+#eval (5 : Z)
+```
+```leanOutput intFive
+5
+```
+```lean (name := intMinusFive)
+#eval (-5 : Z)
+```
+```leanOutput intMinusFive
+-5
+```
+
+
+Addition is addition of the underlying {lean}`Nat`s:
+```lean
+instance : Add Z where
+  add n k := Z.mk' (n.a + k.a) (n.b + k.b)
+```
+
+```lean (name := addInt)
+#eval (-5 + 22: Z)
+```
+```leanOutput addInt
+17
+```
+
+Because each equivalence class is uniquely represented, there's no need to write a proof that these functions from {lean}`Z` respect the equvialence relation.
+
+:::
 
 
 # Setoids
+%%%
+tag := "setoids"
+%%%
 
 Quotient types are built on setoids.
 A {deftech}_setoid_ is a type paired with a distinguished equivalence relation.
 Unlike a quotient type, the abstraction barrier is not enforced, and proof automation designed around equality cannot be used with the setoid's equivalence relation.
-Setoids are primarily used as a building block for quotient types.
+Setoids are useful on their own, in addition to being a building block for quotient types.
 
 {docstring Setoid}
 
@@ -74,7 +154,6 @@ Setoids are primarily used as a building block for quotient types.
 
 An {deftech}_equivalence relation_ is a relation that is reflexive, symmetric, and transitive.
 
-
 :::syntax term (title := "Equivalence Relations")
 Equivalence according to some canonical equivalence relation for a type is written using `≈`, which is overloaded using the {tech}[type class] {name}`HasEquiv`.
 ```grammar
@@ -97,20 +176,38 @@ The fact that a relation {lean}`r` is actually an equivalence relation is stated
 end
 ```
 
+Every {name}`Setoid` instance leads to a corresponding {name}`HasEquiv` instance.
+
+```lean (show := false)
+-- Check preceding para
+section
+variable {α : Sort u} [Setoid α]
+/-- info: instHasEquivOfSetoid -/
+#guard_msgs in
+#synth HasEquiv α
+end
+```
+
 # Quotient API
 
+The quotient API relies on a pre-existing {name}`Setoid` instance.
+
 ## Introducing Quotients
 
-The type {lean}`Quotient` expects an instance of {lean}`Setoid` as its explicit parameter.
+The type {lean}`Quotient` expects an instance of {lean}`Setoid` as an ordinary parameter, rather than as an {tech}[instance implicit] parameter.
+This helps ensure that the quotient uses the intended equivalence relation.
+The instance can be provided either by naming the instance or by using {name}`inferInstance`.
+
 A value in the quotient is a value from the setoid's underlying type, wrapped in {lean}`Quotient.mk`.
 
 {docstring Quotient.mk}
 
 {docstring Quotient.mk'}
 
-:::example "The Integers"
-The integers can be defined as pairs of natural numbers where the represented integer is the difference of the two numbers.
+:::example "The Integers as a Quotient Type"
+The integers, defined as pairs of natural numbers where the represented integer is the difference of the two numbers, can be represented via a quotient type.
 This representation is not unique: both {lean}`(4, 7)` and {lean}`(1, 4)` represent {lean type:="Int"}`-3`.
+
 Two encoded integers should be considered equal when they are related by {name}`Z.eq`:
 
 ```lean
@@ -139,7 +236,7 @@ def Z.eq.eqv : Equivalence Z.eq where
 
 Thus, it can be used as a {name}`Setoid`:
 ```lean
-instance Z.instSetoid : Setoid Z'where
+instance Z.instSetoid : Setoid Z' where
   r := Z.eq
   iseqv := Z.eq.eqv
 ```
@@ -159,7 +256,7 @@ However, numeric literals are even more convenient.
 An {name}`OfNat` instance allows numeric literals to be used for integers:
 ```lean
 instance : OfNat Z n where
-  ofNat := .mk _ (n, 0)
+  ofNat := Z.mk (n, 0)
 ```
 :::
 
@@ -167,7 +264,7 @@ instance : OfNat Z n where
 
 ## Eliminating Quotients
 
-Functions from quotients can be defined based on functions from the underlying type by proving that the function respects the quotient's equivalence relation.
+Functions from quotients can be defined by proving that a function from the underlying type respects the quotient's equivalence relation.
 This is accomplished using {lean}`Quotient.lift`.
 
 {docstring Quotient.lift}
@@ -216,7 +313,7 @@ instance : Neg Z where
     Quotient.lift neg' <| by
       intro n k equiv
       apply Quotient.sound
-      simp only [instHasEquivOfSetoid, Setoid.r, Z.eq] at *
+      simp only [· ≈ ·, Setoid.r, Z.eq] at *
       omega
 ```
 
@@ -235,7 +332,7 @@ instance : Add Z where
       intro n k n' k'
       intro heq heq'
       apply Quotient.sound
-      simp only [instHasEquivOfSetoid, Setoid.r, Z.eq] at *
+      simp only [· ≈ ·, Setoid.r, Z.eq] at *
       cases n; cases k; cases n'; cases k'
       simp_all
       omega
@@ -244,17 +341,96 @@ instance : Add Z where
 
 ## Proofs About Quotients
 
-The fundamental tools for proving properties of elements of quotient types are
+The fundamental tools for proving properties of elements of quotient types are the soundness axiom and the induction principle.
+The soundness axiom states that if two elements of the underlying type are related by the quotient's equivalence relation, then they are equal in the quotient type.
+The induction principle follows the structure of recursors for inductive types: in order to prove that a predicate holds all elements of a quotient type, it suffices to prove that it holds for an application of {name}`Quotient.mk` to each element of the underlying type.
+Because {name}`Quotient` is not an {tech}[inductive type], tactics such as {tactic}`cases` and {tactic}`induction` require that {name}`Quotient.ind` be specified explicitly with the {keyword}`using` modifier.
 
 {docstring Quotient.sound}
 
 {docstring Quotient.ind}
 
+:::example "Proofs About Quotients"
+
+```lean (show := false)
+def Z' : Type := Nat × Nat
+
+def Z.eq (n k : Z') : Prop :=
+  n.1 + k.2 = n.2 + k.1
+
+def Z.eq.eqv : Equivalence Z.eq where
+  refl := by
+    intro (x, y)
+    simp_arith [eq]
+  symm := by
+    intro (x, y) (x', y') heq
+    simp_all only [eq]
+    omega
+  trans := by
+    intro (x, y) (x', y') (x'', y'')
+    intro heq1 heq2
+    simp_all only [eq]
+    omega
+
+instance Z.instSetoid : Setoid Z' where
+  r := Z.eq
+  iseqv := Z.eq.eqv
+
+def Z : Type := Quotient Z.instSetoid
+
+def Z.mk (n : Z') : Z := Quotient.mk _ n
+
+def neg' : Z' → Z
+  | (x, y) => .mk (y, x)
+
+instance : Neg Z where
+  neg :=
+    Quotient.lift neg' <| by
+      intro n k equiv
+      apply Quotient.sound
+      simp only [· ≈ ·, Setoid.r, Z.eq] at *
+      omega
+
+def add' (n k : Nat × Nat) : Z :=
+  .mk (n.1 + k.1, n.2 + k.2)
+
+instance : Add Z where
+  add (n : Z) :=
+    n.lift₂ add' <| by
+      intro n k n' k'
+      intro heq heq'
+      apply Quotient.sound
+      simp only [· ≈ ·, Setoid.r, Z.eq] at *
+      cases n; cases k; cases n'; cases k'
+      simp_all
+      omega
+```
+
+Given the definition of integers as a quotient type from the prior examples, {name}`Quotient.ind` and {name}`Quotient.sound` can be used to prove that negation is an additive inverse.
+First, {lean}`Quotient.ind` is used to replace instances of `n` with applications of {name}`Quotient.mk`.
+Having done so, the left side of the equality becomes definitionally equal to a single application of {name}`Quotient.mk`, via unfolding definitions and the computation rule for {name}`Quotient.lift`.
+This makes {name}`Quotient.sound` applicable, which yields a new goal: to show that both sides are related by the equivalence relation.
+This is provable using {tactic}`simp_arith`.
+
+```lean
+theorem Z.add_neg_inverse (n : Z) : n  + (-n) = 0 := by
+  cases n using Quotient.ind
+  apply Quotient.sound
+  simp_arith [· ≈ ·, Setoid.r, eq]
+```
+
+:::
+
 # Logical Model
 
-Like functions and universes, quotient types are a built-in feature of Lean.
+Like functions and universes, quotient types are a built-in feature of Lean's type system.
+However, the underlying primitives are based on the somewhat simpler {name}`Quot` type rather than on {name}`Quotient`, and {name}`Quotient` is defined in terms of {name}`Quot`.
+The primary difference is that {name}`Quot` is based on an arbitrary relation, rather than a {name}`Setoid` instance.
+The provided relation need not be an equivalence relation; the rules that govern {name}`Quot` and {name}`Eq` automatically extend the provided relation into its reflexive, transitive, symmetric closure.
+When the relation is already an equivalence relation, {name}`Quotient` should be used instead of {name}`Quot` so Lean can make use of the fact that the relation is an equivalence relation.
+
 The fundamental quotient type API consists of {lean}`Quot`, {name}`Quot.mk`, {name}`Quot.lift`, {name}`Quot.ind`, and {name}`Quot.sound`.
-The first four are constants, while {name}`Quot.sound` is an axiom.
+These are used in the same way as their {name}`Quotient`-based counterparts.
 
 {docstring Quot}
 
@@ -282,6 +458,10 @@ Given a relation {lean}`r` over {lean}`α`, a function {lean}`f` from {lean}`α`
 end
 ```
 
+```lean (show := false)
+section
+```
+
 ```lean
 variable
   (r : α → α → Prop)
@@ -292,7 +472,123 @@ variable
 example : Quot.lift f ok (Quot.mk r x) = f x := rfl
 ```
 
+```lean (show := false)
+end
+```
+
+Because {name}`Quot` is not an inductive type, types implemented as quotients may not occur around {ref "nested-inductive-types"}[nested occurrences] in inductive type declarations.
+These types declarations must be rewritten to remove the nested quotient, which can often be done by defining a quotient-free version and then separately defining an equivalence relation that implements the desired equality relation.
+
+:::example "Nested Inductive Types and Quotients"
+
+The nested inductive type of rose trees nests the recursive occurrence of {lean}`RoseTree` under {lean}`List`:
+```lean
+inductive RoseTree (α : Type u) where
+  | leaf : α → RoseTree α
+  | branch : List (RoseTree α) → RoseTree α
+```
+
+However, taking a quotient of the {name}`List` that identifies all elements in the style of {ref "squash-types"}[squash types] causes Lean to reject the declaration:
+```lean (error := true) (name := nestedquot)
+inductive SetTree (α : Type u) where
+  | leaf : α → SetTree α
+  | branch :
+    Quot (fun (xs ys : List (SetTree α)) => True) →
+    SetTree α
+```
+```leanOutput nestedquot
+(kernel) arg #2 of 'SetTree.branch' contains a non valid occurrence of the datatypes being declared
+```
+
+:::
+
+
+# Quotients and Function Extensionality
+
+:::::keepEnv
+
+Because Lean's definitional equality includes a computational reduction rule for {lean}`Quot.lift`, quotient types are used in the standard library to prove function extensionality, which would need to be an {ref "axioms"}[axiom] otherwise.
+This is done by first defining a type of functions quotiented by extensional equality, for which extensional equality holds by definition.
+
+```lean
+variable {α : Sort u} {β : α → Sort v}
+
+def extEq (f g : (x : α) → β x) : Prop :=
+  ∀ x, f x = g x
+
+def ExtFun (α : Sort u) (β : α → Sort v) :=
+  Quot (@extEq α β)
+```
+
+Extensional functions can be applied just like ordinary functions.
+Application respects extensional equality by definition: if applying to functions gives equal results, then applying them gives equal results.
+```lean
+def extApp
+    (f : ExtFun α β)
+    (x : α) :
+    β x :=
+  f.lift (· x) fun g g' h => by
+    exact h x
+```
+
+```lean (show := false)
+section
+variable (f : (x : α) → β x)
+```
+To show that two functions that are extensionally equal are in fact equal, it suffices to show that the functions that result from extensionally applying the corresponding extensional functions are equal.
+This is because
+```leanTerm
+extApp (Quot.mk _ f)
+```
+is definitionally equal to
+```leanTerm
+fun x => (Quot.mk extEq f).lift (· x) (fun _ _ h => h x)
+```
+which is definitionally equal to {lean}`fun x => f x`, which is definitionally equal (by {tech}[η-equivalence]) to {lean}`f`.
+
+```lean (show := false)
+end
+```
+
+From here, it is enough to show that the extensional versions of the two functions are equal.
+This is true due to {name}`Quot.sound`: the fact that they are in the quotient's equivalence relation is an assumption.
+This proof is a much more explicit version of the one in the standard library:
+
+```lean
+theorem funext'
+    {f g : (x : α) → β x}
+    (h : ∀ x, f x = g x) :
+    f = g := by
+  suffices extApp (Quot.mk _ f) = extApp (Quot.mk _ g) by
+    unfold extApp at this
+    dsimp at this
+    exact this
+  suffices Quot.mk extEq f = Quot.mk extEq g by
+    apply congrArg
+    exact this
+  apply Quot.sound
+  exact h
+```
+
+:::::
+
 # Squash Types
+%%%
+tag := "squash-types"
+%%%
+
+```lean (show := false)
+section
+variable {α : Sort u}
+```
+Squash types are a quotient by the relation that relates all elements, transforming it into a {tech}[subsingleton].
+In other words, if {lean}`α` is inhabited, then {lean}`Squash α` has a single element, and if {lean}`α` is uninhabited, then {lean}`Squash α` is also uninhabited.
+Unlike {lean}`Nonempty α`, which is a proposition stating that {lean}`α` is inhabited and is thus represented by a dummy value at runtime, {lean}`Squash α` is a type that is represented identically to {lean}`α`.
+Because {lean}`Squash α` is in the same universe as {lean}`α`, it is not subject to the restrictions on computing data from propositions.
+
+```lean (show := false)
+end
+```
 
 {docstring Squash}
 
diff --git a/Manual/Types.lean b/Manual/Types.lean
index 542deeba..0bc6acb7 100644
--- a/Manual/Types.lean
+++ b/Manual/Types.lean
@@ -81,7 +81,7 @@ export S (f1 f2)
 
 Definitional equality includes η-equivalence of functions and single-constructor inductive types.
 That is, {lean}`fun x => f x` is definitionally equal to {lean}`f`, and {lean}`S.mk x.f1 x.f2` is definitionally equal to {lean}`x`, if {lean}`S` is a structure with fields {lean}`f1` and {lean}`f2`.
-It also features proof irrelevance, so any two proofs of the same proposition are definitionally equal.
+It also features {deftech}_proof irrelevance_: any two proofs of the same proposition are definitionally equal.
 It is reflexive, symmetric, and a congruence.
 ::::
 

From df55d7e6c03184481359999dab7db8e58abb6d34 Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@davidchristiansen.dk>
Date: Wed, 29 Jan 2025 23:09:39 +0100
Subject: [PATCH 3/7] Fix link and tag sections

---
 Manual/Language/Functions.lean |  2 +-
 Manual/Quotients.lean          | 31 ++++++++++++++++++++++++++++++-
 2 files changed, 31 insertions(+), 2 deletions(-)

diff --git a/Manual/Language/Functions.lean b/Manual/Language/Functions.lean
index 07142607..32a358a8 100644
--- a/Manual/Language/Functions.lean
+++ b/Manual/Language/Functions.lean
@@ -169,7 +169,7 @@ In addition to reduction and renaming of bound variables, definitional equality
 Given {lean}`f` with type {lean}`(x : α) → β x`, {lean}`f` is definitionally equal to {lean}`fun x => f x`.
 ::::
 
-When reasoning about functions, the theorem {lean}`funext`{margin}[Unlike some intensional type theories, {lean}`funext` is a theorem in Lean. It can be proved using {tech}[quotient] types.] or the corresponding tactics {tactic}`funext` or {tactic}`ext` can be used to prove that two functions are equal if they map equal inputs to equal outputs.
+When reasoning about functions, the theorem {lean}`funext`{margin}[Unlike some intensional type theories, {lean}`funext` is a theorem in Lean. It can be proved {ref "quotient-funext"}[using quotient types].] or the corresponding tactics {tactic}`funext` or {tactic}`ext` can be used to prove that two functions are equal if they map equal inputs to equal outputs.
 
 {docstring funext}
 
diff --git a/Manual/Quotients.lean b/Manual/Quotients.lean
index ec5eb07e..e9b47a3d 100644
--- a/Manual/Quotients.lean
+++ b/Manual/Quotients.lean
@@ -57,7 +57,11 @@ One alternative to quotient types would be to reason directly about the equivale
 The downside of this approach is that it does not allow _computation_: in addition to knowing _that_ there is an integer that is the sum of 5 and 8, it is useful for $`5 + 8 = 13` to not be a theorem that requires proof.
 Defining functions out of sets of equivalence classes relies on noncomputational classical reasoning principles.
 
-# Alternatives
+# Alternatives to Quotient Types
+%%%
+tag := "quotient-alternatives"
+%%%
+
 
 Quotient types are not the only way to implement quotients.
 An alternative is to select a canonical representative for each equivalence class induced by the equivalence relation, and then pair an element of the underlying type with a proof that it is such a canonical representative.
@@ -151,6 +155,9 @@ Setoids are useful on their own, in addition to being a building block for quoti
 {docstring Setoid}
 
 # Equivalence Relations
+%%%
+tag := "equivalence-relations"
+%%%
 
 An {deftech}_equivalence relation_ is a relation that is reflexive, symmetric, and transitive.
 
@@ -189,10 +196,17 @@ end
 ```
 
 # Quotient API
+%%%
+tag := "quotient-api"
+%%%
 
 The quotient API relies on a pre-existing {name}`Setoid` instance.
 
 ## Introducing Quotients
+%%%
+tag := "quotient-intro"
+%%%
+
 
 The type {lean}`Quotient` expects an instance of {lean}`Setoid` as an ordinary parameter, rather than as an {tech}[instance implicit] parameter.
 This helps ensure that the quotient uses the intended equivalence relation.
@@ -263,6 +277,10 @@ instance : OfNat Z n where
 
 
 ## Eliminating Quotients
+%%%
+tag := "quotient-elim"
+%%%
+
 
 Functions from quotients can be defined by proving that a function from the underlying type respects the quotient's equivalence relation.
 This is accomplished using {lean}`Quotient.lift`.
@@ -340,6 +358,10 @@ instance : Add Z where
 :::
 
 ## Proofs About Quotients
+%%%
+tag := "quotient-proofs"
+%%%
+
 
 The fundamental tools for proving properties of elements of quotient types are the soundness axiom and the induction principle.
 The soundness axiom states that if two elements of the underlying type are related by the quotient's equivalence relation, then they are equal in the quotient type.
@@ -422,6 +444,10 @@ theorem Z.add_neg_inverse (n : Z) : n  + (-n) = 0 := by
 :::
 
 # Logical Model
+%%%
+tag := "quotient-model"
+%%%
+
 
 Like functions and universes, quotient types are a built-in feature of Lean's type system.
 However, the underlying primitives are based on the somewhat simpler {name}`Quot` type rather than on {name}`Quotient`, and {name}`Quotient` is defined in terms of {name}`Quot`.
@@ -504,6 +530,9 @@ inductive SetTree (α : Type u) where
 
 
 # Quotients and Function Extensionality
+%%%
+tag := "quotient-funext"
+%%%
 
 :::::keepEnv
 

From 10f6e73eba1d99f57a885c66eaf41b42c08c6635 Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@davidchristiansen.dk>
Date: Wed, 29 Jan 2025 23:21:27 +0100
Subject: [PATCH 4/7] fix: Vale feedback

---
 .vale/styles/config/ignore/terms.txt | 4 ++++
 Manual/Quotients.lean                | 4 ++--
 2 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/.vale/styles/config/ignore/terms.txt b/.vale/styles/config/ignore/terms.txt
index d35e2604..c317b125 100644
--- a/.vale/styles/config/ignore/terms.txt
+++ b/.vale/styles/config/ignore/terms.txt
@@ -113,6 +113,7 @@ quasiquotation
 quasiquotations
 quasiquote
 quasiquoted
+quotiented
 recursor
 recursor's
 recursors
@@ -121,6 +122,9 @@ scrutinees
 se
 semigroup
 semireducible
+setoid
+setoid's
+setoids
 simp
 simproc
 simprocs
diff --git a/Manual/Quotients.lean b/Manual/Quotients.lean
index e9b47a3d..aa573199 100644
--- a/Manual/Quotients.lean
+++ b/Manual/Quotients.lean
@@ -55,7 +55,7 @@ However, they occur regularly in mathematics:
 
 One alternative to quotient types would be to reason directly about the equivalence classes introduced by the relation.
 The downside of this approach is that it does not allow _computation_: in addition to knowing _that_ there is an integer that is the sum of 5 and 8, it is useful for $`5 + 8 = 13` to not be a theorem that requires proof.
-Defining functions out of sets of equivalence classes relies on noncomputational classical reasoning principles.
+Defining functions out of sets of equivalence classes relies on non-computational classical reasoning principles, while functions from quotient types are ordinary computational functions that additionally respect an equivalence relation.
 
 # Alternatives to Quotient Types
 %%%
@@ -137,7 +137,7 @@ instance : Add Z where
 17
 ```
 
-Because each equivalence class is uniquely represented, there's no need to write a proof that these functions from {lean}`Z` respect the equvialence relation.
+Because each equivalence class is uniquely represented, there's no need to write a proof that these functions from {lean}`Z` respect the equivalence relation.
 
 :::
 

From 0e00c1ecbbb66c8e54e5448e02506c785a00ac7c Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@davidchristiansen.dk>
Date: Thu, 30 Jan 2025 08:52:53 +0100
Subject: [PATCH 5/7] fix: error in proof

---
 Manual/Quotients.lean | 18 +++++++++++++-----
 1 file changed, 13 insertions(+), 5 deletions(-)

diff --git a/Manual/Quotients.lean b/Manual/Quotients.lean
index aa573199..f1b28d6c 100644
--- a/Manual/Quotients.lean
+++ b/Manual/Quotients.lean
@@ -283,10 +283,17 @@ tag := "quotient-elim"
 
 
 Functions from quotients can be defined by proving that a function from the underlying type respects the quotient's equivalence relation.
-This is accomplished using {lean}`Quotient.lift`.
+This is accomplished using {lean}`Quotient.lift` or its binary counterpart {lean}`Quotient.lift₂`.
+The variants {lean}`Quotient.liftOn` and {lean}`Quotient.liftOn₂` place the quotient parameter first rather than last in the parameter list.
 
 {docstring Quotient.lift}
 
+{docstring Quotient.liftOn}
+
+{docstring Quotient.lift₂}
+
+{docstring Quotient.liftOn₂}
+
 :::example "Integer Negation and Addition"
 
 ```lean (show := false)
@@ -350,9 +357,8 @@ instance : Add Z where
       intro n k n' k'
       intro heq heq'
       apply Quotient.sound
-      simp only [· ≈ ·, Setoid.r, Z.eq] at *
       cases n; cases k; cases n'; cases k'
-      simp_all
+      simp_all only [· ≈ ·, Setoid.r, Z.eq]
       omega
 ```
 :::
@@ -422,10 +428,12 @@ instance : Add Z where
       intro n k n' k'
       intro heq heq'
       apply Quotient.sound
-      simp only [· ≈ ·, Setoid.r, Z.eq] at *
       cases n; cases k; cases n'; cases k'
-      simp_all
+      simp_all only [· ≈ ·, Setoid.r, Z.eq]
       omega
+
+instance : OfNat Z n where
+  ofNat := Z.mk (n, 0)
 ```
 
 Given the definition of integers as a quotient type from the prior examples, {name}`Quotient.ind` and {name}`Quotient.sound` can be used to prove that negation is an additive inverse.

From 99651409723b0dbe2fd51619bbadc3f0266f3c6f Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@davidchristiansen.dk>
Date: Thu, 30 Jan 2025 09:31:18 +0100
Subject: [PATCH 6/7] feat: add missing Quotient constants

---
 Manual.lean           |  5 +++++
 Manual/Quotients.lean | 31 +++++++++++++++++++++++++++++++
 2 files changed, 36 insertions(+)

diff --git a/Manual.lean b/Manual.lean
index 3dea10b7..fd110594 100644
--- a/Manual.lean
+++ b/Manual.lean
@@ -284,6 +284,11 @@ String.fromUTF8.loop
 String.one_le_csize
 ```
 
+```exceptions
+Quot.indep
+Quot.lcInv
+```
+
 ```exceptions
 String.sluggify
 ```
diff --git a/Manual/Quotients.lean b/Manual/Quotients.lean
index f1b28d6c..1d69744c 100644
--- a/Manual/Quotients.lean
+++ b/Manual/Quotients.lean
@@ -363,6 +363,13 @@ instance : Add Z where
 ```
 :::
 
+When the function's result type is a {tech}[subsingleton], {name}`Quotient.recOnSubsingleton` or {name}`Quotient.recOnSubsingleton₂` can be used to define the function.
+Because all elements of a subsingleton are equal, such a function automatically respects the equivalence relation, so there is no proof obligation.
+
+{docstring Quotient.recOnSubsingleton}
+
+{docstring Quotient.recOnSubsingleton₂}
+
 ## Proofs About Quotients
 %%%
 tag := "quotient-proofs"
@@ -451,6 +458,16 @@ theorem Z.add_neg_inverse (n : Z) : n  + (-n) = 0 := by
 
 :::
 
+For more specialized use cases, {name}`Quotient.rec`, {name}`Quotient.recOn`, and {name}`Quotient.hrecOn` can be used to define dependent functions from a quotient type to a type in any other universe.
+Stating that a dependent function respects the quotient's equivalence relation requires a means of dealing with the fact that the dependent result type is instantiated with different values from the quotient on each side of the equality.
+{name}`Quotient.rec` and {name}`Quotient.recOn` use the {name}`Quotient.sound` to equate the related elements, inserting the appropriate cast into the statement of equality, while {name}`Quotient.hrecOn` uses heterogeneous equality.
+
+{docstring Quotient.rec}
+
+{docstring Quotient.recOn}
+
+{docstring Quotient.hrecOn}
+
 # Logical Model
 %%%
 tag := "quotient-model"
@@ -510,6 +527,10 @@ example : Quot.lift f ok (Quot.mk r x) = f x := rfl
 end
 ```
 
+{name}`Quot.liftOn` is an version of {name}`Quot.lift` that takes the quotient type's value first, by analogy to {name}`Quotient.liftOn`.
+
+{docstring Quot.liftOn}
+
 Because {name}`Quot` is not an inductive type, types implemented as quotients may not occur around {ref "nested-inductive-types"}[nested occurrences] in inductive type declarations.
 These types declarations must be rewritten to remove the nested quotient, which can often be done by defining a quotient-free version and then separately defining an equivalence relation that implements the desired equality relation.
 
@@ -536,6 +557,16 @@ inductive SetTree (α : Type u) where
 
 :::
 
+Lean also provides convenient elimination from {name}`Quot` into any subsingleton without further proof obligations, along with dependent elimination principles that correspond to those used for {name}`Quotient`.
+
+{docstring Quot.recOnSubsingleton}
+
+{docstring Quot.rec}
+
+{docstring Quot.recOn}
+
+{docstring Quot.hrecOn}
+
 
 # Quotients and Function Extensionality
 %%%

From 9d440d0a70b2af1c4fc7e926d5f41206974db3d3 Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@davidchristiansen.dk>
Date: Fri, 31 Jan 2025 10:07:45 +0100
Subject: [PATCH 7/7] Add sentence about propositional computation rule

---
 Manual/Quotients.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Manual/Quotients.lean b/Manual/Quotients.lean
index 1d69744c..cc31ce3c 100644
--- a/Manual/Quotients.lean
+++ b/Manual/Quotients.lean
@@ -613,6 +613,7 @@ is definitionally equal to
 fun x => (Quot.mk extEq f).lift (· x) (fun _ _ h => h x)
 ```
 which is definitionally equal to {lean}`fun x => f x`, which is definitionally equal (by {tech}[η-equivalence]) to {lean}`f`.
+A propositional version of the computation rule for {name}`Quot.lift` would not suffice, because the reducible expression occurs in the body of a function and rewriting by an equality in a function would already require function extensionality.
 
 ```lean (show := false)
 end