Restructure products

src/Cat/Categories/Cat.agda

@@ -151,16 +151,17 @@ module _ {ℓ ℓ' : Level} (unprovable : IsCategory (RawCat ℓ ℓ')) where
     private
       module P = CatProduct ℂ 𝔻
 
-      instance
+      rawProduct : RawProduct {ℂ = Catℓ} ℂ 𝔻
-        isProduct : IsProduct Catℓ P.proj₁ P.proj₂
+      RawProduct.obj   rawProduct = P.obj
-        isProduct = P.isProduct
+      RawProduct.proj₁ rawProduct = P.proj₁
+      RawProduct.proj₂ rawProduct = P.proj₂
+
+      isProduct : IsProduct Catℓ rawProduct
+      IsProduct.isProduct isProduct = P.isProduct
 
     product : Product {ℂ = Catℓ} ℂ 𝔻
-    product = record
+    Product.raw       product = rawProduct
-      { obj = P.obj
+    Product.isProduct product = isProduct
-      ; proj₁ = P.proj₁
-      ; proj₂ = P.proj₂
-      }
 
   instance
     hasProducts : HasProducts Catℓ

src/Cat/Categories/Sets.agda

@@ -64,17 +64,17 @@ module _ {ℓ : Level} where
             lem : proj₁ Function.∘′ (f &&& g) ≡ f × proj₂ Function.∘′ (f &&& g) ≡ g
             proj₁ lem = refl
             proj₂ lem = refl
-        instance
+        rawProduct : RawProduct {ℂ = 𝓢} 0A 0B
-          isProduct : IsProduct 𝓢 {0A} {0B} {0A×0B} proj₁ proj₂
+        RawProduct.obj   rawProduct = 0A×0B
-          isProduct {X = X} f g = (f &&& g) , lem {0X = X} f g
+        RawProduct.proj₁ rawProduct = Data.Product.proj₁
+        RawProduct.proj₂ rawProduct = Data.Product.proj₂
+        isProduct : IsProduct 𝓢 rawProduct
+        IsProduct.isProduct isProduct {X = X} f g
+          = (f &&& g) , lem {0X = X} f g
 
       product : Product {ℂ = 𝓢} 0A 0B
-      product = record
+      Product.raw       product = rawProduct
-        { obj = 0A×0B
+      Product.isProduct product = isProduct
-        ; proj₁ = Data.Product.proj₁
-        ; proj₂ = Data.Product.proj₂
-        ; isProduct = λ { {X} → isProduct {X = X}}
-        }
 
   instance
     SetsHasProducts : HasProducts 𝓢

src/Cat/Category/Product.agda

@@ -2,61 +2,60 @@ module Cat.Category.Product where
 
 open import Agda.Primitive
 open import Cubical
-open import Data.Product as P hiding (_×_)
+open import Data.Product as P hiding (_×_ ; proj₁ ; proj₂)
 
-open import Cat.Category
+open import Cat.Category hiding (module Propositionality)
 
 open Category
 
-module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') {A B obj : Object ℂ} where
+module _ {ℓa ℓb : Level} where
-  IsProduct : (π₁ : ℂ [ obj , A ]) (π₂ : ℂ [ obj , B ]) → Set (ℓ ⊔ ℓ')
+  record RawProduct {ℂ : Category ℓa ℓb} (A B : Object ℂ) : Set (ℓa ⊔ ℓb) where
-  IsProduct π₁ π₂
+    no-eta-equality
-    = ∀ {X : Object ℂ} (x₁ : ℂ [ X , A ]) (x₂ : ℂ [ X , B ])
+    field
-    → ∃![ x ] (ℂ [ π₁ ∘ x ] ≡ x₁ P.× ℂ [ π₂ ∘ x ] ≡ x₂)
+      obj : Object ℂ
+      proj₁ : ℂ [ obj , A ]
+      proj₂ : ℂ [ obj , B ]
 
--- Tip from Andrea; Consider this style for efficiency:
+  record IsProduct (ℂ : Category ℓa ℓb) {A B : Object ℂ} (raw : RawProduct {ℂ = ℂ} A B) : Set (ℓa ⊔ ℓb) where
--- record IsProduct {ℓa ℓb : Level} (ℂ : Category ℓa ℓb)
+    open RawProduct raw public
---   {A B obj : Object ℂ} (π₁ : Arrow ℂ obj A) (π₂ : Arrow ℂ obj B) : Set (ℓa ⊔ ℓb) where
+    field
---   field
+      isProduct : ∀ {X : Object ℂ} (x₁ : ℂ [ X , A ]) (x₂ : ℂ [ X , B ])
---      issProduct : ∀ {X : Object ℂ} (x₁ : ℂ [ X , A ]) (x₂ : ℂ [ X , B ])
+        → ∃![ x ] (ℂ [ proj₁ ∘ x ] ≡ x₁ P.× ℂ [ proj₂ ∘ x ] ≡ x₂)
---        → ∃![ x ] (ℂ [ π₁ ∘ x ] ≡ x₁ P.× ℂ [ π₂ ∘ x ] ≡ x₂)
 
--- open IsProduct
+    -- | Arrow product
+    _P[_×_] : ∀ {X} → (π₁ : ℂ [ X , A ]) (π₂ : ℂ [ X , B ])
+      → ℂ [ X , obj ]
+    _P[_×_] π₁ π₂ = P.proj₁ (isProduct π₁ π₂)
 
--- TODO `isProp (Product ...)`
+  record Product {ℂ : Category ℓa ℓb} (A B : Object ℂ) : Set (ℓa ⊔ ℓb) where
--- TODO `isProp (HasProducts ...)`
+    field
-record Product {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} (A B : Object ℂ) : Set (ℓ ⊔ ℓ') where
+      raw        : RawProduct {ℂ = ℂ} A B
-  no-eta-equality
+      isProduct  : IsProduct ℂ {A} {B} raw
-  field
-    obj : Object ℂ
-    proj₁ : ℂ [ obj , A ]
-    proj₂ : ℂ [ obj , B ]
-    {{isProduct}} : IsProduct ℂ proj₁ proj₂
 
-  -- | Arrow product
+    open IsProduct isProduct public
-  _P[_×_] : ∀ {X} → (π₁ : ℂ [ X , A ]) (π₂ : ℂ [ X , B ])
-    → ℂ [ X , obj ]
-  _P[_×_] π₁ π₂ = proj₁ (isProduct π₁ π₂)
 
-record HasProducts {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') : Set (ℓ ⊔ ℓ') where
+  record HasProducts (ℂ : Category ℓa ℓb) : Set (ℓa ⊔ ℓb) where
-  field
+    field
-    product : ∀ (A B : Object ℂ) → Product {ℂ = ℂ} A B
+      product : ∀ (A B : Object ℂ) → Product {ℂ = ℂ} A B
 
-  open Product hiding (obj)
+    module _ (A B : Object ℂ) where
+      open Product (product A B)
+      _×_ : Object ℂ
+      _×_ = obj
 
-  module _ (A B : Object ℂ) where
+    -- | Parallel product of arrows
-    open Product (product A B)
+    --
-    _×_ : Object ℂ
+    -- The product mentioned in awodey in Def 6.1 is not the regular product of
-    _×_ = obj
+    -- arrows. It's a "parallel" product
+    module _ {A A' B B' : Object ℂ} where
+      open Product
+      open Product (product A B) hiding (_P[_×_]) renaming (proj₁ to fst ; proj₂ to snd)
+      _|×|_ : ℂ [ A , A' ] → ℂ [ B , B' ] → ℂ [ A × B , A' × B' ]
+      a |×| b = product A' B'
+        P[ ℂ [ a ∘ fst ]
+        ×  ℂ [ b ∘ snd ]
+        ]
 
-  -- | Parallel product of arrows
+module Propositionality where
-  --
+  -- TODO `isProp (Product ...)`
-  -- The product mentioned in awodey in Def 6.1 is not the regular product of
+  -- TODO `isProp (HasProducts ...)`
-  -- arrows. It's a "parallel" product
-  module _ {A A' B B' : Object ℂ} where
-    open Product (product A B) hiding (_P[_×_]) renaming (proj₁ to fst ; proj₂ to snd)
-    _|×|_ : ℂ [ A , A' ] → ℂ [ B , B' ] → ℂ [ A × B , A' × B' ]
-    a |×| b = product A' B'
-      P[ ℂ [ a ∘ fst ]
-      ×  ℂ [ b ∘ snd ]
-      ]