From fae492a1e33f212085a371a790debc944343e02b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Thu, 8 Mar 2018 10:20:29 +0100 Subject: [PATCH] Restructure products --- src/Cat/Categories/Cat.agda | 17 ++++--- src/Cat/Categories/Sets.agda | 18 +++---- src/Cat/Category/Product.agda | 91 +++++++++++++++++------------------ 3 files changed, 63 insertions(+), 63 deletions(-) diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda index 5e442b3..3ae0c4b 100644 --- a/src/Cat/Categories/Cat.agda +++ b/src/Cat/Categories/Cat.agda @@ -151,16 +151,17 @@ module _ {ℓ ℓ' : Level} (unprovable : IsCategory (RawCat ℓ ℓ')) where private module P = CatProduct ℂ 𝔻 - instance - isProduct : IsProduct Catℓ P.proj₁ P.proj₂ - isProduct = P.isProduct + rawProduct : RawProduct {ℂ = Catℓ} ℂ 𝔻 + RawProduct.obj rawProduct = P.obj + RawProduct.proj₁ rawProduct = P.proj₁ + RawProduct.proj₂ rawProduct = P.proj₂ + + isProduct : IsProduct Catℓ rawProduct + IsProduct.isProduct isProduct = P.isProduct product : Product {ℂ = Catℓ} ℂ 𝔻 - product = record - { obj = P.obj - ; proj₁ = P.proj₁ - ; proj₂ = P.proj₂ - } + Product.raw product = rawProduct + Product.isProduct product = isProduct instance hasProducts : HasProducts Catℓ diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index 11ddc3f..970ae96 100644 --- a/src/Cat/Categories/Sets.agda +++ b/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 - isProduct : IsProduct 𝓢 {0A} {0B} {0A×0B} proj₁ proj₂ - isProduct {X = X} f g = (f &&& g) , lem {0X = X} f g + rawProduct : RawProduct {ℂ = 𝓢} 0A 0B + RawProduct.obj 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 + = (f &&& g) , lem {0X = X} f g product : Product {ℂ = 𝓢} 0A 0B - product = record - { obj = 0A×0B - ; proj₁ = Data.Product.proj₁ - ; proj₂ = Data.Product.proj₂ - ; isProduct = λ { {X} → isProduct {X = X}} - } + Product.raw product = rawProduct + Product.isProduct product = isProduct instance SetsHasProducts : HasProducts 𝓢 diff --git a/src/Cat/Category/Product.agda b/src/Cat/Category/Product.agda index 490f415..80baaab 100644 --- a/src/Cat/Category/Product.agda +++ b/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 - IsProduct : (π₁ : ℂ [ obj , A ]) (π₂ : ℂ [ obj , B ]) → Set (ℓ ⊔ ℓ') - IsProduct π₁ π₂ - = ∀ {X : Object ℂ} (x₁ : ℂ [ X , A ]) (x₂ : ℂ [ X , B ]) - → ∃![ x ] (ℂ [ π₁ ∘ x ] ≡ x₁ P.× ℂ [ π₂ ∘ x ] ≡ x₂) +module _ {ℓa ℓb : Level} where + record RawProduct {ℂ : Category ℓa ℓb} (A B : Object ℂ) : Set (ℓa ⊔ ℓb) where + no-eta-equality + field + obj : Object ℂ + proj₁ : ℂ [ obj , A ] + proj₂ : ℂ [ obj , B ] --- Tip from Andrea; Consider this style for efficiency: --- record IsProduct {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) --- {A B obj : Object ℂ} (π₁ : Arrow ℂ obj A) (π₂ : Arrow ℂ obj B) : Set (ℓa ⊔ ℓb) where --- field --- issProduct : ∀ {X : Object ℂ} (x₁ : ℂ [ X , A ]) (x₂ : ℂ [ X , B ]) --- → ∃![ x ] (ℂ [ π₁ ∘ x ] ≡ x₁ P.× ℂ [ π₂ ∘ x ] ≡ x₂) + record IsProduct (ℂ : Category ℓa ℓb) {A B : Object ℂ} (raw : RawProduct {ℂ = ℂ} A B) : Set (ℓa ⊔ ℓb) where + open RawProduct raw public + field + isProduct : ∀ {X : Object ℂ} (x₁ : ℂ [ X , A ]) (x₂ : ℂ [ X , B ]) + → ∃![ x ] (ℂ [ proj₁ ∘ x ] ≡ x₁ P.× ℂ [ proj₂ ∘ x ] ≡ x₂) --- open IsProduct + -- | Arrow product + _P[_×_] : ∀ {X} → (π₁ : ℂ [ X , A ]) (π₂ : ℂ [ X , B ]) + → ℂ [ X , obj ] + _P[_×_] π₁ π₂ = P.proj₁ (isProduct π₁ π₂) --- TODO `isProp (Product ...)` --- TODO `isProp (HasProducts ...)` -record Product {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} (A B : Object ℂ) : Set (ℓ ⊔ ℓ') where - no-eta-equality - field - obj : Object ℂ - proj₁ : ℂ [ obj , A ] - proj₂ : ℂ [ obj , B ] - {{isProduct}} : IsProduct ℂ proj₁ proj₂ + record Product {ℂ : Category ℓa ℓb} (A B : Object ℂ) : Set (ℓa ⊔ ℓb) where + field + raw : RawProduct {ℂ = ℂ} A B + isProduct : IsProduct ℂ {A} {B} raw - -- | Arrow product - _P[_×_] : ∀ {X} → (π₁ : ℂ [ X , A ]) (π₂ : ℂ [ X , B ]) - → ℂ [ X , obj ] - _P[_×_] π₁ π₂ = proj₁ (isProduct π₁ π₂) + open IsProduct isProduct public -record HasProducts {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') : Set (ℓ ⊔ ℓ') where - field - product : ∀ (A B : Object ℂ) → Product {ℂ = ℂ} A B + record HasProducts (ℂ : Category ℓa ℓb) : Set (ℓa ⊔ ℓb) where + field + 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 - open Product (product A B) - _×_ : Object ℂ - _×_ = obj + -- | Parallel product of arrows + -- + -- The product mentioned in awodey in Def 6.1 is not the regular product of + -- 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 - -- - -- The product mentioned in awodey in Def 6.1 is not the regular product of - -- 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 ] - ] +module Propositionality where + -- TODO `isProp (Product ...)` + -- TODO `isProp (HasProducts ...)`