diff --git a/BACKLOG.md b/BACKLOG.md
index 64ea62f..3eec938 100644
--- a/BACKLOG.md
+++ b/BACKLOG.md
@@ -15,6 +15,10 @@ Prove univalence for the category of
   * sets
   * functors and natural transformations
 
+Prove:
+  * `isProp (Product ...)`
+  * `isProp (HasProducts ...)`
+
 * Functor ✓
 * Applicative Functor ✗
   * Lax monoidal functor ✗
diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda
index ce493b6..5e442b3 100644
--- a/src/Cat/Categories/Cat.agda
+++ b/src/Cat/Categories/Cat.agda
@@ -46,9 +46,8 @@ module _ (ℓ ℓ' : Level) where
     open RawCategory RawCat
     isAssociative : IsAssociative
     isAssociative {f = F} {G} {H} = assc {F = F} {G = G} {H = H}
-    -- TODO: Rename `ident'` to `ident` after changing how names are exposed in Functor.
-    ident' : IsIdentity identity
-    ident' = ident-r , ident-l
+    ident : IsIdentity identity
+    ident = ident-r , ident-l
     -- NB! `ArrowsAreSets RawCat` is *not* provable. The type of functors,
     -- however, form a groupoid! Therefore there is no (1-)category of
     -- categories. There does, however, exist a 2-category of 1-categories.
diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index 62a7221..e547a81 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -24,9 +24,6 @@
 -- ------
 --
 -- Propositionality for all laws about the category.
---
--- TODO: An equality principle for categories that focuses on the pure data-part.
---
 {-# OPTIONS --allow-unsolved-metas --cubical #-}
 
 module Cat.Category where
@@ -91,7 +88,7 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
 
   -- | Laws about the data
 
-  -- TODO: It seems counter-intuitive that the normal-form is on the
+  -- FIXME It seems counter-intuitive that the normal-form is on the
   -- right-hand-side.
   IsAssociative : Set (ℓa ⊔ ℓb)
   IsAssociative = ∀ {A B C D} {f : Arrow A B} {g : Arrow B C} {h : Arrow C D}
@@ -286,6 +283,17 @@ record Category (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
 
   open IsCategory isCategory public
 
+Category≡ : {ℓa ℓb : Level} {ℂ 𝔻 : Category ℓa ℓb} → Category.raw ℂ ≡ Category.raw 𝔻 → ℂ ≡ 𝔻
+Category≡ {ℂ = ℂ} {𝔻} eq i = record
+  { raw        = eq i
+  ; isCategory = isCategoryEq i
+  }
+  where
+  open Category
+  module ℂ = Category ℂ
+  isCategoryEq : (λ i → IsCategory (eq i)) [ isCategory ℂ ≡ isCategory 𝔻 ]
+  isCategoryEq = {!!}
+
 -- | Syntax for arrows- and composition in a given category.
 module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
   open Category ℂ
@@ -353,9 +361,7 @@ module Opposite {ℓa ℓb : Level} where
       RawCategory.𝟙        (rawInv _) = 𝟙
       RawCategory._∘_      (rawInv _) = _∘_
 
-    -- TODO: Define and use Monad≡
     oppositeIsInvolution : opposite (opposite ℂ) ≡ ℂ
-    Category.raw        (oppositeIsInvolution i) = rawInv i
-    Category.isCategory (oppositeIsInvolution x) = {!!}
+    oppositeIsInvolution = Category≡ rawInv
 
 open Opposite public
diff --git a/src/Cat/Category/Functor.agda b/src/Cat/Category/Functor.agda
index d627539..6724dee 100644
--- a/src/Cat/Category/Functor.agda
+++ b/src/Cat/Category/Functor.agda
@@ -61,7 +61,7 @@ module _ {ℓc ℓc' ℓd ℓd'}
   record IsFunctor (F : RawFunctor) : 𝓤 where
     open RawFunctor F public
     field
-      -- TODO Really ought to be preserves identity or something like this.
+      -- FIXME Really ought to be preserves identity or something like this.
       isIdentity : IsIdentity
       isDistributive : IsDistributive
 
diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda
index c0c42bf..6ce46bb 100644
--- a/src/Cat/Category/Monad.agda
+++ b/src/Cat/Category/Monad.agda
@@ -250,7 +250,7 @@ module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
         fmap g ∘ fmap f                   ≡⟨⟩
         bind (pure ∘ g) ∘ bind (pure ∘ f) ∎
 
-    -- TODO: Naming!
+    -- FIXME Naming!
     R : EndoFunctor ℂ
     Functor.raw       R = rawR
     Functor.isFunctor R = isFunctorR