1 Things to describe not in the original quotient paper:

     2 

     3 * Type maps and Relation maps (show the case for functions)

     4 * Quotient extensions

     5 * Respectfulness and preservation

     6   - Show special cases for quantifiers and lambda

     7 * Quotient-type locale

     8   - Show the proof as much simpler than Homeier's one

     9 * Infrastructure for storing theorems (rsp, prs, eqv, quot and idsimp)

    10 * Lifting vs Descending vs quot_lifted

    11   - automatic theorem translation heuristic

    12 * Partial equivalence quotients

    13   - Bounded abstraction

    14   - Respects

    15   - partial_descending

    16 * The heuristics for automatic regularization, injection and cleaning.

    17 * A complete example of a lifted theorem together with the regularized

    18   injected and cleaned statement

    19 * Examples of quotients and properties that we used the package for.

    20 * co/contra-variance from Ondrej should be taken into account