From 6db2a3e5d4100a5227c8833a7cd48f90730ab1b4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Tue, 13 Mar 2018 10:40:43 +0100
Subject: [PATCH] Update changelog and backlog

---
 BACKLOG.md   |  5 -----
 CHANGELOG.md | 20 +++++++++++++++++++-
 2 files changed, 19 insertions(+), 6 deletions(-)

diff --git a/BACKLOG.md b/BACKLOG.md
index 3eec938..ed1b205 100644
--- a/BACKLOG.md
+++ b/BACKLOG.md
@@ -1,14 +1,9 @@
 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
diff --git a/CHANGELOG.md b/CHANGELOG.md
index a7a3d14..625d640 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,9 +1,27 @@
 Changelog
 =========
 
+Version 1.4.0
+-------------
+Adds documentation to a number of modules.
+
+Adds an "equality principle" for categories and monads.
+
+Prove that `IsMonad` is a mere proposition.
+
+Provides the yoneda embedding without relying on the existence of a category of
+categories. This is acheived by providing some of the data needed to make a ccc
+out of the category of categories without actually having such a category.
+
+Renames functors object map and arrow map to `omap` and `fmap`.
+
+Prove that kleisli- and monoidal- monads are equivalent!
+
+[WIP] Started working on the proofs for univalence for the category of sets and
+the category of functors.
+
 Version 1.3.0
 -------------
-
 Removed unused modules and streamlined things more: All specific categories are
 in the namespace `Cat.Categories`.