From 472dbba84de9b5a24752c70ba0c6eba628570df7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Mon, 9 Apr 2018 16:03:02 +0200
Subject: [PATCH] Update backlog

---
 BACKLOG.md | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

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