feat: Quotient type chapter

.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

Manual.lean

@@ -254,6 +254,8 @@ Setoid
 Squash
 Subsingleton
 WellFoundedRelation
+Equivalence
+HasEquiv
 Lake
 Lake.RecBuildM
 Lake.FetchM
@@ -282,6 +284,11 @@ String.fromUTF8.loop
 String.one_le_csize
 ```
 
+```exceptions
+Quot.indep
+Quot.lcInv
+```
+
 ```exceptions
 String.sluggify
 ```

Manual/Language.lean

@@ -577,6 +577,9 @@ scoped
 :::
 
 # Axioms
+%%%
+tag := "axioms"
+%%%
 
 :::planned 78
 Describe {deftech}_axioms_ in detail

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}
 

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.