From fa9a470875e6579aeca9fed0fa55ec96fec8181b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Thu, 8 Mar 2018 00:54:42 +0100
Subject: [PATCH] Update backlog

---
 BACKLOG.md                  | 19 ++++++++++++++++++-
 src/Cat/Categories/Rel.agda |  1 -
 2 files changed, 18 insertions(+), 2 deletions(-)

diff --git a/BACKLOG.md b/BACKLOG.md
index bfbb32b..64ea62f 100644
--- a/BACKLOG.md
+++ b/BACKLOG.md
@@ -4,6 +4,16 @@ Backlog
 Prove univalence for various categories
 
 Prove postulates in `Cat.Wishlist`
+`propHasLevel` should be in `cubical`
+`ntypeCommulative` might be there as well.
+
+Define and use Monad≡
+
+Prove that the opposite category is a category.
+
+Prove univalence for the category of
+  * sets
+  * functors and natural transformations
 
 * Functor ✓
 * Applicative Functor ✗
@@ -11,4 +21,11 @@ Prove postulates in `Cat.Wishlist`
     * Monoidal functor ✗
   * Tensorial strength ✗
 * Category ✓
-  * Monoidal category ✗
\ No newline at end of file
+  * Monoidal category ✗
+* Monad
+  * Monoidal monad ✓
+  * Kleisli monad ✓
+  * Problem 2.3 in voe
+    * 1st contruction ~ monoidal ✓
+    * 2nd contruction ~ klesli ✓
+      * 1st ≃ 2nd ✗
diff --git a/src/Cat/Categories/Rel.agda b/src/Cat/Categories/Rel.agda
index de3d1f2..1dbed3d 100644
--- a/src/Cat/Categories/Rel.agda
+++ b/src/Cat/Categories/Rel.agda
@@ -56,7 +56,6 @@ module _ {A B : Set} {S : Subset (A × B)} (ab : A × B) where
       backwards (a' , (a=a' , a'b∈S)) = subst (sym a=a') a'b∈S
 
       fwd-bwd : (x : (a , b) ∈ S) → (backwards ∘ forwards) x ≡ x
-      -- isbijective x = pathJ (λ y x₁ → (backwards ∘ forwards) x ≡ x) {!!} {!!} {!!}
       fwd-bwd x = pathJprop (λ y _ → y) x
 
       bwd-fwd : (x : Σ[ a' ∈ A ] (a , a') ∈ Diag A × (a' , b) ∈ S)