diff --git a/BACKLOG.md b/BACKLOG.md
index 9a72a1d..af3f622 100644
--- a/BACKLOG.md
+++ b/BACKLOG.md
@@ -1,24 +1,12 @@
 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) (idToIso A B)
-    ∀ A   → isContr (Σ[ X ∈ Object ] A ≅ X)
-
 Prove univalence for the category of
   * functors and natural transformations
 
-Prove:
-  * `isProp (Product ...)`
-  * `isProp (HasProducts ...)`
+In AreInverses, dont use the "point-free" version. I.e.:
 
-Rename composition in categories
-
-In stead of using AreInverses, just use a sigma-type
+  `∀ x → f x ≡ g x` rather than `f ≡ g`
 
 Ideas for future work
 ---------------------
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 6bd4bc4..6bb631b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,6 +1,32 @@
 Change log
 =========
 
+Version 1.5.0
+-------------
+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
+  * "pair" category
+
+Finish the proof that products are propositional:
+
+  * `isProp (Product ...)`
+  * `isProp (HasProducts ...)`
+
+Remove --allow-unsolved-metas pragma from various files
+
+Also renamed a lot of different projections. E.g. arrow-composition, etc..
+
 Version 1.4.1
 -------------
 Defines a module to work with equivalence providing a way to go between
diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda
index 3fa14ce..e707b55 100644
--- a/src/Cat/Categories/Sets.agda
+++ b/src/Cat/Categories/Sets.agda
@@ -1,5 +1,5 @@
 -- | The category of homotopy sets
-{-# OPTIONS --allow-unsolved-metas --cubical --caching #-}
+{-# OPTIONS --cubical --caching #-}
 module Cat.Categories.Sets where
 
 open import Cat.Prelude as P
diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index 749ba42..274f94e 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -24,7 +24,7 @@
 -- ------
 --
 -- Propositionality for all laws about the category.
-{-# OPTIONS --allow-unsolved-metas --cubical #-}
+{-# OPTIONS --cubical #-}
 
 module Cat.Category where
 
diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda
index e071d92..8d5abc6 100644
--- a/src/Cat/Category/Monad.agda
+++ b/src/Cat/Category/Monad.agda
@@ -17,7 +17,7 @@ These two formulations are proven to be equivalent:
 The monoidal representation is exposed by default from this module.
  ---}
 
-{-# OPTIONS --cubical --allow-unsolved-metas #-}
+{-# OPTIONS --cubical #-}
 module Cat.Category.Monad where
 
 open import Cat.Prelude
diff --git a/src/Cat/Category/Monad/Kleisli.agda b/src/Cat/Category/Monad/Kleisli.agda
index 75e5a22..e0ebf86 100644
--- a/src/Cat/Category/Monad/Kleisli.agda
+++ b/src/Cat/Category/Monad/Kleisli.agda
@@ -1,7 +1,7 @@
 {---
 The Kleisli formulation of monads
  ---}
-{-# OPTIONS --cubical --allow-unsolved-metas #-}
+{-# OPTIONS --cubical #-}
 open import Agda.Primitive
 
 open import Cat.Prelude
diff --git a/src/Cat/Category/Monad/Monoidal.agda b/src/Cat/Category/Monad/Monoidal.agda
index 86111b6..f5b20ad 100644
--- a/src/Cat/Category/Monad/Monoidal.agda
+++ b/src/Cat/Category/Monad/Monoidal.agda
@@ -1,7 +1,7 @@
 {---
 Monoidal formulation of monads
  ---}
-{-# OPTIONS --cubical --allow-unsolved-metas #-}
+{-# OPTIONS --cubical #-}
 open import Agda.Primitive
 
 open import Cat.Prelude
diff --git a/src/Cat/Category/Monad/Voevodsky.agda b/src/Cat/Category/Monad/Voevodsky.agda
index e5ff355..abc8438 100644
--- a/src/Cat/Category/Monad/Voevodsky.agda
+++ b/src/Cat/Category/Monad/Voevodsky.agda
@@ -1,7 +1,7 @@
 {-
 This module provides construction 2.3 in [voe]
 -}
-{-# OPTIONS --cubical --allow-unsolved-metas --caching #-}
+{-# OPTIONS --cubical --caching #-}
 module Cat.Category.Monad.Voevodsky where
 
 open import Cat.Prelude
diff --git a/src/Cat/Category/NaturalTransformation.agda b/src/Cat/Category/NaturalTransformation.agda
index 1a7223d..3771643 100644
--- a/src/Cat/Category/NaturalTransformation.agda
+++ b/src/Cat/Category/NaturalTransformation.agda
@@ -17,7 +17,7 @@
 -- Functions for manipulating the above:
 --
 -- * A composition operator.
-{-# OPTIONS --allow-unsolved-metas --cubical #-}
+{-# OPTIONS --cubical #-}
 open import Cat.Prelude
 
 open import Data.Nat using (_≤′_ ; ≤′-refl ; ≤′-step)
diff --git a/src/Cat/Category/Product.agda b/src/Cat/Category/Product.agda
index c0c68c3..4856668 100644
--- a/src/Cat/Category/Product.agda
+++ b/src/Cat/Category/Product.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --allow-unsolved-metas --cubical --caching #-}
+{-# OPTIONS --cubical --caching #-}
 module Cat.Category.Product where
 
 open import Cat.Prelude as P hiding (_×_ ; fst ; snd)
@@ -299,7 +299,7 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
         open Σ ump renaming (fst to f')
         open Σ (snd ump) renaming (fst to f'-cond)
         𝒻 : Arrow 𝒴 𝒳
-        𝒻 = f' , {!f'-cond!}
+        𝒻 = f' , f'-cond
         contractible : (f : Arrow 𝒴 𝒳) → 𝒻 ≡ f
         contractible ff@(f , f-cond) = res
           where
diff --git a/src/Cat/Category/Yoneda.agda b/src/Cat/Category/Yoneda.agda
index afea823..c02274b 100644
--- a/src/Cat/Category/Yoneda.agda
+++ b/src/Cat/Category/Yoneda.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --allow-unsolved-metas --cubical #-}
+{-# OPTIONS --cubical #-}
 
 module Cat.Category.Yoneda where
 
diff --git a/src/Cat/Equivalence.agda b/src/Cat/Equivalence.agda
index 1103b9f..6e55cbf 100644
--- a/src/Cat/Equivalence.agda
+++ b/src/Cat/Equivalence.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --allow-unsolved-metas --cubical #-}
+{-# OPTIONS --cubical #-}
 module Cat.Equivalence where
 
 open import Cubical.Primitives