From 4ae898dfe017403b6389f2057a0c6616190e0169 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Thu, 22 Mar 2018 14:51:43 +0100
Subject: [PATCH] Update backlog and changelog

---
 BACKLOG.md   | 32 +++++++++++++++++++++++++-------
 CHANGELOG.md | 19 +++++++++++++++++++
 2 files changed, 44 insertions(+), 7 deletions(-)

diff --git a/BACKLOG.md b/BACKLOG.md
index c8fb54b..91d6b63 100644
--- a/BACKLOG.md
+++ b/BACKLOG.md
@@ -4,17 +4,37 @@ Backlog
 Prove postulates in `Cat.Wishlist`:
  * `ntypeCommulative : n ≤ m → HasLevel ⟨ n ⟩₋₂ A → HasLevel ⟨ m ⟩₋₂ A`
 
+Prove that these two formulations of univalence are equivalent:
+
+    ∀ A B → isEquiv (A ≡ B) (A ≅ B) (id-to-iso A B)
+    ∀ A   → isContr (Σ[ X ∈ Object ] A ≅ X)
+
 Prove univalence for the category of
   * the opposite category
-  * sets
-    This does not follow trivially from `Cubical.Univalence.univalence` because
-    objects are not `Set` but `hSet`
   * functors and natural transformations
 
 Prove:
   * `isProp (Product ...)`
   * `isProp (HasProducts ...)`
 
+Ideas for future work
+---------------------
+
+It would be nice if my formulation of monads is not so "stand-alone" as it is at
+the moment.
+
+We can built up the notion of monads and related concept in multiple ways as
+demonstrated in the two equivalent formulations of monads (kleisli/monoidal):
+There seems to be a category-theoretic approach and an approach more in the
+style of functional programming as e.g. the related typeclasses in the
+standard library of Haskell.
+
+It would be nice to build up this hierarchy in two ways: The
+"category-theoretic" way and the "functional programming" way.
+
+Here is an overview of some of the concepts that need to be developed to acheive
+this:
+
 * Functor ✓
 * Applicative Functor ✗
   * Lax monoidal functor ✗
@@ -26,9 +46,7 @@ Prove:
   * Monoidal monad ✓
   * Kleisli monad ✓
   * Kleisli ≃ Monoidal ✓
-  * Problem 2.3 in [voe]
+  * Problem 2.3 in [voe] ✓
     * 1st contruction ~ monoidal ✓
     * 2nd contruction ~ klesli ✓
-      * 1st ≃ 2nd ✗
-        I've managed to set this up so I should be able to reuse the proof that
-        Kleisli ≃ Monoidal, but I don't know why it doesn't typecheck.
+      * 1st ≃ 2nd ✓
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 625d640..42ab3e0 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,6 +1,25 @@
 Changelog
 =========
 
+Version 1.4.1
+-------------
+Defines a module to work with equivalence providing a way to go between
+equivalences and quasi-inverses (in the parlance of HoTT).
+
+Finishes the proof that the category of homotopy-sets are univalent.
+
+Defines a custom "prelude" module that wraps the `cubical` library and provides
+a few utilities.
+
+Reorders Category.isIdentity such that the left projection is left identity.
+
+Include some text for the half-time report.
+
+Renames IsProduct.isProduct to IsProduct.ump to avoid ambiguity in some
+circumstances.
+
+[WIP]: Adds some stuff about propositionality for products.
+
 Version 1.4.0
 -------------
 Adds documentation to a number of modules.