diff --git a/BACKLOG.md b/BACKLOG.md
index 7e18b07..9a72a1d 100644
--- a/BACKLOG.md
+++ b/BACKLOG.md
@@ -10,13 +10,16 @@ Prove that these two formulations of univalence are equivalent:
     ∀ A   → isContr (Σ[ X ∈ Object ] A ≅ X)
 
 Prove univalence for the category of
-  * the opposite category
   * functors and natural transformations
 
 Prove:
   * `isProp (Product ...)`
   * `isProp (HasProducts ...)`
 
+Rename composition in categories
+
+In stead of using AreInverses, just use a sigma-type
+
 Ideas for future work
 ---------------------