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+
−