From 63b5f5c68d9ba9f16469739b508a73b425ad9b2b 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:45:15 +0100
Subject: [PATCH] Use long name for product object

---
 src/Cat/Categories/Cat.agda   |  6 +++---
 src/Cat/Categories/Sets.agda  |  6 +++---
 src/Cat/Category/Product.agda | 11 ++++++-----
 3 files changed, 12 insertions(+), 11 deletions(-)

diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda
index 8c29f7b..121d83d 100644
--- a/src/Cat/Categories/Cat.agda
+++ b/src/Cat/Categories/Cat.agda
@@ -152,9 +152,9 @@ module _ {ℓ ℓ' : Level} (unprovable : IsCategory (RawCat ℓ ℓ')) where
       module P = CatProduct ℂ 𝔻
 
       rawProduct : RawProduct Catℓ ℂ 𝔻
-      RawProduct.obj   rawProduct = P.obj
-      RawProduct.proj₁ rawProduct = P.proj₁
-      RawProduct.proj₂ rawProduct = P.proj₂
+      RawProduct.object rawProduct = P.obj
+      RawProduct.proj₁  rawProduct = P.proj₁
+      RawProduct.proj₂  rawProduct = P.proj₂
 
       isProduct : IsProduct Catℓ _ _ rawProduct
       IsProduct.isProduct isProduct = P.isProduct
diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda
index d5d92ec..ac6bd72 100644
--- a/src/Cat/Categories/Sets.agda
+++ b/src/Cat/Categories/Sets.agda
@@ -66,9 +66,9 @@ module _ {ℓ : Level} where
             proj₂ lem = refl
 
         rawProduct : RawProduct 𝓢 0A 0B
-        RawProduct.obj   rawProduct = 0A×0B
-        RawProduct.proj₁ rawProduct = Data.Product.proj₁
-        RawProduct.proj₂ rawProduct = Data.Product.proj₂
+        RawProduct.object rawProduct = 0A×0B
+        RawProduct.proj₁  rawProduct = Data.Product.proj₁
+        RawProduct.proj₂  rawProduct = Data.Product.proj₂
 
         isProduct : IsProduct 𝓢 _ _ rawProduct
         IsProduct.isProduct isProduct {X = X} f g
diff --git a/src/Cat/Category/Product.agda b/src/Cat/Category/Product.agda
index 8150e1b..118b72b 100644
--- a/src/Cat/Category/Product.agda
+++ b/src/Cat/Category/Product.agda
@@ -1,3 +1,4 @@
+{-# OPTIONS --allow-unsolved-metas #-}
 module Cat.Category.Product where
 
 open import Agda.Primitive
@@ -14,9 +15,9 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
     record RawProduct : Set (ℓa ⊔ ℓb) where
       no-eta-equality
       field
-        obj : Object
-        proj₁ : ℂ [ obj , A ]
-        proj₂ : ℂ [ obj , B ]
+        object : Object
+        proj₁  : ℂ [ object , A ]
+        proj₂  : ℂ [ object , B ]
 
     -- FIXME Not sure this is actually a proposition - so this name is
     -- misleading.
@@ -28,7 +29,7 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
 
       -- | Arrow product
       _P[_×_] : ∀ {X} → (π₁ : ℂ [ X , A ]) (π₂ : ℂ [ X , B ])
-        → ℂ [ X , obj ]
+        → ℂ [ X , object ]
       _P[_×_] π₁ π₂ = P.proj₁ (isProduct π₁ π₂)
 
     record Product : Set (ℓa ⊔ ℓb) where
@@ -43,7 +44,7 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
       product : ∀ (A B : Object) → Product A B
 
     _×_ : Object → Object → Object
-    A × B = Product.obj (product A B)
+    A × B = Product.object (product A B)
 
     -- | Parallel product of arrows
     --