From 2fcc5836465983df68bca52883f7a13e88daed2d 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 10:50:18 +0100
Subject: [PATCH] Add note

---
 src/Cat/Category/Product.agda | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Cat/Category/Product.agda b/src/Cat/Category/Product.agda
index 118b72b..dff488a 100644
--- a/src/Cat/Category/Product.agda
+++ b/src/Cat/Category/Product.agda
@@ -60,6 +60,7 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
         ]
 
 module Propositionality {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} {A B : Category.Object ℂ} where
+  -- TODO I'm not sure this is actually provable. Check with Thierry.
   propProduct : isProp (Product ℂ A B)
   propProduct = {!!}