--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Quotient-Paper-jv/TODO	Tue Dec 20 17:54:53 2011 +0900
@@ -0,0 +1,20 @@
+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