Things to describe not in the original quotient paper:* Type maps and Relation maps (show the case for functions)* Quotient extensions* Respectfulness and preservation - Show special cases for quantifiers and lambda* Quotient-type locale - Show the proof as much simpler than Homeier's one* Infrastructure for storing theorems (rsp, prs, eqv, quot and idsimp)* Lifting vs Descending vs quot_lifted - automatic theorem translation heuristic* Partial equivalence quotients - Bounded abstraction - Respects - partial_descending* The heuristics for automatic regularization, injection and cleaning.* A complete example of a lifted theorem together with the regularized injected and cleaned statement* Examples of quotients and properties that we used the package for.* co/contra-variance from Ondrej should be taken into account